ИИ-агент Google DeepMind решил 9 задач Эрдёша, две ждали 56 лет
AlphaProof Nexus решил открытые математические задачи, связанные с именем венгерского математика Пала Эрдёша.
Исследовательский агент Google DeepMind ищет формальные доказательства математических утверждений с помощью нескольких ИИ-моделей и языка Lean. В исследовании авторы проверили его на открытых задачах, а не только на олимпиадных примерах.
AlphaProof Nexus решил 9 из 353 открытых задач, связанных с именем венгерского математика Пала Эрдёша. Две из них оставались без решения 56 лет. По оценке авторов, вычисления для каждой решённой задачи обошлись в несколько сотен долларов. Кроме того, система доказала 44 из 492 открытых гипотез из Онлайн-энциклопедии целочисленных последовательностей (OEIS), которая содержит математические последовательности.
Lean задаёт системе строгую проверку: агент представляет доказательство в формальном виде, а среда контролирует каждый логический шаг. Если находит ошибку, она сообщает об этом, и поиск продолжается. Одного убедительного объяснения недостаточно: доказательство должно пройти машинную проверку.
В AlphaProof Nexus несколько ИИ-агентов параллельно предлагают решения, проверяют их и уточняют доказательства. В самой сложной конфигурации их работу координирует эволюционный алгоритм. На отдельных этапах поиска система использует AlphaProof, разработанную Google DeepMind программу автоматического доказательства теорем, основанную на обучении с подкреплением.
Авторы сравнили эту архитектуру с более простым агентом: он по очереди генерирует доказательства с помощью языковой модели и проверяет их в Lean. При повторной проверке тот справился со всеми девятью решёнными задачами Эрдёша, но на самых трудных обходился дороже. Затраты зависели не только от языковой модели, но и от того, как был устроен поиск.
Помимо задач Эрдёша и гипотез OEIS, AlphaProof Nexus помогла решить открытую задачу в алгебраической геометрии, улучшить оценку в выпуклой оптимизации и найти ошибки в формализации утверждений из научной литературы. Систему также применяют в исследованиях по теории графов и квантовой оптике.
Однако большая часть открытых задач Эрдёша осталась нерешённой. Успехи агента пока сосредоточены в областях с развитой библиотекой формализованных результатов, где сложное рассуждение можно разбить на подзадачи. Как и другие языковые модели, система может выдавать разные результаты при повторных запусках, а задачи, требующие создания обширной новой теории, ей не под силу.
