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）は、長い連鎖思考（chain-of-thought）を伴う強化学習を活用することで、強力な数学的推論能力を示してきた。しかし、自然言語のみを使用する場合、明確な教師信号が不足しているため、定理証明において依然として困難を抱えている。Leanのような専用のドメイン固有言語は、証明の形式的検証を通じて明確な教師信号を提供し、強化学習による効果的なトレーニングを可能にする。本研究では、Seed-Proverという補題スタイルの全証明推論モデルを提案する。Seed-Proverは、Leanからのフィードバック、証明済みの補題、および自己要約に基づいて、証明を反復的に洗練することができる。IMOレベルの競技問題を解決するために、深い推論と広範な推論を可能にする3つのテスト時推論戦略を設計した。Seed-Proverは、過去のIMO問題の形式化されたものの78.1%を証明し、MiniF2Fを飽和させ、PutnamBenchで50%以上を達成し、従来の最先端技術を大幅に上回る性能を示した。Leanにおける幾何学サポートの不足に対処するため、Seed-Geometryという幾何学推論エンジンを導入し、従来の形式的幾何学エンジンを上回る性能を実現した。これら2つのシステムを使用してIMO 2025に参加し、6問中5問を完全に証明した。この研究は、長い連鎖思考推論を伴う形式的検証の有効性を示し、自動化された数学的推論における重要な進展を表している。

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.