Seed-Prover: Tiefgreifende und umfassende Argumentation für automatisches Theorembeweisen

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

July 31, 2025

papers.authors: 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

papers.abstract

LLMs haben durch den Einsatz von Reinforcement Learning mit langen Gedankenketten starke mathematische Fähigkeiten bewiesen, kämpfen jedoch weiterhin mit dem Beweisen von Theoremen, da bei der alleinigen Verwendung natürlicher Sprache klare Überwachungssignale fehlen. Spezielle domänenspezifische Sprachen wie Lean bieten klare Überwachung durch formale Verifizierung von Beweisen, was ein effektives Training durch Reinforcement Learning ermöglicht. In dieser Arbeit schlagen wir Seed-Prover vor, ein Lemma-basiertes Ganzbeweis-Modell. Seed-Prover kann seinen Beweis iterativ auf der Grundlage von Lean-Feedback, bewiesenen Lemmata und Selbstzusammenfassung verfeinern. Um IMO-Level-Wettbewerbsprobleme zu lösen, entwerfen wir drei Testzeit-Inferenzstrategien, die sowohl tiefes als auch breites Denken ermöglichen. Seed-Prover beweist 78,1 % der formalisierten vergangenen IMO-Probleme, sättigt MiniF2F und erreicht über 50 % auf PutnamBench, womit es den bisherigen Stand der Technik deutlich übertrifft. Um den Mangel an Geometrieunterstützung in Lean zu beheben, führen wir eine Geometrie-Engine namens Seed-Geometry ein, die bisherige formale Geometrie-Engines übertrifft. Wir verwenden diese beiden Systeme, um an der IMO 2025 teilzunehmen und 5 von 6 Problemen vollständig zu beweisen. Diese Arbeit stellt einen bedeutenden Fortschritt im automatisierten mathematischen Denken dar und demonstriert die Wirksamkeit der formalen Verifizierung mit langen Gedankenketten.

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.