ИИ впервые стал призером международной олимпиады по математике

Новый ИИ AlphaProof научился решать олимпиадные задачи, проверяя каждый шаг рассуждений формальной логикой — это первый такой успех в истории.

Уникальность модели в том, что она не только решает, но и сама проверяет свои задачи

Источник: hsbi.hse.ru

«Серебро» олимпиады досталось сложной программе AlphaProof, разработанной Google DeepMind. Модель изначально была создана для решения математических задач в форме строгих формальных доказательств.

Главная особенность AlphaProof — способность находить и исправлять ошибки. В то время как большие языковые модели (LLM) могут решать математические задачи, они часто не могут гарантировать точность своих решений — в их рассуждениях могут скрываться незаметные изъяны.

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

В систему загрузили не только тексты и данные, но и 300 тысяч готовых доказательств от лучших математиков мира

Источник: SecurityLab

Система создавалась в три этапа. Сначала AlphaProof обучали на массиве примерно из 300 млрд токенов, включавшем программный код, учебные материалы и научные тексты. Это дало модели базовое понимание логических структур, формального языка и принципов построения доказательств. Затем исследователи загрузили в систему 300 тыс. готовых доказательств, заранее оформленных в Lean. Модель переняла стиль мышления профессиональных математиков и получила ориентир для дальнейшего обучения.

На третьем этапе программе дали «домашнюю работу» из 80 миллионов формализованных задач. Здесь был использован метод, при котором модель поощрялась за успешное решение.

На третьем этапе модели дали дали задание — решить 80 млн математических задач

Источник: Freepik

Для самых сложных задач команда добавила дополнительный инструмент — Test-Time Reinforcement Learning (TTRL). Эта схема создает множество упрощенных версий исходной задачи, которые нужно решать одну за другой, собирая полезные логические шаблоны. Обучаясь таким образом, AlphaProof перенесла отработанные стратегии на исходное, гораздо более трудное задание. Авторы исследования отмечают, что потенциал модели не ограничивается олимпиадами. Они надеются, что AlphaProof поможет в проверке математических гипотез и разработке новых теоретических идей.

Ранее Наука Mail рассказала о том, как нейросети обучаются здравомыслию и интуиции.