ИИ решает сложные задачи по математике: расхождения между доказательством и кодом Lean
Сотни решений за раз
OpenAI опубликовала сотни заявленных решений одних из самых сложных математических задач современности. Лаборатория заявила, что перед публикацией консультировалась с группой ведущих математиков, чтобы избежать скандала, сопровождавшего прошлое громкое «решение» её модели. Однако, как отмечает TechCrunch, планка сообщества соблюдена не была — прежде всего там, где математики настаивали на необходимости человеческого понимания результата.
Что говорят математики
Консультативная группа по математике и искусственному интеллекту (AGMAI) при Институте перспективных исследований (IAS), объединяющая девять известных исследователей, в конце сентября выпустила рекомендации для фронтир-лабораторий. Первая же просьба группы — «прекратить тестировать сложные математические задачи на проприетарных моделях» — оказалась проигнорирована: релиз OpenAI прямо говорит, что компания оценивает свои закрытые модели на открытых исследовательских задачах.
Из 719 рукописей только в 10 опубликована цепочка рассуждений модели, а формализацию прошли менее половины работ. По мнению сообщества, для доказательств, которые человек не понимает, формализация обязательна — но OpenAI этого требования не выполнила.
«Потерянные в переводе»
Известный математик Теренс Тао раскритиковал подход: по его словам, задачи «решаются автономно ИИ-промптерами, которым нет дела до самой области, как только их первоначальная цель „решена“», и они не понимают вывод настолько, чтобы отвечать на вопросы или выступать с докладами.
Проблему иллюстрирует работа математиков из Кембриджского университета и Королевского колледжа Лондона. Когда модель решает задачу, она сначала формулирует объяснение на естественном языке, а затем переводит его в Lean — язык программирования, который в теории подтверждает корректность доказательства при компиляции. Исследователи задокументировали минимум два расхождения между словесным доказательством и кодом Lean в решении OpenAI задачи, производной от уравнений Навье — Стокса, описывающих поведение жидкостей.
Эти расхождения не обязательно опровергают сами решения, но ставят под вопрос доверие к автопереводу доказательств без участия человека. «Из-за эффекта mistranslation доказательство OpenAI на естественном языке и другие автоформализованные доказательства на Lean не должны априори приниматься без той же экспертной проверки, которой подвергаются остальные работы», — заключают авторы.
Источник: TechCrunch
Об авторе
