Математическое сообщество сомневается, насколько можно доверять 719 математическим рукописям, сгенерированным OpenAI, после того как в новом препринте было заявлено: опубликованное компанией доказательство по уравнениям Навье — Стокса не совпадает с их же формальной, машинно-проверяемой версией.
Ключевые моменты:
- Каталог OpenAI сократился с 722 до 719 рукописей после того, как компания отозвала три работы из‑за знаковой ошибки.
- Три математика из Великобритании зафиксировали два расхождения между текстовым доказательством Навье — Стокса и его кодом на Lean.
- Авторы не утверждают, что доказательство неверно, но настаивают: машинная проверка не заменяет рецензирование специалистами.
Публикация математического корпуса OpenAI
OpenAI выложила коллекцию 6 октября. В опубликованном в четверг расследовании отмечается, что проект отклоняется от рекомендаций, которые независимая группа математиков подготовила для лабораторий ИИ. Изначально каталог включал 722 рукописи. Уже на следующий день OpenAI удалила из репозитория три работы: знаковая ошибка разрушала одно из рассуждений, а ещё две статьи на нём основывались.
Эти рекомендации были опубликованы 29 сентября девятью участниками Advisory Group on Mathematics and Artificial Intelligence (Консультативная группа по математике и искусственному интеллекту). Документ начинается с призыва к лабораториям прекратить тестировать сложные математические задачи на закрытых моделях. В репозитории OpenAI говорится, что статьи получены при оценке нерелизнутой внутренней модели на открытых исследовательских задачах.
Подробные объяснения хода рассуждений модели даны лишь по десяти результатам, и примерно 42% «верхнеуровневых» утверждений формализованы в Lean — языке, позволяющем компьютеру строго проверять доказательства.
Также читайте: Сколько зарабатывает CEO Anthropic? Ответ — в документах к IPO
Пробелы в доказательстве по Навье — Стоксу
Александр Бастунис из Королевского колледжа Лондона, а также Фабиан Чирцелли и Андерс Хансен из Кембриджского университета проанализировали доказательство по уравнениям Навье — Стокса, о котором OpenAI объявила в сентябре. Они описали два места, где текстовый аргумент и код на Lean расходятся, в том числе эпизод, в котором формальный код устанавливает более слабую оценку, чем заявлено в статье.
Авторы подчёркивают, что не выносят суждения о корректности самого текстового доказательства. Их тезис уже: Lean подтверждает истинность конечной теоремы, пишут они, но не гарантирует корректность промежуточных шагов, которые читает человек. Поэтому формализованные доказательства по‑прежнему нуждаются в классическом рецензировании.
Обладатель медали Филдса Теренс Тао написал 6 октября, что многие задачи сейчас «решаются промпт-джоками ИИ», которые сами недостаточно понимают полученные результаты, чтобы отвечать на вопросы или читать по ним доклады. Профессор Гарварда Мелани Мэтчетт Вуд, член консультативной группы, добавила, что на момент публикации «ни один человек ещё не понимает эти доказательства целиком — и теперь работа только начинается».
Спор вокруг доказательства OpenAI
Консультативная группа заявила, что только широкое математическое сообщество может оценить, насколько OpenAI соблюла её рекомендации. Это происходит на фоне напряжённого месяца. OpenAI объявила о результатах по Навье — Стоксу 8 сентября, что спровоцировало спор о приоритете с математиком Нью-Йоркского университета Тристаном Бакмастером. Уже через три дня 25 лауреатов медали Филдса выступили с декларацией, предупреждая, что массовое производство результатов ИИ может нанести ущерб развитию математики.
Читайте далее: OpenAI выложила 722 математические статьи ИИ. Теперь слово за математиками
