Математики нашли ошибку в одном из доказательств задачи Навье-Стокса от OpenAI

Вероятно, модель поправила решение, чтобы верифицировать код на Lean.

Математики из Кембриджского университета и Королевского колледжа Лондона обнаружили расхождение в двух версиях доказательства задачи Навье-Стокса, опубликованных OpenAI.

Оказалось, что модель компании изменила одно из математических условий при переводе доказательства на язык Lean, используемый для формализации доказательств. Обе версии прошли соответствующие этапы подготовки, однако их содержание оказалось разным.

Исследователи обнаружили, что в текстовом доказательстве определенная величина должна быть меньше m + 4, где m обозначает целое число. В версии Lean аналогичное условие допускает значения меньше m + 5. Второе ограничение математически слабее первого, поскольку охватывает более широкий диапазон значений.

По мнению математиков, причина заключается в особенностях автоматической формализации. При преобразовании доказательства в код Lean ИИ стремится добиться успешной верификации; если какой-то фрагмент вызывает ошибку, то модель может изменить формулировку, чтобы код прошел проверку.

Примечательно, что для поиска ошибок математики использовали ChatGPT, поручив чат-боту сравнить обе версии доказательства. Находки нейросети анализировались учеными вручную, на обнаружение одного несоответствия у математиков ушло около двух недель.

Обнаруженное расхождение само по себе не доказывает ошибочность решения задачи Навье-Стокса, предложенного моделью OpenAI. Сама компания пообещала исправить все найденные проблемы.