EasyProver доказала 669 из 672 задач PutnamBench без дообучения модели
В статье представлена EasyProver, система для доказательства теорем в Lean, построенная из рекурсивных агентов с изолированными контекстами, асинхронного поиска, параллельного опробования тактик и эластичного сервиса проверки (elaboration). В основе, готовая передовая модель без какого-либо дополнительного обучения.
Результаты на существующих бенчмарках близки к максимуму: EasyProver доказывает 669 из 672 задач PutnamBench и все шесть формализаций задач IMO 2026. На NTP4VC она разбирается с 597 из 600 условий верификации, а на VERINA, со всеми 189 задачами; в двух последних случаях задача считается решённой, если найдено доказательство или опровержение.
Поскольку эти бенчмарки близки к насыщению, авторы предлагают новый, Aegis. Это конвейер, который превращает задачи спортивного программирования в заметно более трудные задачи верификации над реальными реализациями. Конвейер пишет безопасные решения на Rust, переводит их в Lean с помощью Aeneas, генерирует спецификации и помечает каждое зафиксированное утверждение доказательством или опровержением, проверенным ядром Lean. На выходе, 2045 программных пар Rust, Lean, прошедших дифференциальную валидацию, и 11 533 кандидата в спецификации.
В отличие от написанных вручную бенчмарков, задачи Aegis несут обязательства уровня реализации: арифметика с фиксированной разрядностью, явные отказы, сгенерированные циклы, приведения типов и функционализованная мутация данных. На стратифицированной выборке из 2000 утверждений EasyProver доказывает 1054 (52,7%) при лимите 30 минут на утверждение. Авторы отмечают, что те же задачи годятся для сравнения других систем доказательства и в качестве наград при обучении с подкреплением.
Ключевые факты
- EasyProver, система доказательства теорем в Lean на готовой передовой модели без дообучения: рекурсивные агенты с изолированными контекстами, асинхронный поиск, параллельный подбор тактик.
- PutnamBench: 669 из 672 задач и все шесть формализаций IMO 2026; NTP4VC: 597 из 600 условий; VERINA: все 189 задач (доказательством или опровержением).
- Aegis превращает задачи спортивного программирования в верификацию реального кода: Rust переводится в Lean через Aeneas, получено 2045 проверенных пар и 11 533 кандидата в спецификации.
- На выборке из 2000 утверждений Aegis EasyProver доказывает 1054 (52,7%) при лимите 30 минут на утверждение.
Почему это важно
Авторы утверждают, что привычные бенчмарки по доказательству теорем в Lean почти исчерпаны: система на готовой модели без дообучения решает почти все задачи PutnamBench, NTP4VC и VERINA. Новый бенчмарк Aegis переносит оценку ближе к практике, к проверке реального кода на Rust с требованиями вроде арифметики фиксированной разрядности и приведений типов. Результат 52,7% на нём показывает, что запас для роста ещё остаётся.
Кому это важно
Исследователям автоматического доказательства теорем и формальной верификации программ, а также разработчикам систем, где корректность кода нужно доказывать, а не только тестировать. Бенчмарк Aegis пригодится тем, кто сравнивает системы доказательства или обучает их с подкреплением: по заявлению авторов, задачи подходят и как оценочный набор, и как источник наград.
Как это применить
Из аннотации следует, что подход не требует обучения собственной модели: берётся готовая передовая модель, а вся работа лежит на агентной обвязке и инфраструктуре проверки. Задачи Aegis можно использовать для сравнения других систем и как награды в обучении с подкреплением. Практические детали запуска, включая использованную модель, в аннотации не названы.
Можно ли доверять
Это препринт, и приведённые цифры, собственные заявления авторов; в аннотации не названа использованная модель и нет сравнения с результатами других систем доказательства. Не упомянут и выпуск кода, бенчмарка или набора данных, так что независимо проверить результаты по одной аннотации нельзя. Доказательства и опровержения в Aegis проверяются ядром Lean, что снижает риск ошибок в самих метках.
Риски и подводные камни
Оценка на Aegis сделана на стратифицированной выборке из 2000 утверждений, а не на всём наборе из 11 533 кандидатов в спецификации; как строилась выборка, в аннотации не раскрыто. Показатель 52,7% получен при лимите 30 минут на утверждение, при другом бюджете цифра может отличаться. Для NTP4VC и VERINA не указано, сколько задач решено доказательством, а сколько опровержением. Стоимость вычислений и используемое оборудование не названы.