У Google DeepMind есть ИИ-агент, решивший девять открытых задач, связанных с именем Пала Эрдёша, причём две из них оставались нерешёнными 56 лет. Но самое интересное — не заголовок, а детали: авторы также рассказывают, с чем система не справилась, а более дешёвый и простой агент оказался почти столь же способным.
Результаты в цифрах
Система называется AlphaProof Nexus. Её испытали на 353 открытых задачах, связанных с венгерским математиком Эрдёшем, и она решила 9 из них — примерно 2,5 процента. Ей также предложили 492 недоказанные гипотезы из Online Encyclopedia of Integer Sequences (OEIS), и она доказала 44 — чуть меньше 9 процентов.
Затраты — тоже часть этой истории. На каждую решённую задачу Эрдёша ушло вычислительных ресурсов на несколько сотен долларов. Это не копейки, но меньше недельного бюджета научного семинара на кофе и значительно дешевле, чем 56 лет, в течение которых математики так и не замечали доказательство.
| Бенчмарк | Открытых задач | Решено |
|---|---|---|
| Erdős problems | 353 | 9 (две оставались открытыми 56 лет) |
| OEIS conjectures | 492 | 44 |
Почему Lean меняет суть дела
Любой, кто просил чат-бота предложить доказательство, знает типичный сценарий провала. Ответ звучит замечательно, читается легко, а на четвёртом шаге оказывается неверным. Убедительная проза — единственное, что языковые модели производят даром.
AlphaProof Nexus обходит эту проблему, работая в Lean — языке и среде для формализации математических доказательств. Модель записывает доказательство в формальном виде, а Lean проверяет каждый логический шаг. Если что-то не проходит проверку, агент получает сообщение об ошибке в качестве обратной связи и продолжает поиск. За красиво сформулированное объяснение баллов не дают. Засчитывается лишь доказательство, выдержавшее машинную проверку.
Именно в этом и состоит настоящий вклад работы. Авторы статьи поставили перед собой задачу проверить, способен ли поиск формальных доказательств под управлением LLM справляться с открытыми исследовательскими задачами, а не только с олимпиадными упражнениями. Для девяти задач Эрдёша и 44 гипотез OEIS ответ оказался положительным.
Как устроена система
Nexus — не одна модель, отвечающая на один промпт. Несколько ИИ-агентов работают параллельно: пробуют разные подходы, проверяют их и дорабатывают доказательства. В самом сложном варианте всю работу координирует эволюционный алгоритм. На некоторых этапах поиска используется AlphaProof — автоматическая система доказательства теорем от DeepMind, основанная на обучении с подкреплением.
Механизм кажется довольно громоздким, поэтому авторы поступили разумно: решили проверить, нужен ли он вообще.
Неудобный контрольный эксперимент
Они сравнили полную архитектуру с гораздо более простым агентом, который всего лишь чередует генерацию доказательств языковой моделью и их проверку в Lean. Когда те же девять решённых задач Эрдёша дали простому агенту, он тоже решил их все.
Здесь сложная система не выиграла по возможностям. Её преимущество проявилось на самых трудных задачах, где работа простого агента обходилась дороже. Так что сложная оркестрация дала выигрыш в эффективности, а не расширила круг доступных задач — по крайней мере, на этом наборе.
Авторы делают скромный, но полезный вывод. Результаты зависят не только от возможностей базовой языковой модели, но и от того, как организован поиск доказательств. Иначе говоря, продуманный процесс вокруг модели имеет значение, и выяснить это экспериментально дешевле, чем с помощью пресс-релиза.
Не только Эрдёш и OEIS
Систему применяли и за пределами этих двух бенчмарков. Согласно отчёту, она:
- Помогла решить открытую задачу в алгебраической геометрии.
- Улучшила оценку в выпуклой оптимизации.
- Нашла ошибки в формализации математических утверждений из опубликованной литературы.
- Применяется в исследованиях по теории графов и квантовой оптике.
К третьему пункту стоит присмотреться. Формализация — это перевод сформулированного человеком утверждения на язык Lean, и здесь легко допустить ошибку и легко её не заметить. Инструмент, который находит такие ошибки, полезен даже в те дни, когда не доказывает ничего нового.
Чего система не умеет
Авторы прямо говорят об ограничениях — приятная перемена для области, в которой ограничения обычно прячут в сносках.
- Большинство задач остаются открытыми. Из 353 задач Эрдёша 344 решить не удалось.
- Успехи сосредоточены в отдельных областях. Система справляется там, где уже есть хорошо развитая библиотека формализованных результатов, а сложные рассуждения можно разбить на отдельные подзадачи.
- Результаты нестабильны. Как и у лежащих в основе языковых моделей, результаты системы могут сильно различаться от попытки к попытке.
- Создание масштабной новой теории ей не по силам. Задачи, требующие построения обширного нового теоретического аппарата, системе пока недоступны.
Именно второй пункт стоит запомнить. Lean может проверить лишь то, что можно выразить на его языке, и помогать искать доказательства лишь там, где уже заложен достаточный формальный фундамент. Система сильнее всего там, где математики уже проделали утомительную работу, записав всё в машиночитаемом виде. Так что стоит отдать должное людям, которые формализовали эти библиотеки.
Какие выводы делают авторы
Авторы считают, что формальные доказательства могут стать способом включить ИИ в настоящую математическую работу, вместо того чтобы воспринимать его как машину, выдающую ответы, которым остаётся либо верить, либо не верить. Это становится возможным благодаря проверке. Математику не нужно доверять модели — достаточно доверять Lean.
Это более зрелый подход к результатам работы ИИ, чем привычный сценарий, в котором читателю предлагают восхититься ответом и надеяться на лучшее.
Главный вывод
Девять решённых задач из 353 не удовлетворят тех, кто надеется на математическую революцию уже ко вторнику. Но две из этих девяти не поддавались людям 56 лет, каждое доказательство прошло машинную проверку, а цена вопроса составила несколько сотен долларов. Возможно, самым полезным результатом в итоге окажется то, что простой цикл «сгенерировать и проверить» сравнялся со сложной системой на наборе решённых задач. В математике, как и во многом другом, дорогая на вид архитектура иногда оказывается просто более дорогим способом получить тот же ответ.