--- title: "DeepSeekMathとは？V2の自己検証の仕組みとIMO 2025実績・2024年版7Bとの違い" url: "https://www.issoh.co.jp/tech/details/10022/" published: 2025-11-28 updated: 2026-09-27 categories: ["LLM・RAG"] publisher: "株式会社一創" --- # DeepSeekMathとは？V2の自己検証の仕組みとIMO 2025実績・2024年版7Bとの違い DeepSeekMathという名前は、まったく性格の違う2つのモデルを指します。ひとつは2024年2月の論文「DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models」（arXiv:2402.03300）で公開された7Bの数式計算モデルで、強化学習アルゴリズムGRPOの初出としてよく参照されます。もうひとつが2025年11月27日公開のDeepSeekMath-V2で、こちらは答えではなく証明の厳密さを自分で採点させることに賭けた685Bのモデルです。両者は規模も課題設定も別物で、片方の情報をもう片方に当てはめると結論を間違えます。 本記事は技術報告、Hugging Face APIの実測値、公式の評価スクリプトを一次情報として、この2つを切り分けて整理します。 ## まとめ：DeepSeekMathの要点 - **同名で2系統あります。**2024年版はDeepSeekMath 7B（arXiv:2402.03300）、2025年版はDeepSeekMath-V2（685B）で、GRPOの提案元は前者です。 - **V2の中核は自己検証です。**証明の妥当性を採点する検証器を先に育て、それを報酬モデルにして証明生成器を訓練します。 - **実測スコアは、IMO 2025が6問中5問で83.3%、CMO 2024が73.8%、Putnam 2024が118/120（98.3%）です。**「全問正解」ではありません。 - **IMO-ProofBenchでは勝敗が分かれます。**Basicは99.0でGemini Deep Think（IMO Gold）の89.0を上回り、Advancedは61.9で65.7に届きません。 - **ライセンスはApache 2.0ですが、手軽には動きません。**重みはFP8で約689GBあり、公式手順は重み変換込みの`torchrun`実行です。 - **競技スコアは大量の検証計算を投入した条件下の値です。**1回の呼び出しで同じ品質は出ません。 ## 2024年版DeepSeekMath 7Bと2025年版V2の違い 「deepseekmath」で探している情報がどちらにあるかを先に判別できるよう、両者の素性を並べます。 ### 2024年版：120Bトークンの数学コーパスとGRPOの初出 2024年2月5日投稿の論文で公開されたのがDeepSeekMath 7Bです。DeepSeek-Coder-Base-v1.5 7Bを出発点に、Common Crawl由来の数学関連120Bトークンを自然言語・コードデータと合わせて継続事前学習したモデルで、外部ツールも多数決も使わずMATHベンチマークで51.7%、64サンプルの自己一貫性（self-consistency）併用で60.9%を記録しました。 この論文がよく引かれるもうひとつの理由が、PPOの派生として提案されたGRPO（Group Relative Policy Optimization）です。要旨では、PPOのメモリ使用量を最適化しつつ数学推論能力を高める手法と位置づけられています。GRPOはDeepSeek-R1にも採用され、いまでは元論文の主題である7Bモデルより広く知られています。GRPOの目的関数やPPOとの差分そのものは、[GRPOとは？DeepSeekの強化学習アルゴリズムの公式・仕組みとPPOとの違い](https://www.issoh.co.jp/tech/details/5506/)で個別に扱っています。 ### 2025年版：証明の厳密さを採点対象にしたV2 DeepSeekMath-V2は2025年11月27日にHugging Faceへ公開されました。土台はDeepSeek-V3.2-Exp-Baseで、Hugging Face APIが返すsafetensorsのパラメータ合計は685,396,921,376（約685B）です。内訳はFP8（E4M3）が681,408,069,632、BF16が3,946,184,704、FP32が42,667,040で、単一の精度で保存されているわけではありません。 技術報告の問題意識は、最終解答が合っていても推論が正しいとは限らない、という点にあります。AIMEやHMMTのように答えの正誤だけを見る指標は1年で飽和した一方、定理証明のように答えという形を取らない課題では最終解答報酬が使えません。そこでV2は、証明の網羅性と厳密さを評価する検証器を訓練し、それを報酬に生成器を鍛えます。 ### 2系統の対照表 | 項目 | DeepSeekMath（2024年版） | DeepSeekMath-V2（2025年版） | | ------ | --------------------------- | ------------------------------------------ | | 公開時期 | 2024年2月5日（arXiv投稿） | 2025年11月27日 | | 規模 | 7B | 685B（safetensors実測） | | 土台 | DeepSeek-Coder-Base-v1.5 7B | DeepSeek-V3.2-Exp-Base | | 主な課題 | 数式計算の正答率（MATH等） | 自然言語による定理証明 | | 代表値 | MATH 51.7%（自己一貫性64で60.9%） | Putnam 2024で118/120 | | 手法上の売り | GRPOの提案 | 自己検証とメタ検証 | | 識別子 | arXiv:2402.03300 | Hugging Face: deepseek-ai/DeepSeek-Math-V2 | V2の技術報告は、GitHubリポジトリ直下のPDF（DeepSeekMath\_V2.pdf、19ページ）のほか、arXiv:2511.22570としても2025年11月27日に投稿されています。2024年版の2402.03300と混同しやすいため、参照時は番号で区別してください。 ## V2の自己検証を育てる4段階の学習手順 V2の説明でよく見かける「生成器と検証器という2つのモデルが協調する」という図式は、技術報告と食い違います。報告は高計算量探索の節で、すべての実験は最終的な証明生成器という単一のモデルを使い、そのモデルが生成と検証の両方を行うと明記しています。2つが並走するのではなく、1つのモデルが2つの役割を担える状態まで訓練されている、というのが実際の構成です。 ### 第1段階：検証器を鍛える2つの報酬 まず、数学の専門家が注記した「問題・証明・証明スコア」の組で検証器を訓練します。証明スコアは0か0.5か1の3値で、0〜1の連続値ではありません。報酬は次の2成分です。 - **形式報酬**：出力に「指摘した問題点の要約」と「証明スコア」の両方が含まれるかを判定する指示関数です。技術報告は、最終応答に`Here is my evaluation of the solution:` という語句が含まれること、および `Based on my evaluation, the final overall score should be:` に続く`\boxed{}`内のスコアが存在することを条件として明示しています。 - **スコア報酬**：予測スコアと注記スコアの近さで、式は 1 から両者の差の絶対値を引いた値です。 検証器の学習目的は、この2つの積を最大化する形で定義されます。 ### 第2段階：でっち上げの指摘を潰すメタ検証 第1段階だけでは抜け道が残ります。欠陥のある証明を評価する場面で、存在しない問題点を作り上げながらスコアだけ正しく当てれば満額の報酬を得られてしまうためです。技術報告はこれを信頼性を損なう致命的な脆弱性と表現しています。 対策として導入されたのがメタ検証です。検証器が指摘した問題点が実在するか、その指摘が予測スコアを論理的に正当化しているかを、二段目の評価プロセスが判定します。専門家が検証器の出力品質を0・0.5・1で注記したデータセットを作り、それでメタ検証器を訓練したうえで、検証器側の報酬を「形式報酬×スコア報酬×メタ検証スコア」の積に変更します。 効果は数値で示されています。検証データの検証用分割において、メタ検証器が評価した検証器の分析品質スコアは0.85から0.96へ改善し、その間も証明スコア予測の正確さは維持されました。 ### 第3段階：自分の粗を先に見つけさせる報酬設計 訓練済みの検証器を生成的な報酬モデルとして使い、証明生成器を訓練します。ただし制約が観察されました。生成と自己分析を一度に行わせると、外部の検証器なら容易に見つける欠陥があっても、生成器は自分の証明を正しいと主張しがちだったのです。外部の指摘には従えるのに、自分の仕事へは専用検証器と同じ厳しさを適用できない、という現象です。 そこで報酬を、証明のスコアと、自己分析側のスコア（自己採点の一致度とメタ検証スコアの積）の重み付き和に、形式報酬を掛ける形で組み立てます。技術報告が採用した重みは、証明側が0.76、自己分析側が0.24です。この設計では、誤りを正直に認めるほうが、正しいと偽るより高く報われます。最大の報酬は、正しい証明を作り、かつそれが正しいと正確に認識できた場合です。結果として生成器の最善手は、確定前に自分の証明の問題点を自分で潰しておくことになります。 ### 第4段階：検証計算の拡大による学習データの自動生成 生成器が強くなると検証器との実力差（generation-verification gap）が詰まり、検証器が報酬として機能しなくなります。これを避けるため、V2は検証計算量を増やして、人手では判定しづらい証明に自動でラベルを付けます。 手順は3段です。まず証明ごとにn件の検証分析を独立に生成します。次に問題点を報告した分析（スコア0または0.5）についてm件のメタ検証をかけ、その過半数が指摘を認めた分析だけを妥当と扱います。最後に最も低いスコアを付けた分析を見て、妥当と認められたものがk件以上あれば、その最低スコアがラベルになります。すべての検証試行で正当な問題点が挙がらなければ1が付き、どちらにも当てはまらない証明は破棄するか人間の専門家へ回します。 技術報告は、最後の2回の学習反復ではこの全自動パイプラインが人手の注記を完全に置き換えたとし、自動ラベルが専門家の判断とよく整合することを品質チェックで確認したとしています。 なお、この一連の強化学習にはGRPOがそのまま使われています。「GRPOの変種を独自開発した」わけではなく、技術報告はShaoら2024を引用してGRPOを採用したと記述しており、2系統のDeepSeekMathはここで直接つながります。 ## ベンチマーク実測値と勝敗が分かれる境目 ### 競技数学3種の実測 技術報告のTable 1が示す結果は次のとおりです。原論文の表では灰色が完全正解、下線が部分点を表しますが、以下では得点した問題をまとめて記載しています。 | 大会 | 問題数 | 得点した問題 | 得点率 | | ----------- | --- | -------------- | ----- | | IMO 2025 | 6問 | P1、P2、P3、P4、P5 | 83.3% | | CMO 2024 | 6問 | P1、P2、P4、P5、P6 | 73.8% | | Putnam 2024 | 12問 | A1からB4、B5、B6 | 98.3% | 本文の記述と突き合わせると、IMO 2025は6問中5問を解いて金メダル相当、CMO 2024は4問完答＋1問部分点で金メダル相当です。IMO 2025を全問正解した、あるいは5問中5問正解した、という説明は誤りで、V2が得点できなかったP6が残っています。得点率83.3%は42点満点に対する35点です。 この35点は、2025年7月にIMO 2025で金メダル相当を発表したGemini Deep ThinkやOpenAIの推論モデルと同水準です。V2の新規性は点数の高さではなく、それをオープンウェイトのモデルと公開された検証手順で出した点にあります。 Putnam 2024では12問中11問を完答し、残る1問も軽微な誤りにとどめて118/120を獲得しました。技術報告は同大会の人間の最高得点を90点として引用し、それを上回ったと述べています。 ### IMO-ProofBench：論文掲載モデル間でBasic首位・Advanced2位 IMO-ProofBenchは、Deep ThinkのIMO金メダル達成を担ったDeepMindチームが開発した60問のベンチマークで、basic集合30問（IMO予選からIMO中程度）とadvanced集合30問（IMO本番相当から最難関）に分かれます。技術報告の図3が示す専門家評価は次のとおりで、V2以外はLuongら2025からの引用値です。 | モデル | ProofBench Basic | ProofBench Advanced | | ----------------------------------- | ---------------- | ------------------- | | DeepSeekMath-V2（Heavy） | 99.0 | 61.9 | | Gemini Deep Think（IMO Gold） | 89.0 | 65.7 | | Gemini Deep Think（IMO lite） | 83.8 | 37.6 | | Gemini 2.5 Pro（Huang & Yang 2025併用） | 69.5 | 24.8 | | GPT-5 | 59.0 | 20.0 | | Gemini 2.5 Pro | 55.2 | 17.6 | | Grok 4 | 46.7 | 18.6 | 掲載されている残り3モデルはQwen3-235Bが33.3と5.2、DeepSeek R1が29.0と3.8、Claude Sonnet 4が27.1と4.8で、いずれもadvanced集合はほぼ解けていません。読み取るべき点は2つです。basic集合ではDeepSeekMath-V2の99.0がDeep Think（IMO Gold）の89.0を上回り、advanced集合では61.9対65.7で下回ります。技術報告自身も、basic集合では上回りadvanced集合では拮抗していると書き分け、最難関のIMOレベル問題は依然として難しいと明言しています。「Gemini Deep Thinkを上回った」の一言でまとめると、後半を落とすことになります。 一度の生成だけで比較した場合の結果も報告されています。自社作成のCNMLレベル91問（代数13、幾何24、整数論19、組合せ24、不等式11）を問題あたり8サンプル生成し、DeepSeek側の最終検証器による8件の分析の多数決で採点したところ、全カテゴリでGPT-5-Thinking-HighとGemini 2.5 Proを上回りました。専門家評価であるIMO-ProofBenchとは採点主体が異なる点に注意してください。 ### 競技スコアの前提となる生成・検証の計算量 競技数学の結果は、生成と検証の両方に大量の計算を投入した条件で得られています。技術報告が記す手順は次のとおりです。 - 問題ごとに64件の証明サンプルを作り、それぞれに64件の検証分析を生成して候補プールを初期化します。 - 各改善反復で平均検証スコア上位64件の証明を選び、それぞれにランダムな8件の分析を組み合わせます。問題点を指摘している分析（スコア0または0.5）が優先されます。 - 組ごとに改善版の証明を1件生成し、候補プールを更新します。 - これを最大16反復、または64回すべての検証を通過するまで続けます。 つまり「1問あたり数千回規模の生成と検証を回した結果の最高得点」であり、APIを1回叩いて得られる品質とは別物です。 ## 公式配布物と推論環境の実際 ### 重みは689GBのFP8チェックポイント Hugging Faceのリポジトリ`deepseek-ai/DeepSeek-Math-V2`には163個のsafetensorsファイルが置かれており、合計サイズは約689.5GB（689,483,049,129バイト）です。config.jsonの`quantization_config`は量子化方式がfp8、形式がe4m3、ブロックサイズが128かける128、活性化スケールがdynamicとなっています。すでにFP8で配布されているため、そこから追加量子化でどれだけ削れるか、精度がどう動くかは、配布形式の情報だけでは判断できません。 同じconfig.jsonから読める構成は、アーキテクチャが`DeepseekV32ForCausalLM`、61層、hidden\_sizeが7168、ルーティング対象エキスパート256でトークンあたり8つを選択、共有エキスパート1つ、最大位置埋め込みが163,840トークンです。コンテキスト長は約16万トークンであり、10億トークン規模ではありません。またV100やA100はFP8のネイティブ演算に対応しないため、枚数を並べても前提を満たしません。FP8対応のGPUを用意する場合も、演算対応と推論実装側の対応機種は別に確認が必要です。 ### Hugging Faceの自動生成スニペットとDeepSeek公式の案内 Hugging Faceのモデルページを開くと、`AutoModelForCausalLM.from_pretrained`や`vllm serve`を使うコード例が上部に表示されます。ただしこれは、モデルカードのメタデータに`library_name: transformers`が指定され、APIが`auto_model`に`AutoModelForCausalLM`を返すことから、Hugging Face側が機械的に組み立てている定型スニペットです。 DeepSeekが書いたQuick Startの節にあるのは、「DeepSeekMath-V2はDeepSeek-V3.2-Exp-Baseの上に構築されている。推論のサポートについてはDeepSeek-V3.2-Expのリポジトリを参照してほしい」という案内だけです。ただしHugging Faceのリポジトリ自体にも`inference`ディレクトリが同梱されており、そこのREADMEは別の手順を示します。`convert.py`で重みをこのプロジェクト形式へ変換したうえで、`torchrun`から`generate.py`を起動する流れで、対話実行・ファイル入力のバッチ実行・複数ノード実行の3つの起動例が並んでいます。 つまり公式のローカル推論経路は、transformersの`from_pretrained`ではなく、この変換込みの`torchrun`手順です。自動生成されたスニペットを公式の動作保証と読み違えないでください。 ### 公式評価スクリプトの既定値と実行の前提 GitHubリポジトリのinferenceディレクトリには、競技問題を解かせる一式（generate.py、main.py、math\_templates.py、run.sh、utils.py）と、IMO 2025・CMO 2024・CMO 2025・Putnam 2024の入力JSON、IMO-ProofBenchを含む出力JSONLが同梱されています。READMEの指示はgenerate.pyにAPIキーを書いてrun.shを実行する、というもので、こちらはローカル推論用ではなくAPIを叩く評価ハーネスです。 run.shが渡している値は、探索の重さを具体的に示しています。ただしこれは設定の抜粋であって、そのまま実行できる完成手順ではありません。公開されている`main.py`は`proof_gen_url`、`proof_rate_url`、`infer_script`、`proof_gen_with_self_eval`の4つを`args`から読みますが、いずれも`add_argument`で定義されていないため、手当てなしでは起動しません。 ``` python main.py \ --input_paths ${input_path} \ --output_dirname ${output_dirname} \ --proof_pool_dirname ${proof_pool_dirname} \ --n_best_proofs_to_sample 32 \ --n_proofs_to_refine 1 \ --n_agg_trials 32 \ --n_parallel_proof_gen 128 \ --n_verification_per_proof 64 \ --skip_meta_verification \ --start_round 1 \ --max_rounds 16 ``` main.pyの既定値は、証明生成の最大長が128Kトークン、検証とメタ検証が64Kトークン、温度はいずれも1.0、検証プロセス数320、生成プロセス数40、バッチサイズ160、反復上限20です。`n_verification_per_proof`の既定値は4ですが、run.shは64へ引き上げています。検証回数を16倍にしている点がこの評価設定の要点です。 ### ライセンスと利用条件 リポジトリと重みはApache License 2.0で提供されます。商用利用や改変、再配布が許されるライセンスであり、この点は旧来のDeepSeekモデル向け独自ライセンスから緩和された扱いです。ただし、Apache 2.0が課す条件は再配布時のもので、ライセンス文の交付、変更したファイルへの変更表示、権利表示やNOTICEの保持などが求められます。社外へ配る成果物に含める場合はこの義務を満たしてください。なお、Hugging Face上のリポジトリは2025年11月27日の公開以降に更新されていません。これは確認時点の更新履歴であり、今後の更新頻度を約束するものではありません。 ## 適用に向く用途と避けるべき条件 ### 向いている使い方：自然言語の証明レビュー 自然言語で書かれた証明の妥当性を機械的に採点したい場面が本来の射程です。技術報告が強調するのも、従来は自動検証が難しいとされた証明についてLLMベースの検証器を訓練できた点でした。模範解答の粗探し、書き直し候補の量産、学生の証明への初期フィードバックは、人間の確認を前提にすれば現実的な適用範囲です。 ただし0・0.5・1というスコアは、採点結果そのものとして扱うより、どこを人間が見るべきかの優先順位付けに使うほうが安全です。解けなかった問題でも自分の証明の真の問題点は特定できていた、という報告がこの使い方を後押しします。 ### 向かない使い方：形式検証・即時応答・自社設備 まず、形式検証の置き換えにはなりません。V2が扱うのは自然言語の証明で、Lean 4やCoqのように証明チェッカが機械的に正しさを保証する仕組みとは性質が異なります。正しさを保証したい場面では、[Lean4とは？入門・インストールからMathlib4・VSCode設定まで](https://www.issoh.co.jp/tech/details/8641/)で扱っている形式手法のほうが目的に合います。 次に、対話的な数学アシスタントとしても向きません。競技スコアを支えているのは1問あたり数千回規模の生成と検証で、応答時間と費用が一般的なチャット用途と合わないためです。日常的な数式計算や解法の説明なら、汎用の推論モデルのほうが扱いやすくなります。 最後に、十分なGPUメモリを確保できないのであれば、自社設備での常時稼働は勧められません。約689GBの重みに加えて推論用のメモリも要るうえ、その規模を証明検証という限られた用途に占有することになるためです。DeepSeek系のモデルを業務で使う前提での選定は、[DeepSeek V4とは？Compressed Sparse Attention(CSA)の仕組みとPro/Flashの性能・料金・移行期限](https://www.issoh.co.jp/tech/details/12053/)で扱っている現行の汎用モデル側から検討するほうが現実的です。 ## よくある質問 ### DeepSeekMathとDeepSeekMath-V2は同じモデルの新旧版ですか？ 系譜としてはつながっていますが、中身は別物です。2024年版は7BでDeepSeek-Coder-Base-v1.5 7Bを土台にした数式計算向けモデル、2025年版のV2は685BでDeepSeek-V3.2-Exp-Baseを土台にした定理証明向けモデルです。共通するのは、2024年版の論文が提案したGRPOがV2の強化学習でも使われている点です。 ### V2はIMO 2025で全問正解したのですか？ いいえ。技術報告のTable 1と本文によれば、6問中5問（P1からP5）を解いて83.3%を得点し、金メダル相当と評価されています。残るP6は得点していません。 ### Gemini Deep Thinkより強いと考えてよいですか？ ベンチマークの難度によって結果が分かれます。IMO-ProofBenchのbasic集合では99.0対89.0でDeepSeekMath-V2が上回りますが、advanced集合では61.9対65.7でDeep Think（IMO Gold）が上回ります。技術報告も、basic集合で上回りadvanced集合では拮抗していると書き分けています。 ### 生成器と検証器は別々のモデルとして配布されていますか？ いいえ。Hugging Faceで配布されているのは単一のチェックポイントです。技術報告も、すべての実験は最終的な証明生成器という単一モデルを使い、そのモデルが生成と検証の両方を行うと明記しています。 ### 商用利用は可能ですか？ リポジトリと重みはApache License 2.0で提供されるため、商用利用が可能です。再配布する場合は、ライセンス文の交付、変更したファイルへの変更表示、権利表示やNOTICEの保持といった条件を満たす必要があります。 ### 手元のGPU 1枚で動かせますか？ 動きません。配布されている重みはFP8で約689.5GBあり、単一GPUのメモリに収まる規模ではありません。V100やA100はFP8のネイティブ演算にも対応しません。公式のinference/READMEも、重みを変換したうえで`torchrun`で並列実行する前提の手順を示しています。 ### APIやチャットから試せますか？ 公式リポジトリに同梱されている評価スクリプトはAPIエンドポイントを呼ぶ構成で、generate.pyにAPIキーを設定して使います。ただしモデルカードとGitHubのREADMEには、DeepSeekMath-V2を提供する公式APIのモデル名や料金の記載はありません。利用可否は各配信元の提供状況を確認してください。 ## 関連記事 - [GRPOとは？DeepSeekの強化学習アルゴリズムの公式・仕組みとPPOとの違い](https://www.issoh.co.jp/tech/details/5506/)：2024年版が提案した強化学習手法を、目的関数とPPOとの差分から解説しています。 - [DeepSeek-V3.2とは？V3.2-Speciale・DSAの仕組みと性能・使い方・料金を徹底解説](https://www.issoh.co.jp/tech/details/10128/)：V2の土台であるV3.2系の構成と提供形態を確認できます。 - [DeepSeek V4とは？Compressed Sparse Attention(CSA)の仕組みとPro/Flashの性能・料金・移行期限](https://www.issoh.co.jp/tech/details/12053/)：業務用の汎用モデルとして検討する場合の現行世代を扱っています。 - [Lean4とは？入門・インストールからMathlib4・VSCode設定まで](https://www.issoh.co.jp/tech/details/8641/)：機械的に正しさを保証する形式証明側の環境構築を解説しています。 - [セルフコンシステンシーとは？複数サンプリングと多数決の実装・費用設計を実装目線で解説【2026年版】](https://www.issoh.co.jp/tech/details/16464/)：2024年版の60.9%が前提とする、複数サンプリングによる精度向上を扱っています。 --- 出典: [DeepSeekMathとは？V2の自己検証の仕組みとIMO 2025実績・2024年版7Bとの違い]()（株式会社一創）