Seed-Prover 1.5：経験からの学習による学部レベルの定理証明の習得
Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
December 19, 2025
著者: Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, Zhihong Wang, Mingxuan Wang, Chenrui Wei, Shufa Wei, Huajian Xin, Fan Yang, Weihao Gao, Zheng Yuan, Tianyang Zhan, Zeyu Zheng, Tianxi Zhou, Thomas Hanwen Zhu
cs.AI
要旨
大規模言語モデルは近年、厳密な数学的証明を生成する能力において著しい進歩を遂げている。一方、形式言語（Leanなど）における定理証明へのLLM応用は依然として困難であり、特に学部レベル以上の課題に対処する際には計算コストが高い。本研究では、大規模エージェント強化学習により訓練された形式定理証明モデルSeed-Prover 1.5と、効率的なテスト時スケーリング（TTS）ワークフローを提案する。Leanなどのツールとの大規模な相互作用を通じて、モデルはRLプロセス中に継続的に経験を蓄積し、形式定理証明の能力と効率を大幅に向上させる。さらに、自然言語証明における最近の進展を活用したTTSワークフローは、自然言語と形式言語の間のギャップを効率的に橋渡しする。従来の最先端手法と比較して、Seed-Prover 1.5はより少ない計算予算で優れた性能を発揮し、PutnamBench（学部レベル）の88%、Fate-H（大学院レベル）の80%、Fate-X（博士レベル）の33%の問題を解決した。特筆すべきは、本システムを用いてPutnam 2025の12問中11問を9時間以内に解決した点である。高品質な形式的フィードバックに駆動された経験からの学習のスケーリングが、形式的数学推論の将来に大きな可能性をもたらすことが示唆される。
English
Large language models have recently made significant progress to generate rigorous mathematical proofs. In contrast, utilizing LLMs for theorem proving in formal languages (such as Lean) remains challenging and computationally expensive, particularly when addressing problems at the undergraduate level and beyond. In this work, we present Seed-Prover 1.5, a formal theorem-proving model trained via large-scale agentic reinforcement learning, alongside an efficient test-time scaling (TTS) workflow. Through extensive interactions with Lean and other tools, the model continuously accumulates experience during the RL process, substantially enhancing the capability and efficiency of formal theorem proving. Furthermore, leveraging recent advancements in natural language proving, our TTS workflow efficiently bridges the gap between natural and formal languages. Compared to state-of-the-art methods, Seed-Prover 1.5 achieves superior performance with a smaller compute budget. It solves 88\% of PutnamBench (undergraduate-level), 80\% of Fate-H (graduate-level), and 33\% of Fate-X (PhD-level) problems. Notably, using our system, we solved 11 out of 12 problems from Putnam 2025 within 9 hours. Our findings suggest that scaling learning from experience, driven by high-quality formal feedback, holds immense potential for the future of formal mathematical reasoning.