数日前、DeepSeek-R2 のリリースに関する噂が広まっていましたが、DeepSeek には新しい動きがありました。しかし、皆が待っていた R2 ではなく、DeepSeek-Prover-V2 が登場しました。もちろん、こちらもオープンソースです。
Prover-V2 は定理証明の分野で業界最高のパフォーマンスを実現し、MiniF2F テストでは 88.9% の合格率を達成し、AIME 24、25 でも良いスコアを記録しました。4 月 30 日の夜、機械学習協力プラットフォーム HuggingFace では、DeepSeek-Prover-V2 のいくつかの技術的詳細が更新されました。
今回、DeepSeek チームは DeepSeek-Prover-V2 モデルの 2 つのバージョンをリリースしました。パラメータの規模はそれぞれ 7B と 671B です。その中で、DeepSeek-Prover-V2-671B は DeepSeek-V3-Base を基にトレーニングされ、DeepSeek-Prover-V2-7B は DeepSeek-Prover-V1.5-Base を基に構築され、最大 32K トークンのコンテキスト長の拡張をサポートしています。
- DeepSeek-Prover-V2-7B リンク：DeepSeek-Prover-V2-7B
- DeepSeek-Prover-V2-671B リンク：DeepSeek-Prover-V2-671B
DeepSeek-Prover-V2 を一言でまとめると？それは「数学 AI プログラミング言語」Lean 4 のために特別に設計されたオープンソースの大規模言語モデルで、形式的な定理証明に特化しています。
その初期データは、DeepSeek-V3 によって駆動される再帰的な定理証明プロセスを通じて収集されました。コールドスタートのトレーニング段階では、まず DeepSeek-V3 が複雑な問題を一連の解決可能なサブゴールに分解します。各サブゴールを解決するたびに、これらの証明が「思考の連鎖」として統合されます。そして、DeepSeek-V3 の逐次的な推論の軌跡を融合させ、強化学習のための初期トレーニングデータを共同で構築します。
この戦略の巧妙さは、非形式的および形式的な数学的推論を統一されたモデルに融合できることです。これにより、モデルは人間のように柔軟に考え、機械のように厳密に証明することができ、数学的推論の統合的な融合を実現しました。
技術概要#
再帰的証明検索によるコールドスタート推論データの生成#
コールドスタートデータセットを構築するために、DeepSeek チームはシンプルで効率的な再帰的定理証明プロセスを設計し、DeepSeek-V3 を統一ツールとして使用し、サブゴールの分解と推論ステップの形式的表現の両方を担当します。具体的なプロセスは、DeepSeek-V3 が定理を高レベルの証明スケッチに分解するように促すことで進行し、その過程でこれらの推論ステップを Lean 4 言語で形式化し、最終的に構造が明確で論理的に厳密なサブゴールの一連を生成します。
DeepSeek-Prover-V2 はコールドスタートデータ収集プロセスの概要を使用します。計算コストを削減することは、DeepSeek チームの得意分野であり、今回も例外ではありません。彼らは、各サブゴールの証明検索を完了するために、より小さな 7B モデルを使用して計算負担を軽減します。複雑な問題が分解された各ステップが成功裏に解決されると、彼らは完全な形式的逐次証明を DeepSeek-V3 が生成した思考の連鎖に対応させ、コールドスタート推論データを組み合わせます。
合成コールドスタートデータに基づく強化学習#
DeepSeek チームは、挑戦的な定理問題の一部を選びました。7B 証明モデルはそれらをエンドツーエンドで解決することはできませんが、分解された一連のサブゴールを把握することができます。すべてのサブゴールの証明を統合することで、元の問題の完全な形式的証明を構築できます。その後、その正式な証明を DeepSeek-V3 が生成した思考の連鎖に追加し、この思考の連鎖は対応する補題の分解プロセスを示し、非形式的推論とその後の形式的プロセスを密接に融合させたトレーニングデータを形成します。
証明モデルに合成コールドスタートデータの微調整を行った後、研究チームはさらに強化学習段階を導入し、非形式的推論を形式的証明に変換するモデルの能力を向上させました。トレーニングプロセスでは、推論モデルの一般的な目標に従い、「正 / 誤」の二値フィードバックを主要な報酬信号として採用します。
最終的に得られたモデル DeepSeek-Prover-V2-671B は神経定理証明タスクで現在の最先端の性能を達成し、MiniF2F-test での合格率は 88.9% に達し、PutnamBench データセットの 658 問のうち 49 問を成功裏に解決しました。DeepSeek-Prover-V2 が miniF2F データセット上で生成したすべての証明は ZIP ファイルに整理されており、ダウンロード可能です。
- ダウンロードリンク：miniF2F 解決策