DeepSeek-Prover-V2 の内側：なぜこの6710億パラメータモデルがAIの数学的推論の未来の要となるのか
2025年4月30日、中国の祝日の直前に、DeepSeek は、ニッチでありながら、人工知能の基盤として重要な分野である形式的な数学的推論において、大きな波を起こしているモデルを静かに発表しました。より広範な AI レースがチャットボットの個性や派手なマルチモーダルデモに焦点を当てている一方で、DeepSeek は、目立たないものの戦略的に重要な分野、つまり自動定理証明に力を注いでいます。
DeepSeek-Prover-V2 は、最新のオープンウェイトリリースであり、ソーシャルメディアで話題になることはないかもしれませんが、その影響は学界、工学、そして将来の AGI システムに広がります。6710億のパラメータバックボーンと Lean 4 形式証明との深い統合により、数学の問題を解くだけでなく、数学的真実をコードで形式化します。長期投資家、研究機関、AI インフラストラクチャの関係者にとって、このモデルは単なる好奇心ではありません。それはベンチマークであり、おそらく青写真です。
数学エンジンのコールドスタート—DeepSeek が定理証明 LLM をどのように訓練するか
DeepSeek-Prover-V2 は、既存のモデルを単に微調整したものではありません。その中心的な革新は、データが非常に少ないドメインでモデルをトレーニングするための合成「コールドスタート」データを生成する方法にあります。
その理由を理解するために、次のことを考えてください。形式的な証明は、自然言語とは異なり、厳格なロジック、厳密な構文、および検証可能な結果を必要とします。許容範囲はありません。曖昧さやスタイルのばらつきの余地はありません。
DeepSeek の答えは？独自の基盤モデルである DeepSeek-V3 を教師として使用します。パイプラインは、複雑な数学的定理を構造化された一連のサブゴールに分解し、それぞれを Lean 4 経由で形式ロジックに変換します。これらの証明ステップは、効率のために最初に小さい 7B モデルによって処理され、解決されると、一貫した連鎖思考推論トレースに織り込まれ、合成コールドスタートデータセットを形成します。
この再帰的な生成フレームワークは、単に賢いだけでなく、スケーラブルです。DeepSeek は基本的に、数学者が問題を分解する方法を模倣した自己学習ループを構築しました。考え、単純化し、証明し、合成します。
データから強化へ—検証済みの推論によるトレーニング
コールドスタートデータが合成されると、DeepSeek は強化学習に移行します。ただし、人間がラベル付けしたデータではなく、検証可能な結果が得られる問題を使用します。モデルはバイナリフィードバックを受け取ります。正しい証明が生成されたかどうかです。
このフィードバックループは、非形式的な推論 (LLM の自然なドメイン) と形式的なロジック (Lean 4 の厳密なドメイン) を橋渡しします。最終的な結果である DeepSeek-Prover-V2-671B は、単に言葉で推論するだけではありません。機械や数学者が行ごとに検証できる証明を生成しています。
パフォーマンスの数値は、その有望性を示しています。
- MiniF2F テスト (数学的推論のベンチマーク) で 88.9% の合格率
- エリートレベルの数学チャレンジのセットである PutnamBench で 658 問中 49 問を解決
背景として、これらの数値はニューラル定理証明の最先端を押し上げています。画像生成や対話エージェントほど華やかには聞こえないかもしれませんが、基盤となる機能は、堅牢で信頼性の高い AI 推論システムにはるかに転用可能です。
ProverBench—形式化された数学評価の新しい標準
モデルに加えて、DeepSeek は ProverBench、325 の厳密に形式化された問題のデータセットをリリースしました。これには以下が含まれます。
- 最近の AIME コンテスト からの 15 の問題
- 代数、微積分、実数および複素解析、確率などの主要な数学ドメインからの数十の問題
これが重要なのは、形式的な定理証明の以前のデータセットが、合成的すぎるか、狭すぎたかのどちらかであったためです。ProverBench はバランスをもたらします。現実世界の教育的関連性、競争力のある問題の難易度、および多様な数学的構造です。
データセットの内訳:
| ドメイン | 問題数 |
|---|---|
| 微積分 | 90 |
| 線形代数 | 50 |
| 抽象代数 | 40 |
| 数論 | 40 |
| AIME | 15 |
| その他 | 90 |
モデルとこのベンチマークの両方をリリースすることで、DeepSeek は単に能力を誇示するだけでなく、厳密な比較とオープンな実験を促しています。
投資家の影響—なぜこのニッチが重要なのか
カジュアルな観察者にとって、形式的な定理証明は研究の自己満足プロジェクトのように見えるかもしれません。しかし、AGI レースを追跡している人にとっては、パターンがより明確になっています。DeepSeek のロードマップは、以下を優先します。
- 数学およびコーディングモデル
- マルチモーダル統合
- 自然言語推論
そしてその順序で。
Prover-V2 のような数学モデルが投資および戦略の観点から特に魅力的なのは、その 検証可能性 です。ハルシネーションが LLM のアキレス腱である世界では、定理証明器はまれな利点を提供します。決定論的な正確さです。証明が成り立つか、成り立たないかのどちらかです。
数人の専門家は、DeepSeek-Prover-V2 は最終目標ではなく、戦略的な 足がかり であるとほのめかしています。ある内部関係者は、これを DeepSeek の今後の汎用モデル (潜在的に V4 または R2 というコードネーム) の「データシンセサイザー」と呼びました。これらの将来のシステムは、Prover-V2 の厳密な推論を、より広範で一般的なモデルに統合し、人間のレベルの精度でドメイン全体でコードを作成し、記述し、問題を解決することができます。
言い換えれば、DeepSeek は、検証可能で説明責任のある AGI システムの基盤を静かに構築している可能性があります。これは、単なる単語予測を超えて、論理的推論と信頼できる出力につながるものです。
技術アクセスとオープンウェイトリリース
クローズドモデルがますます一般的になっている業界で、DeepSeek が Prover-V2 を 7B と 671B の両方の構成でオープンウェイトにすることを決定したのは注目に値します。特に教育、研究、および Lean 4 のツールチェーン開発において、グローバルなコラボレーションと実験を促します。
どちらのモデルも Hugging Face で入手でき、Transformers 経由で簡単に統合できます。より大きな 671B モデルは DeepSeek-V3 アーキテクチャを反映しており、最大 32K のコンテキスト長と推論対応のパフォーマンスを提供します。
サンプル推論には、次のものを含む完全な Lean 4 コード生成が含まれます。
- 定理の定式化
- 証明計画の生成
- Lean 構文を使用した形式的な証明の実行
AI の未来が形式的である可能性がある理由
要約すると、DeepSeek-Prover-V2 は、楽しみのために教科書の問題を解くことではありません。AI の検証問題 を一度に 1 つの形式的な証明で解決することです。
主なポイント:
- 再帰的証明合成により、スケーラブルなコールドスタート学習が可能になります
- このモデルは、非形式的な LLM 推論と形式的な証明構造を融合します
- 主要な数学ベンチマークで以前のモデルよりも優れています
- 将来の評価のための新しいオープンベンチマーク (ProverBench) を導入します
- 検証可能なインテリジェンスに焦点を当てた、より広範な AGI 戦略を示しています
AI 投資家、研究機関、および高度なエンジニアリングチームにとって、DeepSeek の形式的な定理証明作業は、次世代の AI 能力がどこに向かっているのかを示す最も明確なシグナルである可能性があります。それは、より広範な会話ではなく、より深く、証明可能な思考に向かっています。
今後の DeepSeek R2: AI の強力な新しい競争相手
中国のテクノロジー企業である DeepSeek の次期 AI モデルである DeepSeek R2 は、その印象的な仕様とコスト上の優位性により、西側の AI の優位性に挑戦する準備ができています。2025 年 5 月上旬にリリースされる予定の R2 は、ハイブリッド Mixture-of-Experts アーキテクチャを特徴とし、パラメーターは前任者の 2 倍である 1.2 兆個になると報告されています。このモデルは、Huawei の Ascend 910B チップクラスターを使用して 5.2 ペタバイトのデータでトレーニングされ、82% のハードウェア使用率で 512 ペタフロップスの驚異的な計算効率を達成すると噂されています。
R2 の期待される機能には、推論の強化、画像とビデオのマルチモーダルサポート、高度なコーディング能力、および R1 の中国語と英語の能力を超える多言語サポートの拡張が含まれます。おそらく最も破壊的なのは、DeepSeek が報告しているコスト上の優位性です。R2 は、OpenAI の GPT-4o よりも構築コストが 97.3% 安く、エンタープライズ価格は 100 万入力トークンあたりわずか 0.07 ドルになると予想されています。このコスト効率と、主要な西洋モデルと同等または潜在的に優れたパフォーマンスとの組み合わせにより、DeepSeek R2 はグローバル AI 環境における重要な挑戦者としての地位を確立しています。これらの仕様は、公式リリースまでほとんど確認されていませんが、DeepSeek が次世代モデルを発表する準備を進めているため、AI コミュニティは注意深く見守っています。