Как ИИ-агенты решают задачи международной олимпиады по математике

В последние пару лет большие рассуждающие модели (LRM) заметно подтянулись в олимпиадной математике. На задачах уровня AIME (Американский Инновационный Математический Экзамен) им часто хватает одного длинного «прогона» рассуждений: модель пишет цепочку мыслей, проверяет ответ, иногда делает пару попыток — и падает. Но у уровня IMO (Международная Математическая Олимпиада) другая природа сложности. Там решение редко укладывается в один прямой сценарий: нужно пробовать идеи, откатываться, фиксировать найденные промежуточные факты, а потом собирать доказательство из кирпичиков. И вот здесь модели упираются в довольно прозаичную стену — ограничение контекста. Даже 64k или 128k токенов для некоторых доказательств оказываются тесными, если рассуждение разрастается, а промежуточные находки теряются в «шуме» черновика.

Авторы работы Long-horizon Reasoning Agent for Olympiad-Level Mathematical Problem Solving предлагают смотреть на задачу иначе: не пытаться «впихнуть» всё решение в один прогон, а создать агента, который умеет работать долго и поэтапно, как человек.

Идея: рассуждать итеративно и работать не с текстом, а с леммами

Агент Intern-S1-MO работает в несколько раундов. В каждом раунде он не обязан «добить» задачу до конца. Напротив, ключевой артефакт раунда — аккуратно сформулированные промежуточные результаты: леммы, полезные наблюдения, частичные доказательства. Их затем можно переиспользовать.

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

Получается, что память системы — это не гигантский лог рассуждений, а структурированная «библиотека лемм». Такой формат напоминает человека: мы тоже стараемся удержать в голове не все пробные попытки, а то, что действительно доказано и пригодится дальше.

Как удержать качество

В работе много внимания уделено верификации. Леммы проверяются несколькими независимыми прогонами проверяющего агента, а итоговая уверенность агрегируется — так снижается риск, что случайная убедительная формулировка проскочит как «правда». Отдельно проверяется уже финальное доказательство: специальный верификатор процесса ищет логические дыры по шагам и возвращает текстовый фидбек, после чего решение можно итеративно поправлять.

На практике это закрывает типичную проблему LRM: когда бюджет кончается, модель часто делает преждевременный ответ. Здесь же у неё есть «безопасный режим» — фиксировать прогресс в виде лемм, даже если полного решения пока нет.

Обучение под длинные сценарии

Одна архитектура не гарантирует, что модель действительно научится вести длинные итеративные рассуждения. Поэтому авторы добавляют RL-фреймворк OREAL-H, который подстраивает обучение под иерархический процесс: есть высокоуровневые действия (например, переход к извлечению лемм или к проверке), есть генерация текста, есть промежуточные сигналы от верификатора и финальная награда за правильный ответ.

Граф зависимостей лемм «раздаёт ценность» тем промежуточным утверждениям, которые реально привели к успешному решению. Это похоже на попытку честно наградить не только финальный ответ, но и те этапы рассуждений, которые сделали ответ возможным.

Что получилось на бенчмарках и в «боевых» условиях

По результатам экспериментов система показывает сильные метрики на задачах разного типа. На AIME2025 и HMMT2025 заявлены 96.6% и 95% pass@1. На негеометрических задачах IMO2025 — 26/35 баллов, что сопоставимо с уровнем серебряных призёров. На CNMO2025 — 232.4/260 (также без геометрии). И особенно показательно — участие в CMO2025, где, по проверке экспертов, агент набрал 102/126, то есть уверенно выше «золотого» порога.

С практической точки зрения здесь важно не только «сколько баллов», но и сама демонстрация механизма: система умеет тратить большой инференс-бюджет осмысленно, не превращая его в бесконечный поток токенов. Авторы прямо пишут про масштаб порядка 512K токенов на задачу, но подчёркивают, что ключ не в наращивании контекста, а в том, как хранить и переиспользовать вест прогресс.

Почему это важно

Исследование хорошо подсвечивает границу между тем, как «решить задачу одним рывком» и «решить задачу серией осмысленных шагов, которые можно проверить и сохранить». На олимпиадном уровне важно второе. Подход с леммами выглядит как компромисс между чисто текстовым рассуждением и тяжёлым формальным доказательством: он сохраняет удобство естественного языка, но всё же позволяет эффективнее работать с памятью и контролировать ошибки.

Ограничения тоже читаются между строк. Во‑первых, сильная зависимость от качества верификатора: если проверка ошибается систематически, память начнёт копить мусор. Во‑вторых, геометрию авторы отдельно исключают в ряде оценок — это остаётся сложной задачей. Но как архитектурная идея для долговременного рассуждения это выглядит убедительным шагом вперёд.