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