Математический прорыв OpenAI оказался под вопросом — учёные нашли расхождение в доказательстве

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

Источник изображения: Thomas T /unsplash.com

По словам математиков, расхождение вовсе не означает, что доказательства неверны или что OpenAI неправильно решила задачу, но это ставит под сомнение, всегда ли можно полагаться на математические результаты, генерируемые моделями искусственного интеллекта.

«Что нужно сделать со всеми этими большими доказательствами, созданными на основе языковой модели, так это то, что они должны быть прочитаны людьми, и это создает огромную дополнительную нагрузку на математиков», — сообщил руководитель команды Андерс Хансен (Anders Hansen).

Процесс поиска расхождений занял у команды около двух недель. При этом математики использовали подсказки ChatGPT. Напомним, что у OpenAI на решение задачи ушло 88 часов.

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

Представим, что вас попросили решить уравнение x + 3 = 6, ответом на которое является x = 3. Можно написать доказательство того, что x должно быть меньше 4, а также того, что x должно быть меньше 5. Оба эти математических утверждения абсолютно верны, но последнее допускает больше возможных ответов для x, что делает его математически более слабым.

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

Кевин Баззард (Kevin Buzzard) из Имперского колледжа Лондона сообщил, что можно надёжно формализовать в Lean саму формулировку теоремы и затем проверить, компилируется ли доказательство. Но это не гарантирует, что текстовое доказательство в PDF корректно передаёт логику. То есть Lean‑код может быть внутренне согласован, но не соответствовать тому, что написано в статье. «Я уверен, что проблема Навье — Стокса была решена правильно, — говорит Баззард. — Я гораздо менее уверен в том, что доказательство, описанное текстом, является правильным».

OpenAI сообщила ресурсу New Scientist, что ей известно о несоответствии между доказательством на естественном языке и в виде кода, и что это не означает, что ни одно из них недействительно.