ИИ-система без дообучения доказала все 6 задач IMO 2026 в Lean

Исследователи из Case Western Reserve University (работа сделана во время стажировки в Amazon Web Services) показали, что готовая большая языковая модель без всякого дообучения может доказывать сложные теоремы и корректность программ, если правильно организовать вокруг неё работу. В качестве модели они взяли Anthropic Fable-5. Доказательства пишутся в системе Lean: это язык, где каждый шаг рассуждения проверяет небольшое «ядро», и обмануть его нельзя.

Система решила все шесть формализованных задач Международной математической олимпиады 2026 года. Она также прошла все задачи VERINA (набор по верифицированному программированию) и разобралась с условиями проверки из NTP4VC, промышленного набора по формальной верификации кода. Кроме того, она решает задачи из PutnamBench, набора формализованных задач университетской олимпиады Патнэма.

Каждый засчитанный результат — это либо доказательство, либо опровержение утверждения, и оба проверены ядром Lean.

Дерево агентов вместо серии перезапусков

Сложность в том, что Lean отвечает только на локальный вопрос: проходит ли конкретный шаг. Плохое разбиение задачи на части или недостающая лемма (вспомогательное утверждение) обнаруживаются через десятки шагов. К тому же модель ограничена окном контекста и бюджетом вычислений.

Авторы решают это рекурсивно. Главный агент запускает дочерних, и каждый ищет либо другую стратегию доказательства, либо нужную лемму. Детали устроены так:

• у каждого потомка свой чистый контекст и собственная копия проекта; • потомок может сам порождать потомков, а инструменты у всех одинаковые; • потомок может потратить десятки вызовов на одну лемму, а родителю вернёт только готовую лемму, контрпример или частичные находки; • результаты приходят родителю на следующем ходу, не дожидаясь остальных веток, поэтому ранняя находка может перенаправить поиск; • поиск заканчивается, когда принято первое подходящее доказательство.

По духу это похоже на поиск по дереву Монте-Карло, но решения принимает сама модель. Она читает содержимое ответов потомков и сама выбирает, какие ветки продолжать, менять или расширять. Счётчики посещений и усреднённые оценки не используются.

Ещё один инструмент — параллельная проба тактик. Агент запускает сразу несколько кандидатов на текущем состоянии доказательства. Работающий возвращается в контекст, а следы неудачных попыток отбрасываются, и контекст не засоряется.

Lean как масштабируемый сервис

Самые трудные доказательства потребовали десятков субагентов в одном запуске. Одной машине не хватало мощности Lean, поэтому проверку вынесли в отдельный сервис без состояния. Клиенты шлют исходный код Lean по JSON-RPC, а не ссылаются на локальные файлы. Любая готовая реплика с одинаковыми версиями Lean и Mathlib может обработать любой запрос.

Внутри каждой реплики пул рабочих процессов с заранее загруженной библиотекой Mathlib. Импорт занимает десятки секунд, поэтому процессы переиспользуют, и проверка на «тёплом» процессе идёт заметно быстрее. Реплики работают в Kubernetes, а их число автоматически подстраивается под нагрузку.

От читерства система защищена отдельно. Агент, редактирующий файл с доказательством, мог бы ослабить формулировку теоремы, оставить заглушку sorry или добавить аксиому. Поэтому всё до сигнатуры теоремы заморожено, а финальную проверку делает Lean Comparator: файл должен компилироваться без заглушек и использовать только разрешённые аксиомы. Отчёт самого агента об успехе в расчёт не берётся.

Новый экзамен: олимпиадный код в роли задач на верификацию

Старые тесты почти исчерпаны, а рукописные наборы по верификации кода невелики: в них сотни задач, и их можно запомнить или найти в обучающих данных. Поэтому авторы построили конвейер, который порождает задачи автоматически:

• агент-кодер пишет безопасные решения на Rust для задач в стиле LeetCode, где одна чистая функция над простыми данными (числа, списки, строки, деревья, связные списки); • решение проходит эталонные тесты, затем транслируется в исполняемую модель на Lean; • Rust и Lean прогоняют на одних и тех же входах, и принимаются только программы с полным совпадением выходов; • отдельный агент пишет спецификацию, то есть свойство, которое должно выполняться или нарушаться; • формулировку замораживают, и прувер доказывает либо опровергает её.

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

На выборке утверждений с 30-минутным лимитом на каждое система решает лишь часть. Для прувера, который почти исчерпал старые бенчмарки, задачи остаются далеки от насыщения. Их можно масштабировать вычислениями, использовать для сравнения других доказывателей и как награды в обучении с подкреплением на проверяемых наградах (RLVR). Тест на код ничего не «угадывает», а выдаёт проверяемый вердикт ядра. Мутации программ (небольшие правки правильного кода) дают дополнительные задачи с отрицательными метками, но в статье они не оцениваются.

Что это даёт инженерам

Главный практический вывод: без дообучения упор можно делать на обвязку. Изоляция контекстов, асинхронный поиск, параллельные пробы и эластичный сервис проверки позволяют обычной модели выжать из Lean результат, который раньше требовал специально обученных моделей вроде Goedel-Code-Prover. Тем, кто строит агентов для верификации кода, пригодится и схема с замороженной формулировкой плюс независимой финальной проверкой: она закрывает типовые способы обмана проверяющего.