論文の概要: Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience

• arxiv url: http://arxiv.org/abs/2512.17260v1
• Date: Fri, 19 Dec 2025 06:19:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-22 19:25:54.261742
• Title: Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
• Title（参考訳）: シードプロバー1.5:経験から学ぶことによる大学生レベルの理論証明の習得
• Authors: 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,
• Abstract要約: 大規模エージェント強化学習を用いて学習した公式な定理証明モデルである textbfSeed-Prover 1.5 を提案する。 本システムを用いて,Patnam 2025の12問題のうち,textbf11を9時間以内に解決した。
• 参考スコア（独自算出の注目度）: 38.07918040429112
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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 \textbf{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 \textbf{88\% of PutnamBench} (undergraduate-level), \textbf{80\% of Fate-H} (graduate-level), and \textbf{33\% of Fate-X} (PhD-level) problems. Notably, using our system, we solved \textbf{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.
• Abstract（参考訳）: 大規模言語モデルは最近、厳密な数学的証明を生成するために大きな進歩を遂げた。 対照的に、形式言語(リーンなど)で証明する定理にLLMを利用することは、特に学部レベル以上の問題に対処する場合、困難で計算コストがかかります。 本研究では,大規模なエージェント強化学習を通じて学習した公式な定理証明モデルである「textbf{Seed-Prover 1.5}」を,効率的なテスト時間スケーリング(TTS)ワークフローとともに提示する。 リーンや他のツールとの広範な相互作用を通じて、モデルはRLプロセスでの経験を継続的に蓄積し、形式的定理証明の能力と効率を大幅に向上します。 さらに、最近の自然言語証明の進歩を活用して、我々のTSワークフローは、自然言語と形式言語のギャップを効率的に埋める。 最先端の手法と比較して、Seed-Prover 1.5はより少ない計算予算で優れたパフォーマンスを達成する。 これはPatnamBench} の \textbf{88\%(学部レベル)、Fate-H} の \textbf{80\%(大学院レベル)、Fate-X} の \textbf{33\%(PhDレベル)を解く。 特に,本システムを用いて,パットナム2025号から9時間以内に,12問題のうちのtextbf{11>を解いた。 本研究は,高品質な形式的フィードバックによる経験からの学習のスケーリングが,形式的数学的推論の将来に大きな可能性を秘めていることを示唆する。

関連論文リスト

• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
  本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。 IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。 シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
  論文  参考訳（メタデータ） (2025-07-31T17:00:30Z)
• ProofCompass: Enhancing Specialized Provers with LLM Guidance [6.757964026033364]
  本稿では,計算効率を向上する新しいハイブリッド手法であるProofを紹介する。 DeepSeek-Prover-v1.5-RL (DSP-v1.5) のような既存の特殊な証明手法をLLM (Large Language Model) で戦略的にガイドする。 miniF2F ベンチマークでは、Proof は DSP-v1.5 (54.9% rightarrow 55.3%$) を上回っ、25 個の試行 (3200 rightarrow 128$) を使用する。
  論文  参考訳（メタデータ） (2025-07-18T19:28:01Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。 低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。 提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
  論文  参考訳（メタデータ） (2025-07-07T22:38:49Z)
• MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving [30.112351299773632]
  この問題を解決するために,我々はLean4定理の包括的なフレームワークを提案する。 一般的なNLの認識タスクを完全防御生成と証明修正のための誤り解析に分離する。 我々のフレームワークは、MiniF2F-TestデータセットのLean4バージョンにおいて**61.07%*の精度を達成する。
  論文  参考訳（メタデータ） (2025-03-05T05:50:31Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。