Seed-Prover : Raisonnement approfondi et étendu pour la démonstration automatique de théorèmes

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

Les LLM ont démontré de solides capacités de raisonnement mathématique en exploitant l'apprentissage par renforcement avec des chaînes de pensée longues, mais ils continuent de rencontrer des difficultés dans la démonstration de théorèmes en raison du manque de signaux de supervision clairs lors de l'utilisation exclusive du langage naturel. Des langages dédiés spécifiques au domaine, comme Lean, fournissent une supervision claire via la vérification formelle des preuves, permettant un entraînement efficace grâce à l'apprentissage par renforcement. Dans ce travail, nous proposons Seed-Prover, un modèle de raisonnement sur des preuves complètes de style lemme. Seed-Prover peut affiner itérativement sa preuve en se basant sur les retours de Lean, les lemmes prouvés et l'auto-résumé. Pour résoudre des problèmes de concours de niveau IMO, nous concevons trois stratégies d'inférence au moment du test qui permettent un raisonnement à la fois profond et étendu. Seed-Prover démontre 78,1 % des problèmes passés de l'IMO formalisés, sature MiniF2F et atteint plus de 50 % sur PutnamBench, surpassant largement l'état de l'art précédent. Pour pallier le manque de support géométrique dans Lean, nous introduisons un moteur de raisonnement géométrique Seed-Geometry, qui surpasse les moteurs de géométrie formelle précédents. Nous utilisons ces deux systèmes pour participer à l'IMO 2025 et démontrons entièrement 5 des 6 problèmes. Ce travail représente une avancée significative dans le raisonnement mathématique automatisé, démontrant l'efficacité de la vérification formelle avec un raisonnement en chaîne de pensée longue.

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.