論文の概要: Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2507.23726v1
• Date: Thu, 31 Jul 2025 17:00:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-01 17:19:10.127151
• Title: Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
• Title（参考訳）: シードプロバー:自動定理証明のための深部・広部推論
• 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,
• 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つを完全に証明します。 この研究は、自動化された数学的推論において重要な進歩を示し、長いチェーン・オブ・シークレット推論による形式的検証の有効性を実証している。

関連論文リスト

• 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)
• LAMBADA: Backward Chaining for Automated Reasoning in Natural Language [11.096348678079574]
  LAMBADAと呼ばれる逆チェインアルゴリズムは、推論を4つのサブモジュールに分解する。 LAMBADAは最先端のフォワード推論手法よりも精度が向上することを示す。
  論文  参考訳（メタデータ） (2022-12-20T18:06:03Z)

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

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