ИИ прорвался на Международную математическую олимпиаду: AlphaProof получила серебро — впервые в истории

На Международной математической олимпиаде 2024 года произошёл необычный случай: среди решений, набравших баллы на уровне серебряной медали, оказалось не человеческое решение, а работа, созданная искусственным интеллектом. Ранее ни одна ИИ-система не демонстрировала на олимпиаде результат, сопоставимый с уровнем сильных школьников, которые традиционно доминируют в подобных соревнованиях.

Эту систему назвали AlphaProof — разработка Google DeepMind, предназначенная для решения математических задач в форме строгих формальных доказательств. Сам по себе её выход на уровень международной олимпиады уже впечатлял, но куда важнее способность программы находить собственные промахи и исправлять их. Обычные большие языковые модели действительно могут решать уравнения и логические задачи, однако их выводы нередко содержат тонкие ошибки: формулировка выглядит убедительно, но при проверке рассыпается.

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

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

Самый масштабный этап начался позже, когда системе предложили «домашнее задание» из 80 миллионов формализованных задач. Здесь использовали обучение с подкреплением — метод, при котором модель поощряется за успешные доказательства. Постепенно AlphaProof научилась вырабатывать собственные стратегии поиска решения, опираясь не на копирование человеческих примеров, а на накопленный опыт. Она анализировала собственные попытки, отбрасывала неудачные подходы и искала новые маршруты рассуждений.

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

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