Учёные сравнили опубликованное OpenAI доказательство для уравнений Навье — Стокса с его версией на Lean и нашли расхождения. В нескольких ключевых местах машинный вариант, проверяемый компьютером, содержит более слабые утверждения.
Это ещё не опровержение, но поводы для сомнений появились.
Пример слабости утверждения. Для уравнения x + 3 = 6 (x = 3) верны и доказательство x < 4, и x < 5. Но второе допускает больше значений x, поэтому математически оно слабее.
Лемма 8.6. В тексте доказательства некое значение должно быть меньше m + 4, где m — целое число. В Lean-версии условие мягче: меньше m + 5. Оно допускает больше решений и не эквивалентно исходному.
Кевин Баззард из Имперского колледжа Лондона: в Lean можно надёжно формализовать саму теорему и проверить, компилируется ли доказательство. Но это не гарантирует, что текст в PDF верно передаёт логику.
Lean-код может быть внутренне согласованным, но не соответствовать статье. «Я уверен, что проблема Навье — Стокса была решена правильно, — говорит Баззард. — Я гораздо менее уверен в том, что доказательство, описанное текстом, является правильным».
Математики подчёркивают: расхождение не означает, что доказательства неверны или что OpenAI неправильно решила задачу. Но оно ставит под вопрос, всегда ли можно полагаться на результаты, полученные ИИ-моделями.
Поиск расхождений занял у команды около двух недель, при этом математики использовали подсказки ChatGPT. У OpenAI на решение задачи ушло 88 часов.
Руководитель команды Андерс Хансен: большие доказательства, созданные языковыми моделями, должны читать люди, и это создаёт огромную дополнительную нагрузку на математиков.
По мнению Хансена, неточный перевод мог возникнуть из-за стремления ИИ добиться полностью самосогласованного кода без ошибок. Если часть доказательства не компилируется, модель ищет обходной путь, даже отклоняясь от доказательства на естественном языке.
OpenAI сообщила New Scientist, что знает о несоответствии между доказательством на естественном языке и в коде. По её словам, это не делает недействительным ни одно из них.