Seed-Prover: Глубокий и широкий анализ для автоматического доказательства теорем

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

July 31, 2025

Авторы: Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, Thomas Hanwen Zhu

cs.AI

Аннотация

LLM продемонстрировали сильные способности к математическому рассуждению, используя обучение с подкреплением с длинными цепочками рассуждений, однако они продолжают испытывать трудности с доказательством теорем из-за отсутствия четких сигналов контроля при использовании исключительно естественного языка. Специализированные предметно-ориентированные языки, такие как Lean, обеспечивают четкий контроль через формальную верификацию доказательств, что позволяет эффективно обучать модели с помощью обучения с подкреплением. В данной работе мы предлагаем Seed-Prover, модель рассуждений в стиле лемм для полного доказательства. Seed-Prover может итеративно уточнять свое доказательство на основе обратной связи от Lean, доказанных лемм и самосуммаризации. Для решения задач уровня Международной математической олимпиады (IMO) мы разработали три стратегии вывода на этапе тестирования, которые позволяют проводить как глубокие, так и широкие рассуждения. Seed-Prover доказывает 78,1% формализованных задач прошлых IMO, достигает насыщения на MiniF2F и показывает результат свыше 50% на PutnamBench, значительно превосходя предыдущие достижения. Для решения проблемы отсутствия поддержки геометрии в Lean мы представляем механизм геометрических рассуждений Seed-Geometry, который превосходит предыдущие формальные геометрические движки. Мы используем эти две системы для участия в IMO 2025 и полностью доказываем 5 из 6 задач. Данная работа представляет собой значительный шаг вперед в области автоматизированного математического рассуждения, демонстрируя эффективность формальной верификации в сочетании с длинными цепочками рассуждений.

English

LLMs have demonstrated strong mathematical reasoning abilities by leveraging reinforcement learning with long chain-of-thought, yet they continue to struggle with theorem proving due to the lack of clear supervision signals when solely using natural language. Dedicated domain-specific languages like Lean provide clear supervision via formal verification of proofs, enabling effective training through reinforcement learning. In this work, we propose Seed-Prover, a lemma-style whole-proof reasoning model. Seed-Prover can iteratively refine its proof based on Lean feedback, proved lemmas, and self-summarization. To solve IMO-level contest problems, we design three test-time inference strategies that enable both deep and broad reasoning. Seed-Prover proves 78.1% of formalized past IMO problems, saturates MiniF2F, and achieves over 50\% on PutnamBench, outperforming the previous state-of-the-art by a large margin. To address the lack of geometry support in Lean, we introduce a geometry reasoning engine Seed-Geometry, which outperforms previous formal geometry engines. We use these two systems to participate in IMO 2025 and fully prove 5 out of 6 problems. This work represents a significant advancement in automated mathematical reasoning, demonstrating the effectiveness of formal verification with long chain-of-thought reasoning.