На этой неделе OpenAI представила сотни предполагаемых решений сложных математических задач, пытаясь продемонстрировать способность своих моделей работать с продвинутыми задачами. Однако публикация не полностью соответствовала рекомендациям, разработанным консультативной группой исследователей-математиков, что вновь поставило основной вопрос: достаточно ли, чтобы модели создавали решение, пригодное для формализации в коде, или же оно должно быть понятным и поддающимся проверке со стороны математиков?
В группу Advisory Group on Mathematics and Artificial Intelligence (AGMAI) входят девять ведущих исследователей; ее принимает Институт перспективных исследований Принстонского университета. В конце сентября группа опубликовала рекомендации для лабораторий, разрабатывающих продвинутые модели для решения математических задач.
Частичное соблюдение рекомендаций исследователей
AGMAI указала, что оценка соблюдения ее рекомендаций в конечном счете относится к компетенции математического сообщества. Одна из главных рекомендаций — прекратить тестирование продвинутых математических задач на коммерчески принадлежащих моделях, тогда как OpenAI прямо сообщила, что использует открытые исследовательские задачи для оценки собственных моделей.
OpenAI последовала некоторым принципам, например быстро опубликовала результаты и предоставила информацию о том, как модели пришли к своим выводам. Однако лишь 10 из 719 рукописей содержали собственные цепочки рассуждений модели. Кроме того, 42% опубликованных доказательств не подверглись формализации.
Группа считает, что доказательства, которые трудно понять людям, следует переводить в формальную форму. Но она также подчеркнула ответственность лаборатории за то, чтобы публикация результатов сопровождалась человеческим пониманием этих результатов, и предложила финансировать математиков, которые помогали бы придавать этим результатам действительно научный смысл.
Разрыв между естественным языком и кодом Lean
Обычно модели сначала создают объяснение на естественном языке, а затем пытаются перевести его в Lean — язык программирования, компилятор которого может подтвердить согласованность доказательства в исполнимой форме. Однако автоматический перевод может изменить содержание доказательства или разорвать связь между тем, что говорит объяснение, и тем, что доказывает код.
В статье, опубликованной математиками из Кембриджского университета и Королевского колледжа Лондона, задокументированы как минимум два различия между доказательством на естественном языке и связанным с ним кодом Lean в решении, представленном OpenAI для задачи, производной от уравнений Navier-Stokes, описывающих поведение сложных текучих сред. Эти различия не обязательно доказывают ошибочность какого-либо из двух решений, но вызывают сомнения в том, стоит ли позволять моделям самостоятельно формализовать свои решения без участия человека.
AGMAI также попросила включать машиночитаемые метаданные, связывающие текстовое доказательство с формальной версией, однако OpenAI не предоставила их в этих публикациях. Авторы статьи, известной под названием “lost in translation”, пришли к выводу, что текстовые доказательства и автоматически преобразованные доказательства Lean не следует изначально принимать без экспертной оценки и проверки, сопоставимых с теми, которым подвергаются другие доказательства.
Почему это важно?
Проблема заключается не только в подтверждении того, что код успешно компилируется, но и в доказательстве того, что код действительно представляет математическую идею, объясненную в тексте. В традиционном исследовании ученые несут ответственность за свои результаты и обсуждают их в статьях, на лекциях и семинарах — этот процесс помогает выявлять ошибки и понимать методы, пригодные для повторного использования.
Когда же модели создают решение сложной задачи, такого человеческого понимания может не быть на момент публикации. Поэтому текущие результаты OpenAI выглядят скорее началом процесса научной проверки, чем завершением проблемы; человеческая экспертиза и связывание текстовых и формальных выводов остаются двумя нерешенными условиями перед принятием этих доказательств математическим сообществом.