Математики нашли ошибку в решении ИИ задачи тысячелетия
Недавний громкий прорыв искусственного интеллекта в математике поставлен под сомнение. В Lean-коде решения уравнений Навье — Стокса найдено отличие от текстового варианта. Статья об ошибке выложена на сервере препринтов arXiv. Она допущена при переводе в код и не означает, что доказательство неверно, подчеркивают авторы анализа.
«Со всеми этими доказательствами, сгенерированными большими языковыми моделями, приходится разбираться людям, а это дает огромную дополнительную нагрузку на математиков», — говорит один из них, профессор Андерс Хансен из Кембриджского университета.
Когда OpenAI объявила о победе ИИ в математике, она обнародовала сразу две версии решения — на естественном языке и компьютерном. Вторая нужна для упрощения проверки: вместо того чтобы вычитывать длинный манускрипт, изобилующий формулами, можно поручить это компьютеру.
«Этот процесс формализации пытается заменить рецензирование. Рецензирование означало бы, что доказательства изучаются человеком. Но в нашей статье мы показали, что использование такого рода автоформализации с помощью ИИ не может служить той же цели», — объясняет соавтор статьи Фабиан Чирчелли из Кембриджского университета.
«Мы не говорим, что доказательство на естественном языке неверно. Мы также не говорим, что оно верно», — добавляет Хансен.
Их претензия состоит в том, что OpenAI декларировала обе версии как абсолютно идентичные.
В чем ошибка
Как и текстовое, решение на Lean писал тоже ИИ. Если в процессе автоформализации попадается участок доказательства, который не компилируется, он попытается найти обходной путь, даже если для этого придется отклонится от доказательства на естественном языке.
Конкретно ошибка выявлена в лемме 8.6. В доказательстве на естественном языке одно из уравнений в этой части требует, чтобы некая величина была меньше m+4, где m — целое число. В доказательстве на Lean эквивалентная величина должна быть меньше m+5, что математически слабее.
Проиллюстрируем на примере. Допустим, есть уравнение x+3=6, ответ на которое — x=3. Можно доказать, что x должен быть меньше 4, а также что x должен быть меньше 5. Оба доказательства будут верны, но говорят они о разном. Второе допускает больше возможных x, что делает его математически слабее.
OpenAI подтвердила, что ей известно о несоответствии между тестовым и Lean доказательствами, и это не значит, что какое-то из них неправильное. Ошибку обещали исправить, кроме того, продолжается работа по формализации 722 решений, о которых стало известно на днях.
Авторы исследования искали расхождения с помощью ChatGPT, этот процесс был кропотливым и в известной мере сюрреалистическим: каждую из находок проверяли вручную. Многие из несоответствий, выявленных ИИ, на деле оказывались непротиворечивыми. «Проверять это все вручную было кошмаром», — признается Хансен. Работа заняла две недели.
Вопрос доверия
Качество автоформализации решений ИИ-моделями важно с точки зрения доверия математиков этим результатам. Исследование показало, как ChatGPT может написать версию доказательства на Lean, которая не совпадает с исходной на естественном языке, при этом незаметно изменяет логическую аргументацию, чтобы скрыть любые ошибки. «Он как будто старается помочь — но это не помощь», — считает профессор.
В более длинном и сложном доказательстве такое расхождение могли бы и не обнаружить. Эта проблема доверия становится еще более актуальной в свете публикации массива из 722 решений OpenAI.
ИИ сильно упростил жизнь, и науку в частности. Но опасно думать: «Ну все, теперь достаточно просто прочесть статью», убежден Хансен
«Цель науки в том, чтобы человечество понимало, как устроен мир, чтобы мы могли принимать обоснованные решения. Если мы потеряем это понимание — что тогда?» — заключил он.
