OpenAI выпустила сотни решений сложных математических задач, однако соблюдение рекомендаций группы Advisory Group on Mathematics and Artificial Intelligence (AGMAI) оказалось неполным. Об этом сообщает TechCrunch. Группа, которую курирует Институт перспективных исследований Принстонского университета, объединяет девять известных математиков из разных стран.
AGMAI опубликовала рекомендации для разработчиков передовых моделей, решающих математические задачи, в конце сентября. В заявлении по поводу новых доказательств группа подчеркнула: «в конечном счете математическое сообщество должно оценить, насколько успешно были выполнены наши рекомендации». При этом первым требованием AGMAI был отказ от проверки сложных математических задач на закрытых моделях, тогда как OpenAI прямо указала, что тестирует собственные модели на открытых исследовательских задачах.
OpenAI выпустила 719 рукописей и сопроводила часть материалов сведениями о том, как модели пришли к своим выводам. Однако цепочка рассуждений модели была опубликована только для 10 работ. Кроме того, математики рекомендовали формализовать доказательства, которые люди не могут понять, но такая процедура не была проведена для 42% представленных решений.
Отдельные вопросы вызвала работа, подготовленная математиками Кембриджского университета и Королевского колледжа Лондона. Авторы изучили решение задачи, связанной с уравнениями Навье—Стокса, описывающими сложное поведение жидкостей. Модели сначала формулируют доказательство на естественном языке, а затем переводят его в Lean — язык программирования, который должен подтверждать корректность решения после компиляции кода.
Исследователи обнаружили как минимум два расхождения между текстовым доказательством OpenAI и соответствующим кодом Lean. Эти несоответствия сами по себе не доказывают ошибочность решения, но ставят под сомнение возможность полностью доверять автоматическому переводу без участия человека. AGMAI также призывала публиковать машиночитаемые данные, связывающие текст доказательства с его формальной версией, однако в новых материалах OpenAI таких данных не оказалось.
«Из-за явления ошибочных переводов, на которое указывает эта статья, текстовое доказательство OpenAI и другие автоматически формализованные доказательства на Lean не следует считать заслуживающими доверия без предварительной экспертной проверки и такого же тщательного изучения, которым подвергаются другие доказательства», — заключили авторы исследования. Математик Терренс Тао ранее написал, что решения создаются автономно людьми, которые после получения результата не всегда интересуются соответствующей областью и не способны объяснить выводы модели. Профессор математики Гарвардского университета Мелани Вуд заявила TechCrunch: «В момент публикации решения человеческого понимания их еще нет, и теперь начинается работа».