Математики усомнились в проверке доказательств OpenAI
OpenAI опубликовала 719 рукописей с заявленными решениями сложных открытых математических задач, однако подход лаборатории вызвал вопросы у математического сообщества. Цепочки рассуждений модели раскрыты только для 10 работ, а 42% опубликованных доказательств ещё не были формализованы в проверяемом виде.
Рекомендации AGMAI и открытые вопросы
Перед публикацией OpenAI консультировалась с Advisory Group on Mathematics and Artificial Intelligence, или AGMAI. Группа из девяти исследователей работает при Institute for Advanced Study Принстонского университета и в конце сентября выпустила рекомендации для разработчиков передовых ИИ-моделей.
В числе первых рекомендаций AGMAI был призыв не тестировать продвинутые математические задачи на проприетарных моделях. При этом OpenAI прямо указала, что использует открытые исследовательские задачи для оценки собственных закрытых моделей.
Группа также настаивала на ответственности за то, чтобы после выпуска результата появилось человеческое понимание доказательства. OpenAI быстро раскрыла результаты и часть сведений о том, как модели пришли к выводам, однако представленных материалов недостаточно для полноценной независимой оценки всех работ.
Проблема перевода доказательств в Lean
Особое внимание привлекла статья математиков University of Cambridge и King’s College London. Авторы изучили предложенное OpenAI решение задачи, связанной с уравнениями Навье — Стокса, которые описывают сложное поведение жидкостей.
Обычно модель сначала формулирует объяснение на естественном языке, а затем выражает его в Lean — языке программирования, где доказательство можно проверить компиляцией. Исследователи обнаружили как минимум два расхождения между текстовым доказательством и Lean-кодом. Они не опровергают автоматически ни один из вариантов решения, но показывают риск автоматического перевода без человеческого контроля.
Авторы статьи отмечают, что из-за таких ошибок перевода текстовые и автоматически формализованные доказательства OpenAI не следует принимать без той же экспертной проверки, которой подвергаются другие математические работы. AGMAI также предлагала добавлять машиночитаемые метаданные, связывающие текстовое доказательство с формальным артефактом, но в этой публикации OpenAI таких данных не предоставила.
Почему важна работа математиков
Профессор Гарвардского университета Мелани Вуд подчеркнула, что на момент выпуска решений человеческого понимания может не быть, и последующая работа только начинается. Терри Тао также указал, что авторы запросов к ИИ не всегда способны отвечать на вопросы о полученном результате, выступать с докладами и обсуждать его с профессиональным сообществом.
На фоне публичных планов отрасли, таких как публичных планов отрасли в сфере ИИ, дискуссия о математических доказательствах показывает разницу между демонстрацией возможностей модели и признанием результата научным сообществом. Для компаний, использующих ИИ в исследованиях и инженерных расчётах, практический вывод состоит в необходимости независимой экспертизы, прослеживаемой связи между текстом и формальным кодом и участия профильных специалистов до применения результата.