На Международной математической олимпиаде (IMO) 2024 года один участник показал настолько выдающиеся результаты, что заслуживал бы серебряной медали, если бы не одно обстоятельство: этим участником была система искусственного интеллекта. Впервые в истории соревнований ИИ достиг уровня, позволяющего претендовать на медаль.
В статье, опубликованной в журнале Nature, исследователи подробно описывают технологию, стоящую за этим впечатляющим достижением.
Знакомьтесь: AlphaProof
AlphaProof — это сложная программа, разработанная Google DeepMind, которая учится решать сложные математические задачи. Впечатляющие результаты на IMO — это одно, но что действительно выделяет AlphaProof, так это её способность находить и исправлять ошибки.
В то время как большие языковые модели (LLMs) могут решать математические задачи, они не всегда могут гарантировать точность своих решений. В них могут быть скрытые недостатки в рассуждениях.
AlphaProof отличается тем, что её ответы всегда на 100% точны. Это связано с тем, что она использует специализированную программную среду под названием Lean (первоначально разработанную Microsoft Research), которая действует как строгий учитель, проверяющий каждый логический шаг. Это означает, что компьютер сам проверяет ответы, поэтому его выводы заслуживают доверия.
Трёхэтапное обучение AlphaProof
Для того чтобы обучить эту мощную систему рассуждать на элитном уровне, потребовалось три этапа обучения.
1. Сначала исследователи предоставили AlphaProof около 300 миллиардов токенов общего кода и математических текстов, чтобы дать ей широкое понимание таких концепций, как логика, математический язык и структура программирования.
2. Затем системе были предложены 300 000 математических доказательств, написанных экспертами и уже находящихся в среде Lean.
3. На заключительном этапе система научилась решать задачи самостоятельно. Ей было предложено решить 80 миллионов формальных математических задач. Используя обучение с подкреплением (RL), основанное на методе проб и ошибок, AlphaProof вознаграждалась за каждое успешное доказательство. Решая математические задачи в таком масштабе, система обучила себя новым и сложным стратегиям рассуждений, выходящим за рамки копирования человеческих примеров.
Для решения самых сложных задач AlphaProof использовала технику, разработанную исследователями, под названием Test-Time RL (TTRL), которая создаёт и решает миллионы упрощённых версий целевой задачи, пока не найдёт решение.
«Наша работа демонстрирует, что масштабное обучение на основе практического опыта позволяет создавать агентов со сложными стратегиями математического мышления, открывая путь для надёжного инструмента искусственного интеллекта в решении сложных математических задач», — написали исследователи в своей статье.
Помимо решения сложных математических задач, AlphaProof может быть использована математиками для проверки их работ и помощи в разработке новых теорий.