論文の概要: Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
- arxiv url: http://arxiv.org/abs/2507.23726v2
- Date: Fri, 01 Aug 2025 03:36:47 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-08-04 12:04:25.447801
- Title: Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
- Title（参考訳）: シードプロバー:自動定理証明のための深部・広部推論
- Abstract要約: 本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。
IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。
シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
- 参考スコア（独自算出の注目度）: 36.20164235042574
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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 \textbf{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 \textbf{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.
- Abstract（参考訳）: LLMは、長い連鎖で強化学習を活用することで強力な数学的推論能力を示してきたが、自然言語のみを使用する際に明確な監視信号が欠如していることから、定理証明に苦慮し続けている。
Leanのような専門的なドメイン固有言語は、証明の正式な検証を通じて明確な監視を提供し、強化学習による効果的なトレーニングを可能にします。
本研究では, 補題型完全防御推論モデルである \textbf{Seed-Prover} を提案する。
Seed-Proverは、リーンのフィードバック、証明されたレムマ、自己要約に基づいて、その証明を反復的に洗練することができる。
IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。
Seed-Prover は、過去の IMO の問題を 78.1 % で解決し、MiniF2F を飽和させ、PutnamBench を 50 % 以上上回った。
リーンにおける幾何学的サポートの欠如に対処するため,従来の形式的幾何学的エンジンよりも優れた幾何学的推論エンジンであるtextbf{Seed-Geometry}を導入する。
IMO 2025に参加するためにこの2つのシステムを使用し、6つの問題のうち5つを完全に証明します。
この研究は、自動化された数学的推論において重要な進歩を示し、長いチェーン・オブ・シークレット推論による形式的検証の有効性を実証している。
関連論文リスト
- LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文 参考訳（メタデータ） (2026-06-03T20:09:39Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience [38.07918040429112]
大規模エージェント強化学習を用いて学習した公式な定理証明モデルである textbfSeed-Prover 1.5 を提案する。
本システムを用いて,Patnam 2025の12問題のうち,textbf11を9時間以内に解決した。
論文 参考訳（メタデータ） (2025-12-19T06:19:55Z) - DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [26.142347272743496]
正しい答えは正しい推論を保証するものではない。
深い推論の限界を推し進めるためには、数学的推論の包括性と厳密さを検証する必要があると信じている。
我々のモデルであるDeepSeekMath-V2は、IMO 2025とCMO 2024のゴールドレベルスコア、Patnam 2024のほぼ完璧な118/120のスケールされたテストタイム計算を達成し、強力な定理証明能力を示す。
論文 参考訳（メタデータ） (2025-11-27T16:01:22Z) - Discovering New Theorems via LLMs with In-Context Proof Learning in Lean [6.097030695272925]
数理予想を自動的に生成し,それをLean 4フォーマットで証明するための導出-証明ループパイプラインを提案する。
このアプローチの特徴は、以前に生成された定理とその証明を含む文脈でさらなる予想を生成し、証明することである。
これらの定理のうちの少なくとも1つは、自然言語においても、文脈内学習なしでは LLM によって証明できない。
論文 参考訳（メタデータ） (2025-09-16T06:48:11Z) - Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。
低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。
提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
論文 参考訳（メタデータ） (2025-07-07T22:38:49Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - 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) - Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。
我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。
我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
論文 参考訳（メタデータ） (2024-11-04T05:57:40Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - LAMBADA: Backward Chaining for Automated Reasoning in Natural Language [11.096348678079574]
LAMBADAと呼ばれる逆チェインアルゴリズムは、推論を4つのサブモジュールに分解する。
LAMBADAは最先端のフォワード推論手法よりも精度が向上することを示す。
論文 参考訳（メタデータ） (2022-12-20T18:06:03Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。