Нейросеть решила девять математических задач, над которыми десятилетиями бились ученые

Исследователи Google DeepMind создали систему искусственного интеллекта AlphaProof Nexus, которая смогла найти и формально доказать решения девяти открытых математических задач венгерского математика Пала Эрдёша. Всего система проверила 353 задачи из его каталога.

В числе результатов — две задачи, которые оставались нерешенными более 50 лет. Кроме того, ИИ доказал 44 гипотезы из 492, связанных с онлайн-энциклопедией целочисленных последовательностей. Результаты работы опубликованы в издании EurekAlert!.

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

Как устроена система

AlphaProof Nexus разработали на основе прежних математических инструментов Google DeepMind, в том числе AlphaProof, которую ранее обучили решать сложные математические задачи. В 2024 году AlphaProof вместе с другой системой компании, AlphaGeometry 2, решила четыре из шести задач Международной математической олимпиады. Теперь исследователи попытались приспособить этот подход для решения открытых проблем, над которыми работают профессиональные математики.

В новой системе большие языковые модели объединены с инструментами формального доказательства. Сначала ИИ анализирует математическую задачу, представленную на языке Lean, а затем пытается найти решение.

Какие задачи удалось решить

Исследователи испытали AlphaProof Nexus на нескольких наборах математических проблем. В каталоге Эрдёша они выбрали 353 открытые задачи, из которых ИИ решил девять. Это не означает, что система разобралась со всеми нерешенными вопросами математика: речь идет только о тех задачах, которые вошли в эксперимент.

Еще одним направлением проверки стали гипотезы, связанные с Онлайн-энциклопедией целочисленных последовательностей — базой данных, в которой собраны последовательности чисел и сведения об их свойствах. Из 492 открытых гипотез система доказала 44.

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

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

Почему важна автоматическая проверка

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

Одна из трудностей при использовании языковых моделей в математике состоит в том, что они могут выдать убедительно выглядящее решение с незаметным логическим пробелом. Поэтому важен не только сам ответ, но и возможность независимо проверить доказательство.

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

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

Авторы исследования считают, что этот метод можно применять и за пределами чистой математики. В частности, формальный поиск доказательств и автоматическая проверка рассуждений могут помочь в задачах оптимизации, теории графов и квантовой оптики — областях, где математические доказательства используются для обоснования научных выводов.

При этом работа не означает, что ИИ уже способен самостоятельно решать любые сложные научные задачи. В эксперименте он нашел доказательства лишь для части выбранных открытых проблем. Однако исследование демонстрирует способ, с помощью которого языковые модели могут не только генерировать математические идеи, но и превращать их в доказательства, пригодные для строгой автоматической проверки.

Photo For Everything / Shutterstock / Fotodom