Google DeepMind представила результаты исследования, в котором её исследовательский агент AlphaProof Nexus продемонстрировал способность решать не олимпиадные примеры, а открытые математические проблемы исследовательского уровня. Система решила 9 из 353 открытых задач, связанных с именем венгерского математика Пала Эрдёша, причём две из них оставались без решения 56 лет. Помимо этого, агент доказал 44 из 492 открытых гипотез из Онлайн-энциклопедии целочисленных последовательностей (OEIS). По оценке авторов, вычисления для каждой решённой задачи Эрдёша обошлись в несколько сотен долларов.

Девять задач Эрдёша и 44 гипотезы OEIS

Работа посвящена применению больших языковых моделей для поиска формальных доказательств. Авторы сознательно вышли за рамки стандартных олимпиадных задач и проверили подход на genuinely открытых проблемах, над которыми математика бьётся годами. Успех в 9 задачах Эрдёша и 44 гипотезах OEIS показывает, что подход пригоден для исследовательской математики, а не только для учебных и соревновательных примеров. При этом важно, что большинство открытых задач Эрдёша агент решить не смог: нынешние успехи сосредоточены в областях, для которых уже существует развитая библиотека формализованных результатов и сложные рассуждения удаётся разбить на отдельные подзадачи.

Формальная проверка вместо убедительного объяснения

Ключевое отличие AlphaProof Nexus от обычного чат-бота — использование Lean, языка и среды для формализации математических доказательств. ИИ предлагает доказательство в формальном виде, после чего Lean проверяет каждый логический шаг. Если проверка обнаруживает ошибку, агент получает обратную связь и продолжает поиск. Убедительно написанного объяснения недостаточно: результат должен пройти машинную проверку по строгим логическим правилам. Именно эта петля «генерация — проверка — коррекция» делает процесс пригодным для реальной математики, а не для генерации правдоподобного текста.

Архитектура: несколько агентов и эволюционный алгоритм

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

Простой агент тоже справился — но дороже

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

Горизонты и пределы

Возможности системы не ограничиваются задачами Эрдёша и гипотезами OEIS. AlphaProof Nexus помогла решить открытую задачу в алгебраической геометрии, улучшить оценку в выпуклой оптимизации и обнаружить ошибки в формализации математических утверждений, встречавшиеся в научной литературе. Её также используют в исследованиях по теории графов и квантовой оптике. Вместе с тем система наследует ограничения языковых моделей: результаты поиска могут сильно различаться от попытки к попытке, а задачи, требующие разработки обширной новой теории, остаются за пределами её возможностей. Авторы считают, что формальные доказательства могут стать способом включить ИИ в настоящую математическую работу, а не просто получать от него ответы.