Seed-Prover: Diepgaand en breed redeneren voor automatische stellingbewijzen

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

July 31, 2025

Auteurs: 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

Samenvatting

LLM's hebben sterke wiskundige redeneervaardigheden getoond door gebruik te maken van reinforcement learning met lange ketens van gedachten, maar ze blijven moeite houden met het bewijzen van stellingen vanwege het ontbreken van duidelijke supervisiesignalen bij het uitsluitend gebruik van natuurlijke taal. Domeinspecifieke talen zoals Lean bieden duidelijke supervisie via formele verificatie van bewijzen, waardoor effectieve training door middel van reinforcement learning mogelijk wordt. In dit werk stellen we Seed-Prover voor, een lemma-stijl volledig-bewijs redeneermodel. Seed-Prover kan zijn bewijs iteratief verfijnen op basis van Lean-feedback, bewezen lemma's en zelf-samenvatting. Om IMO-niveau wedstrijdproblemen op te lossen, ontwerpen we drie testtijd inferentiestrategieën die zowel diep als breed redeneren mogelijk maken. Seed-Prover bewijst 78,1% van de geformaliseerde eerdere IMO-problemen, verzadigt MiniF2F en behaalt meer dan 50% op PutnamBench, wat een aanzienlijke verbetering is ten opzichte van de vorige state-of-the-art. Om het gebrek aan geometrie-ondersteuning in Lean aan te pakken, introduceren we een geometrie-redeneermachine Seed-Geometry, die eerdere formele geometrie-machines overtreft. We gebruiken deze twee systemen om deel te nemen aan de IMO 2025 en volledig 5 van de 6 problemen te bewijzen. Dit werk vertegenwoordigt een significante vooruitgang in geautomatiseerd wiskundig redeneren, en demonstreert de effectiviteit van formele verificatie met lange ketens van gedachten.

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.