25 июля 2024 года Google DeepMind сообщила, что связка AlphaProof и AlphaGeometry 2 набрала 28 из 42 баллов на задачах IMO 2024 — это соответствовало верхней границе серебряной категории по правилам того года. Но формулировка «ИИ взял серебро на IMO» легко вводит в заблуждение: задачи сначала вручную перевели в формальные языки, а решения оценивали приглашённые математики по правилам олимпиады; некоторые прогоны заняли до трёх дней. В этом разборе мы держим исторический фокус именно на результате 2024 года, а технические детали дополняем более поздними публикациями Nature и JMLR, где методология AlphaProof и AlphaGeometry 2 была раскрыта уже после анонса.
Коротко
- На IMO 2024 DeepMind опубликовала решения задач P1, P2, P4 и P6; суммарный результат составил 28/42, а золотой порог в 2024 году начинался с 29 баллов.
- Это была не одна универсальная LLM, а связка двух специализированных формальных систем: AlphaProof для негеометрических задач и AlphaGeometry 2 для геометрии.
- Ключевой инженерный ход — перевести задачу в проверяемую среду: Lean для AlphaProof и специальный язык геометрии для AlphaGeometry 2.
- Главное ограничение результата 2024 года: система не была end-to-end. Формализацию делали люди, а вычисления занимали от минут до нескольких дней.
- Поздние статьи 2025–2026 годов показывают, что за результатом стояли RL, search, auto-formalization и нейро-символьный пайплайн, а не просто «длинные рассуждения» в естественном языке.
Контекст
International Mathematical Olympiad (IMO) — это шесть задач, два дня экзамена и по 4,5 часа на каждую сессию; каждая задача оценивается от 0 до 7, максимум — 42 балла. Для ИИ это неудобный бенчмарк сразу по двум причинам. Во-первых, формулировки и решения живут в естественном языке, где легко получить правдоподобное, но неверное рассуждение. Во-вторых, на IMO важен не только ответ, но и полное доказательство.
Здесь важно помнить, что июльский результат 2024 года не появился из пустоты. Уже 17 января 2024 года DeepMind и Google Research опубликовали в Nature работу об AlphaGeometry. Там система решила 25 из 30 задач набора IMO-AG-30, тогда как предыдущий лучший автоматический метод решал 10; авторы также показывали, что это почти уровень среднего золотого медалиста на этом узком геометрическом наборе. Основа AlphaGeometry — нейро-символьная схема: языковая модель предлагает вспомогательные построения, а символьный движок делает строгие выводы.
Однако AlphaGeometry 2024 года была системой для геометрии, а не для всей олимпиадной математики. Кроме того, её исходная предметная «языковая» область покрывала не все типы IMO-геометрии. Поэтому результат июля 2024 года оказался важен не только числом баллов, но и тем, что DeepMind впервые собрала составной пайплайн: отдельный формальный доказчик для алгебры и теории чисел плюс улучшенный геометрический решатель.
Метод
AlphaProof: формальные доказательства в Lean
В анонсе от 25 июля 2024 года DeepMind описывала AlphaProof как систему, которая доказывает математические утверждения в формальном языке Lean и сочетает предобученную языковую модель с reinforcement learning в духе AlphaZero. Идея здесь принципиальная: не просить модель «объяснить решение красиво», а заставить её действовать в среде, где каждый шаг либо проходит формальную проверку, либо нет.
Позже, в статье Nature, опубликованной 12 ноября 2025 года, эта схема была раскрыта подробнее. AlphaProof работает как агент в среде Lean: видит текущее состояние доказательства, предлагает тактики, а дерево поиска разворачивает наиболее перспективные ветви. Для сложных задач система использует не только обычное расширение search budget, но и test-time RL: вокруг конкретной целевой задачи генерируются связанные варианты, и агент дообучается на них прямо во время решения. Для практиков это важная деталь: здесь «больше думать» означает не метафорическое chain-of-thought, а дополнительное обучение и поиск в проверяемой формальной среде.
AlphaGeometry 2: нейро-символьная геометрия второго поколения
AlphaGeometry 2 решает другую подзадачу. Как и первая версия, это нейро-символьная система, но в июльском посте 2024 года DeepMind уже подчёркивала три улучшения: языковая модель на базе Gemini, обучение с нуля на порядке большем объёме синтетических данных и символьный движок, который работает на два порядка быстрее предшественника. Там же было сказано о новом механизме обмена знаниями между деревьями поиска.
Подробности появились позже, в статье JMLR 2025 года. Из неё следует, что AG2 расширила язык геометрии так, чтобы выражать более сложные типы задач: движения объектов, линейные уравнения углов, расстояний и отношений, а также часть неконструктивных постановок. Авторы также формализуют новый алгоритм поиска Shared Knowledge Ensemble of Search Trees (SKEST): несколько деревьев поиска делятся полезными промежуточными находками вместо полностью изолированной работы.
Как выглядел реальный прогон на IMO 2024
Самый важный методологический нюанс: в 2024 году система не работала напрямую от исходного текста задачи к финальному естественноязыковому доказательству. DeepMind прямо пишет, что сначала задачи вручную переводили в формальный математический язык. Страница с опубликованными решениями уточняет ещё сильнее: формулировки задач были вручную формализованы в Lean, а комментарии в опубликованном коде были добавлены вручную для пояснения хода решения.
Иными словами, связка выглядела так: человек переводит задачу в формальный вид; AlphaProof пытается решить негеометрические задачи в Lean; AlphaGeometry 2 решает геометрическую задачу в собственной формальной среде; затем результат проверяется формально и только после этого интерпретируется как решение задачи IMO. Это делает систему менее «магической», но более инженерно понятной: надёжность здесь рождается из верификации, а не из доверия к естественноязычному объяснению.
Результаты
На странице с решениями DeepMind опубликовала четыре доказательства: P1, P2, P4 и P6. Две оставшиеся задачи — P3 и P5 — решены не были. В терминах официальной схемы оценивания IMO это означает четыре полных решения по 7 баллов каждое.
| Задача IMO 2024 | Статус | Система | Баллы | Примечание |
|---|---|---|---|---|
| P1 | Решена | AlphaProof | 7 | Опубликовано формальное решение |
| P2 | Решена | AlphaProof | 7 | Опубликовано формальное решение |
| P3 | Не решена | — | 0 | Решение не опубликовано |
| P4 | Решена | AlphaGeometry 2 | 7 | Единственная решённая геометрическая задача |
| P5 | Не решена | — | 0 | Решение не опубликовано |
| P6 | Решена | AlphaProof | 7 | Опубликовано формальное решение |
| Итого | 4 из 6 | AlphaProof + AG2 | 28/42 | Эквивалент верхней границе серебряной категории 2024 года |
По официальной таблице результатов IMO 2024 золотой порог начинался с 29 баллов, серебряный — с 22, бронзовый — с 16; в соревновании участвовали 609 человек, из них 58 набрали золото. Поэтому 28 баллов действительно попадали в серебряный диапазон и находились в одном балле от золотого порога.
Есть и ещё один слой результатов — уже не соревновательный, а ретроспективно-исследовательский. Более поздняя статья JMLR 2025 года и соответствующий arXiv-препринт сообщают, что AlphaGeometry 2 решает 42 из 50 геометрических задач IMO 2000–2024, то есть 84%, а покрытие языка геометрии выросло с 66% до 88%. Эти цифры полезны для понимания, почему AG2 вообще была способна вытащить P4, но их нельзя путать с собственно результатом IMO 2024: это отдельная поздняя оценка на историческом корпусе.
Интерпретация
Фактический смысл результата 2024 года в том, что DeepMind показала рабочий путь к олимпиадной математике через формальные среды и проверяемый поиск. В статье Nature об AlphaProof авторы прямо формулируют это как первое, по их знанию, достижение medal-level performance для ИИ на IMO. Существенно не только число 28/42, но и то, что три негеометрические задачи были решены формальным доказчиком, а не обычной LLM с непроверяемым текстовым рассуждением.
Наш комментарий
На наш взгляд, этот кейс лучше читать не как историю про «модель научилась думать как олимпиадник», а как историю про правильный выбор среды. AlphaProof силён не потому, что красиво рассуждает в естественном языке, а потому, что действует в Lean, где каждая тактика может быть подтверждена или отвергнута. AlphaGeometry 2 сильна не потому, что «понимает картинку», а потому, что опирается на узкий формальный язык геометрии, символьный движок и специализированный search.
Отсюда и более широкий вывод для практиков: в задачах, где цена ошибки высока, одна только fluent-генерация редко достаточно надёжна. Связка «модель + среда проверки + дополнительный поиск/обучение во время решения» выглядит куда более реалистичной инженерной траекторией. В этом смысле AlphaProof — ранний и очень сильный пример того, что позже стали обсуждать как отдельную ось масштабирования через вычисления во время ответа.
Ограничения и критика
- Это не официальная медаль IMO. В 2024 году решения DeepMind оценивали приглашённые математики по правилам IMO. В посте DeepMind о результате 2025 года отдельно подчёркивается, что именно тогда результаты модели были официально проверены и сертифицированы координаторами IMO. Из сопоставления этих источников следует, что результат 2024 года был эквивалентен серебру по баллам, но не являлся официальным награждением IMO.
- Не end-to-end. В 2024 году задачи вручную переводили в Lean и в язык AlphaGeometry. Это означает, что барьер «понять олимпиадную постановку на естественном языке» тогда ещё не был снят.
- Не сопоставимо с человеческим лимитом по времени. Участники IMO пишут две сессии по 4,5 часа, тогда как DeepMind прямо указывает, что система решила одну задачу за минуты, а другие — за срок до трёх дней.
- AG2 покрывает не всю геометрию. По данным JMLR 2025 года, даже после расширения языка остаются классы задач, которые система не покрывает полностью: среди них 3D-геометрия, неравенства, нелинейные уравнения и постановки с переменным числом точек.
- Детали AlphaProof стали публичными только позже. В самом анонсе июля 2024 года DeepMind дала лишь обзор метода. Полноценная статья Nature с техническими деталями AlphaProof вышла 12 ноября 2025 года, поэтому ранние обсуждения часто опирались на неполную картину.
Итог
Если убрать заголовочный шум, результат AlphaProof и AlphaGeometry 2 на IMO 2024 означает следующее: формально проверяемые ИИ-системы уже могут решать часть задач элитного олимпиадного уровня, но пока делают это через узкие формальные представления, разбиение по доменам и большой вычислительный бюджет. Это серьёзный исследовательский шаг, но не доказательство того, что одна универсальная модель уже «умеет IMO» в человеческом смысле слова.
Источники
- AI achieves silver-medal standard solving International Mathematical Olympiad problems — Google DeepMind
- Results — International Mathematical Olympiad
- What is IMO? — International Mathematical Olympiad
- IMO 2024 Problems — International Mathematical Olympiad
- IMO 2024 Solutions — Google DeepMind
- Solving olympiad geometry without human demonstrations — Nature
- Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2 — Journal of Machine Learning Research
- Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2 — arXiv
- Olympiad-level formal mathematical reasoning with reinforcement learning — Nature
- Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad — Google DeepMind
FAQ
Это было официальное серебро IMO?
Нет, корректнее говорить о результате, эквивалентном серебряной категории по баллам IMO 2024. В 2024 году решения DeepMind оценивали приглашённые математики по правилам олимпиады, а не официальная система награждения участников.
Какие задачи решила система?
DeepMind опубликовала решения P1, P2, P4 и P6. P4 решала AlphaGeometry 2, остальные три — AlphaProof.
Чем AlphaProof отличается от обычной LLM с chain-of-thought?
AlphaProof работает в формальной среде Lean, где шаги доказательства проверяются машинно. Это не просто генерация объяснения, а поиск последовательности тактик с RL и деревом поиска.
Почему понадобилась отдельная система для геометрии?
Потому что олимпиадная геометрия требует специальных представлений: диаграмм, вспомогательных построений, узкого формального языка и символьных правил вывода. Общий доказчик и геометрический решатель здесь решают разные подзадачи.