論文の概要: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning

• arxiv url: http://arxiv.org/abs/2511.22570v1
• Date: Thu, 27 Nov 2025 16:01:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-01 19:47:55.63065
• Title: DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
• Title（参考訳）: DeepSeekMath-V2: 自己検証可能な数学的推論を目指して
• Authors: Zhihong Shao, Yuxiang Luo, Chengda Lu, Z. Z. Ren, Jiewen Hu, Tian Ye, Zhibin Gou, Shirong Ma, Xiaokang Zhang,
• Abstract要約: 正しい答えは正しい推論を保証するものではない。 深い推論の限界を推し進めるためには、数学的推論の包括性と厳密さを検証する必要があると信じている。 我々のモデルであるDeepSeekMath-V2は、IMO 2025とCMO 2024のゴールドレベルスコア、Patnam 2024のほぼ完璧な118/120のスケールされたテストタイム計算を達成し、強力な定理証明能力を示す。
• 参考スコア（独自算出の注目度）: 26.142347272743496
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models have made significant progress in mathematical reasoning, which serves as an important testbed for AI and could impact scientific research if further advanced. By scaling reasoning with reinforcement learning that rewards correct final answers, LLMs have improved from poor performance to saturating quantitative reasoning competitions like AIME and HMMT in one year. However, this approach faces fundamental limitations. Pursuing higher final answer accuracy doesn't address a key issue: correct answers don't guarantee correct reasoning. Moreover, many mathematical tasks like theorem proving require rigorous step-by-step derivation rather than numerical answers, making final answer rewards inapplicable. To push the limits of deep reasoning, we believe it is necessary to verify the comprehensiveness and rigor of mathematical reasoning. Self-verification is particularly important for scaling test-time compute, especially for open problems without known solutions. Towards self-verifiable mathematical reasoning, we investigate how to train an accurate and faithful LLM-based verifier for theorem proving. We then train a proof generator using the verifier as the reward model, and incentivize the generator to identify and resolve as many issues as possible in their own proofs before finalizing them. To maintain the generation-verification gap as the generator becomes stronger, we propose to scale verification compute to automatically label new hard-to-verify proofs, creating training data to further improve the verifier. Our resulting model, DeepSeekMath-V2, demonstrates strong theorem-proving capabilities, achieving gold-level scores on IMO 2025 and CMO 2024 and a near-perfect 118/120 on Putnam 2024 with scaled test-time compute.
• Abstract（参考訳）: 大規模な言語モデルは、AIの重要なテストベッドとして機能し、さらに進歩すれば科学研究に影響を与える可能性がある数学的推論において大きな進歩を遂げた。 最終回答を正す強化学習による推論をスケールすることにより、LCMはパフォーマンスの低下から、AIMEやHMMTのような定量的推論競争を1年で飽和させるまで改善した。 しかし、このアプローチは基本的な制限に直面している。 正しい答えは正しい推論を保証するものではない。 さらに、定理証明のような数学的なタスクの多くは、数値的な答えよりも厳密なステップバイステップの導出を必要とし、最終的な答えの報酬は適用できない。 深い推論の限界を推し進めるためには、数学的推論の包括性と厳密さを検証する必要があると信じている。 自己検証は、テスト時間計算のスケーリング、特に既知のソリューションのないオープンな問題において特に重要である。 自己検証可能な数学的推論に向けて、定理証明のための正確で忠実なLCMベースの検証器の訓練方法を検討する。 次に、検証器を報酬モデルとして用いて証明生成器を訓練し、検証器を確定する前に可能な限り多くの問題を特定し、解決するインセンティブを与える。 生成元がより強くなるにつれて、生成元検証のギャップを保ちながら、検証計算をスケールして新しい検証証明を自動的にラベル付けし、検証をさらに改善するためのトレーニングデータを作成することを提案する。 得られたモデルであるDeepSeekMath-V2は、IMO 2025とCMO 2024のゴールドレベルスコア、Patnam 2024のほぼ完璧な118/120のスケールされたテストタイム計算を達成し、強力な定理証明能力を示す。

関連論文リスト

• Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection [42.21636315733425]
  大規模言語モデルは、最終解答問題において顕著な成功を収めた。 しかし、これらのソリューションの根底にある理由はしばしば欠陥がある。 モデル性能のより信頼性の高い尺度を得るために,証明ベースと最終回答推論の両方を評価した。
  論文  参考訳（メタデータ） (2025-11-17T06:25:35Z)
• Hard2Verify: A Step-Level Verification Benchmark for Open-Ended Frontier Math [80.46254366870447]
  私たちは500時間以上の人的労力で生成された段階レベルの検証ベンチマークであるHard2Verifyを紹介します。 我々は29人の生成的批評家とプロセス報酬モデルを評価し、いくつかの点を超えて、オープンソースの検証者がクローズドソースモデルを評価することを実証した。
  論文  参考訳（メタデータ） (2025-10-15T16:50:54Z)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• Let's Verify Math Questions Step by Step [29.69769942300042]
  MathQ-Verifyは、未定または未定の数学問題を厳格にフィルタリングするために設計された、新しいパイプラインである。 MathQ-Verifyはまず、冗長な命令を削除するためのフォーマットレベルのバリデーションを実行する。 その後、各質問を形式化し、それを原子状態に分解し、数学的定義に対して検証する。
  論文  参考訳（メタデータ） (2025-05-20T04:07:29Z)
• DeepMath-103K: A Large-Scale, Challenging, Decontaminated, and Verifiable Mathematical Dataset for Advancing Reasoning [95.31714779585272]
  DeepMath-103Kは、高い難易度(主に5-9レベル)で設計された大規模な数学的データセットである これには、多数のベンチマークに対する厳格な除染、ルールベースのRL報酬に対する検証可能な回答が含まれる。 DeepMath-103Kは一般化可能な推論の進展を促進する。
  論文  参考訳（メタデータ） (2025-04-15T17:59:51Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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