Математический прорыв OpenAI вызывает вопросы из-за расхождений в доказательстве
Математический прорыв OpenAI начал вызывать вопросы после того, как учёные сравнили опубликованное доказательство по уравнениям Навье — Стокса с его алгоритмической Lean-версией и нашли расхождения. В нескольких ключевых местах машинный вариант, проверяемый на компьютере, содержит более слабые утверждения. Это ещё не опровержение, но почва для сомнений уже вполне плодородна, сообщает 3dnews.
«Что нужно сделать со всеми этими большими доказательствами, созданными на основе языковой модели, так это то, что они должны быть прочитаны людьми, и это создает огромную дополнительную нагрузку на математиков», — сообщил руководитель команды Андерс Хансен.
По словам математиков, расхождение не означает, что доказательства неверны или что OpenAI неправильно решила задачу, но это ставит под сомнение, всегда ли можно полагаться на математические результаты, генерируемые моделями искусственного интеллекта. Процесс поиска расхождений занял у команды около двух недель. При этом математики использовали подсказки ChatGPT.
Математики указали на расхождение в части доказательств, называемой леммой 8.6. В доказательстве на естественном языке уравнение в этой части требует, чтобы определённое значение было меньше m + 4, где m — целое число, а в Lean‑версии — меньше m + 5, что математически слабее, поскольку допускает больше возможных решений и не эквивалентно первому.
По словам Хансена, неправильный перевод мог возникнуть из-за того, что ИИ стремится к тому, чтобы компьютерный код был полностью самосогласован и не выдавал ошибок. Если в процессе автоматической формализации ИИ обнаружит часть доказательства, которая не компилируется, он попытается найти обходной путь, даже если это означает отклонение от доказательства, написанного на естественном языке.
Кевин Баззард из Имперского колледжа Лондона сообщил, что можно надёжно формализовать в Lean саму формулировку теоремы и затем проверить, компилируется ли доказательство. Но это не гарантирует, что текстовое доказательство в PDF корректно передаёт логику. То есть Lean‑код может быть внутренне согласован, но не соответствовать тому, что написано в статье.
OpenAI сообщила ресурсу New Scientist, что ей известно о несоответствии между доказательством на естественном языке и в виде кода, и что это не означает, что ни одно из них недействительно.
Подписывайтесь на наш Telegram-канал, чтобы быть в курсе всех новостей и событий Рунета.
