Простой агент h1 достиг лучших результатов в доказательстве теорем на Lean 4
В статье «A Taste of the Bitter Lesson in Automated Theorem Proving» поставлен вопрос в духе «горького урока»: может ли простой агентный цикл, который наращивает вычисления на этапе решения, сравняться с рабочими процессами, придуманными людьми. Исходное наблюдение авторов таково: в неформальной математике прогресс шёл в основном за счёт масштабирования цепочек рассуждений и агентного поведения передовых языковых моделей, а формальное доказательство теорем всё больше опирается на человеческие схемы вокруг моделей: планирование, декомпозицию задач и оркестровку специализированных доказателей. По мнению авторов, вопрос важен, потому что формальная верификация должна поспевать за передовыми моделями, которые выдают исследовательскую математику, но новые схемы редко дают на него ответ: их выигрыш часто смешан с эффектом более сильной модели или большего объёма вычислений.
Для проверки авторы предлагают h1, простую обвязку (harness), которая даёт модели эффективный интерфейс к системе Lean 4 и удерживает её в работе за счёт обратной связи от верификатора и самоанализа (self-reflection), не навязывая ни декомпозицию, ни структуру поиска.
Результаты, о которых сообщают авторы: h1 достигает лучших известных результатов на бенчмарках PutnamBench, FATE-X и FormalConjectures100-Solved, закрывает восемь открытых задач из набора FormalConjectures, а при сопоставимых моделях сравнивается со специализированными системами вроде Goedel-Architect и AlphaProof Nexus или превосходит их. Неожиданным авторы называют то, что одной попытки (pass@1) нередко хватает, чтобы решать открытые задачи.
Абляции и сравнения при одинаковых моделях с Claude Code и AxProverBase приводят к уточнению: простоты самой по себе недостаточно. Стоимость и долю решённых задач во многом определяет эффективный интерфейс к Lean. Вывод авторов: прежде чем предписывать рабочие процессы, в будущих работах стоит оценивать передовые модели с эффективной обратной связью от исполнения, иначе возможны горькие уроки.
Ключевые факты
- h1, простая обвязка: модель получает эффективный интерфейс к Lean 4 и работает на обратной связи верификатора и самоанализе, без заданной декомпозиции и структуры поиска.
- По словам авторов, h1 достигает лучших известных результатов на PutnamBench, FATE-X и FormalConjectures100-Solved и закрывает восемь открытых задач из FormalConjectures.
- При сопоставимых моделях h1 сравнивается со специализированными системами Goedel-Architect и AlphaProof Nexus или превосходит их.
- Одной попытки (pass@1) нередко достаточно, чтобы решать открытые задачи.
- Простоты мало: по абляциям и сравнениям с Claude Code и AxProverBase, стоимость и долю решённых задач во многом определяет эффективность интерфейса к Lean.
Почему это важно
Работа проверяет, нужны ли в формальном доказательстве теорем сложные схемы, придуманные людьми (планирование, декомпозиция, оркестровка специализированных доказателей), или достаточно простого агентного цикла с большим объёмом вычислений на этапе решения. Авторы подчёркивают, что формальная верификация должна поспевать за передовыми моделями, которые выдают исследовательскую математику. Если простая обвязка действительно догоняет специализированные системы, это меняет представление о том, где искать прогресс.
Кому это важно
Исследователям автоматического доказательства теорем и формальной верификации в Lean 4, разработчикам агентных систем для доказательств и тем, кто сравнивает рабочие процессы вокруг моделей: авторы утверждают, что выигрыш новых схем часто смешан с эффектом более сильной модели или большего объёма вычислений.
Как это применить
Практический совет авторов: перед тем как строить сложный рабочий процесс, оценить передовую модель с эффективной обратной связью от исполнения. Ключевой элемент, по их результатам, эффективный интерфейс к Lean, он во многом определяет стоимость и долю решённых задач. В описании не упомянут выпуск кода или обвязки, поэтому воспроизвести h1 по этим данным нельзя.
Можно ли доверять
Это препринт, и все утверждения принадлежат самим авторам. В описании не названы авторы и организации, не указаны базовые модели, числовые результаты, стоимость и отрыв от прежних рекордов, а также не сказано, какие именно восемь задач закрыты и проверены ли решения независимо. Сильные заявления (лучшие известные результаты, превосходство над специализированными системами) стоит сверять с полным текстом статьи.
Риски и подводные камни
Вывод «простой цикл не хуже сложных схем» подкреплён сравнением при сопоставимых моделях, но по описанию нельзя оценить масштаб преимущества. Сами авторы оговаривают, что простоты недостаточно: без эффективного интерфейса к Lean стоимость и доля решённых задач ухудшаются. Заявление о том, что pass@1 нередко решает открытые задачи, нужно читать с учётом того, что подробности по восьми задачам не приведены.
«Поэтому мы рекомендуем в будущих работах оценивать передовые модели с эффективной обратной связью от исполнения, прежде чем предписывать рабочие процессы, иначе риск, горькие уроки.»
— авторы статьи «A Taste of the Bitter Lesson in Automated Theorem Proving»