論文の概要: DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

• arxiv url: http://arxiv.org/abs/2504.21801v2
• Date: Fri, 18 Jul 2025 08:20:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-21 20:43:26.032979
• Title: DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
• Title（参考訳）: DeepSeek-Prover-V2: 部分分解のための強化学習による形式的数学的推論の促進
• Abstract要約: 我々はDeepSeek-Prover-V2を紹介します。 このモデルは、ニューラル定理の証明における最先端のパフォーマンスを達成し、ミニF2Fテストで88.9%のパス比に達し、PutnamBenchの658問題のうち49を解決した。 標準ベンチマークに加えて、325の形式化された問題の集合であるProverBenchを導入し、最近のAIMEコンペティションから選択された15の問題を含む評価を強化した。
• 参考スコア（独自算出の注目度）: 24.50773495427783
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3's step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model. The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. In addition to standard benchmarks, we introduce ProverBench, a collection of 325 formalized problems, to enrich our evaluation, including 15 selected problems from the recent AIME competitions (years 24-25). Further evaluation on these 15 AIME problems shows that the model successfully solves 6 of them. In comparison, DeepSeek-V3 solves 8 of these problems using majority voting, highlighting that the gap between formal and informal mathematical reasoning in large language models is substantially narrowing.
• Abstract（参考訳）: 我々は,DeepSeek-V3を利用した再帰的定理証明パイプラインを通じて初期化データを収集した,Lean 4で証明された公式な定理のためのオープンソースの大規模言語モデルであるDeepSeek-Prover-V2を紹介する。 コールドスタートトレーニング手順は、DeepSeek-V3に複雑な問題を一連のサブゴールに分解するよう促すことから始まる。 解決されたサブゴールの証明は、DeepSeek-V3のステップバイステップ推論と組み合わせることで、強化学習のための最初のコールドスタートを生成する。 このプロセスにより、非公式な数学的推論と形式的な推論の両方を統一されたモデルに統合することができる。 結果のモデルであるDeepSeek-Prover-V2-671Bは、ニューラル定理の証明における最先端のパフォーマンスを達成し、ミニF2Fテストでのパス比88.9%に達し、パットナムベンチの658問題のうち49を解決した。 標準ベンチマークに加えて、325の形式化された問題の集合であるProverBenchを導入し、最近のAIMEコンペティション(24～25年)から選択された15の問題を含む評価を強化した。 これら15のAIME問題に対するさらなる評価は、モデルが6つをうまく解いたことを示している。 比較としてDeepSeek-V3は、多数決によるこれらの問題の8つを解決し、大きな言語モデルにおける形式的および非公式な数学的推論のギャップが著しく狭まっていることを強調した。

関連論文リスト

• Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction [95.91743732150233]
  一連のオープンソースの言語モデルであるGoedel-Prover-V2は、自動定理の新たな最先端を証明した。 我々は、より複雑な定理をマスターするためにモデルを訓練することの困難さを増す合成タスクを生成する。 Goedel-Prover-V2-32Bは、標準モードのpass@32でMiniF2Fの88.1%、自己補正モードの90.4%を達成する。
  論文  参考訳（メタデータ） (2025-08-05T16:28:22Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。 低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。 提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
  論文  参考訳（メタデータ） (2025-07-07T22:38:49Z)
• Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models [13.498044623556737]
  本稿では,Draft,Sketch,Proveフレームワークの改良版であるtextbfDSP+を紹介する。 相ごとに微細で統合されたニューロシンボリックエンハンスメントを特徴とする。 DSP+は、MiniF2F、ProofNet、PatnamBenchから80.7%、32.8%、24の644の問題を解決する。
  論文  参考訳（メタデータ） (2025-06-13T06:25:59Z)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [37.10426226729792]
  本稿では,パターン駆動型推論と形式的定理証明を統合するモジュール型ニューロシンボリック手法であるLLMe-Conjecture-Prove(ECP)フレームワークを紹介する。 本稿では,様々な数学コンペティションにおける3,431の解題問題のデータセットであるConstructiveBenchを紹介する。
  論文  参考訳（メタデータ） (2025-05-24T03:52:25Z)
• Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving [44.5694120006447]
  決定論的マルコフ決定過程として,問題解決の原理的定式化を提案する。 また,既存のFTP環境を利用してプロセス検証問題解決を行う新しいフレームワークFPSを提案する。 我々は, MATH500ベンチマークのサブセットの形式化であるFormalMath500, MiniF2F-Solving, PutnamBench-Solving, FTPベンチマークのMiniF2FとPutnamBenchの適応の3つのベンチマークを構築した。
  論文  参考訳（メタデータ） (2025-05-07T16:02:14Z)
• Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning [38.4246156415702]
  Kimina-Proverは、形式的定理証明のための新しい推論駆動探索パラダイムを開拓した大きな言語モデルである。 Qwen2.5-72Bから大規模な強化学習パイプラインでトレーニングされたKimina-Proverは、Lean 4の証明生成において、強力なパフォーマンスを示している。 Kimina-Prover は miniF2F ベンチマークに新しい最先端をセットし、pass@8192 で 80.7% に達した。
  論文  参考訳（メタデータ） (2025-04-15T16:23:44Z)
• 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)
• Exploring the Limit of Outcome Reward for Learning Mathematical Reasoning [65.2421542320293]
  推論能力は汎用知能の重要な構成要素である。 OpenAIのoシリーズモデルなどのプロプライエタリ企業による最近の進歩は、推論タスクに顕著な進歩をもたらした。 本稿では、数学的推論タスクのための textbfOutcome textbfREwtextbfArd ベースの強化 textbfLearning により達成できる性能限界を追求する新しい RL フレームワーク OREAL を提案する。
  論文  参考訳（メタデータ） (2025-02-10T18:57:29Z)
• LlamaV-o1: Rethinking Step-by-step Visual Reasoning in LLMs [103.0226977561914]
  大規模言語モデルにおけるステップバイステップの視覚的推論を促進するための包括的フレームワークを提案する。 マルチステップ推論タスクの評価に特化して設計された視覚推論ベンチマークを導入する。 第二に,個々のステップの粒度で視覚的推論品質を評価する新しい指標を提案する。 第3に、マルチステップのカリキュラム学習アプローチを用いて学習したLlamaV-o1という新しいマルチモーダル視覚推論モデルを提案する。
  論文  参考訳（メタデータ） (2025-01-10T18:59:51Z)
• Preference Optimization for Reasoning with Pseudo Feedback [100.62603571434167]
  提案手法では,解のラベル付けを関連するテストケースに対する評価として行うことで,推論タスクに対する疑似フィードバックを生成する手法を提案する。 本研究では,擬似フィードバックを優先最適化に用いる数学的推論と符号化の両タスクについて実験を行い,両タスク間の改善を観察する。
  論文  参考訳（メタデータ） (2024-11-25T12:44:02Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• Advancing LLM Reasoning Generalists with Preference Trees [119.57169648859707]
  推論に最適化された大規模言語モデル(LLM)のスイートであるEulusを紹介する。 Eurusモデルは、様々なベンチマークでオープンソースのモデルの間で最先端の結果を得る。
  論文  参考訳（メタデータ） (2024-04-02T16:25:30Z)
• Distilling Reasoning Capabilities into Smaller Language Models [83.66051257039763]
  思考の連鎖(CoT)のようなステップバイステップの推論アプローチは、大規模言語モデルにおける推論能力の誘導に非常に効果的であることが証明されている。 しかし、CoTアプローチの成功は基本的にモデルのサイズに結びついており、CoTを機能させるためには数十億のパラメータスケールモデルが必要であることが多い。 本研究では,大規模モデルのCoT推論能力を段階的に活用し,これらの能力をより小さなモデルに蒸留する知識蒸留手法を提案する。
  論文  参考訳（メタデータ） (2022-12-01T00:39:56Z)
• HyperTree Proof Search for Neural Theorem Proving [14.677400513932852]
  本稿では,変圧器を用いた自動定理証明のためのオンライン学習手順を提案する。 我々のモデルは、オンライントレーニングを通じて以前の証明検索から学習し、トレーニング分布から遠く離れた領域に一般化することができる。 HTPSだけでは、アノテートされた証明に基づいて訓練されたモデルがメタマス定理の65.4%を証明し、GPT-fにより56.5%の先行状態を著しく上回ることを示した。
  論文  参考訳（メタデータ） (2022-05-23T17:49:55Z)

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

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