OpenAI опубликовала сотни «решений» сложнейших задач, но математики указывают на расхождения

На этой неделе OpenAI опубликовала сотни заявленных решений одних из самых сложных математических задач в мире. Лаборатория заявила, что консультировалась с advisory-группой элитных математиков, чтобы избежать скандала, который возник в прошлый раз, когда одна из её моделей решила давнюю проблему в этой области.

Однако OpenAI не соответствовала этим стандартам, особенно в том, где математики подчёркивали необходимость человеческого понимания математического результата. Это особенно тревожно после публикации новой работы, выявившей расхождения между естественно-языковым и формально выраженным решением задачи на миллион долларов (~80 млн рублей), якобы решённой моделями OpenAI.

Консультативная группа по математике и искусственному интеллекту (AGMAI), действующая при Институте перспективных исследований Принстонского университета, состоит из девяти видных исследователей из учреждений по всему миру.

В конце сентября организация выпустила рекомендации для передовых лабораторий, решающих математические задачи. В заявлении о последнем наборе доказательств AGMAI отметила, что «в конечном счёте именно математическое сообщество должно оценить, насколько успешно были выполнены наши рекомендации».

Однако первым требованием организации было «прекратить тестирование сложных математических задач на проприетарных моделях». В релизе OpenAI прямо сказано, что она оценивает свои проприетарные модели с помощью открытых исследовательских задач по математике.

Консультативная группа не ответила на запрос TechCrunch о более тщательной оценке последнего релиза доказательств OpenAI. Лаборатория явно следовала некоторым её принципам, включая публикацию результатов как можно скорее и включение информации о том, как модели пришли к своим выводам. Но не для всех: лишь десять из 719 рукописей содержали цепочку рассуждений модели.

Для работ, которые люди не понимают, математики предложили формализовать доказательства — но лишь 42% доказательств, опубликованных OpenAI, не прошли этот процесс.

В конечном счёте остаётся неясным, берёт ли OpenAI «ответственность за обеспечение того, чтобы за этим последовало человеческое понимание» при публикации своих доказательств, в соответствии с принципами AGMAI. AGMAI предложила OpenAI помочь финансировать работу математиков-людей, которые потребуются, чтобы решения лаборатории имели какое-либо реальное значение.

«Задачи решаются автономно AI-промптерами, которые не заинтересованы в более широкой области как таковой, как только их первоначальная цель "решена", и не понимают вывод ИИ достаточно хорошо, чтобы отвечать на вопросы о результате, выступать с докладами или иным образом взаимодействовать с остальным сообществом», — написал в соцсетях после релиза Теренс Тао, видный математик, критиковавший подход OpenAI.

Эта проблема наглядно иллюстрируется работой, опубликованной на этой неделе математиками из Кембриджского университета и Королевского колледжа Лондона, которая ставит под сомнение подход передовых лабораторий к этим задачам.

Когда ИИ-модели решают математические задачи, они сначала создают объяснение на «естественном языке», а затем пытаются выразить результат на Lean — языке программирования, который теоретически подтверждает точность доказательства путём его компиляции как кода.

Однако могут возникать проблемы с тем, как модели переводят свои доказательства на естественном языке в код; эта работа документирует как минимум два расхождения между доказательством на естественном языке и кодом Lean, лежащим в основе решения, которое OpenAI предложила для задачи, производной от уравнений Навье — Стокса, описывающих сложное поведение жидкостей.

Эти расхождения не обязательно опровергают то или иное решение, но они поднимают вопросы о том, можно ли просто полагаться на модели в формализации собственных решений без участия человека. Это одна из причин, по которой AGMAI попросила OpenAI «включить машиночитаемые метаданные, связывающие естественно-языковые и формальные артефакты» — чего передовая лаборатория не сделала в этих релизах.

«Из-за феномена ошибок перевода — как подчёркивается в этой работе — доказательству на естественном языке от OpenAI и другим автоформализованным доказательствам на Lean не следует prima facie доверять без того же процесса рецензирования и проверки, которому подвергаются другие доказательства», — заключают авторы работы «потерянные в переводе».

Математики подчёркивают, что когда новые результаты открываются людьми, они берут за них ответственность и взаимодействуют с широким сообществом через статьи, доклады и семинары. Этот процесс углубляет понимание решений, находит стратегии, которые можно использовать для решения других задач, и позволяет применять новые знания в практических областях.

Когда модель получает запрос решить сложную задачу и выдаёт решение, «на момент публикации человеческого понимания этих решений нет, и вот тут-то и начинается работа», — сказала TechCrunch профессор математики Гарвардского университета Мелани Вуд.