プットナムテストでは、新モデルDeepSeek-Prover-V2が49問正解という記録を直接更新しました。
現在の1位は657問中わずか10問で、KimiとAIME2024優勝チームNuminaとの共同研究成果であるKimina-Proverでした。
定理証明に最適化されていないDeepSeek-R1はわずか1問でした。
まだ発表されていないR2への期待が高まります。
評価結果に加え、論文では「強化学習による新スキルの発見」現象が特別に報告されています。
R1が「アハ体験」をもたらしたように、Prover-V2にも予期せぬ能力があります。
具体的には、プットナムテストにおいて、パラメータ数の少ないDeepSeek-Prover-V2-7Bは、非CoT生成モードで671Bモデルが解決できなかった13問を解決しました。
チームがこのモデルの出力を注意深く検査したところ、その推論方法に独特のパターンがあることがわかりました。7Bモデルは有限基数に関する問題を扱う際に、Cardinal.toNatやCardinal.natCast_injを頻繁に使用しますが、671Bモデルの生成出力にはこれらの内容が明らかにありませんでした。
注意すべきは、7BモデルはDeepSeek-Prover-V1.5-Baseモデルを基盤に、まず671Bモデルが強化学習段階で収集したデータを使用してファインチューニングを行い、その後強化学習を実行して得られたということです。
つまり、7Bモデルは671Bモデルが習得できなかった新しいスキルを習得したのです。
形式化された数学的証明と非形式化された数学的証明の統一モデル
DeepSeekの数学的定理証明モデル、DeepSeek-Proverシリーズはこれまでに3つのモデルを発表しています：
2024年3月のDeepSeek-Prover（以下、Prover-V1と略記）
2024年8月のDeepSeek-Prover-V1.5（以下、Prover-V1.5と略記）
2025年5月のDeepSeek-Prover-V2（以下、Prover-V2と略記）
Prover-V1は主に、大規模な合成データセットによるDeepSeek-Math-7Bのファインチューニングを通じて、定理証明を推進することを模索しました。
Prover-V1.5は、これに加えて証明アシスタントからのフィードバックに基づく強化学習（RLPAF）とモンテカルロ木探索手法を導入しました。
Prover-V2はさらに「サブ目標分解の強化学習」を提案し、基盤モデルをDeepSeek-Math-7BからDeepSeek-V3にアップグレードしました。
DeepSeek-V3の高いコンテキストウィンドウと強力な自然言語推論能力を統合し、形式化された数学的証明と非形式化された数学的証明を一つのモデルに統一しました。
Prover-V2はまた、Prover-V1.5が提案したCoTと非CoT生成という二つのモードを継承しています。
次に、Prover-V2の主要な各段階について詳細に紹介します。
再帰的証明探索によるコールドスタート推論データの合成
DeepSeek-V3をサブ目標分解と形式化のための統一ツールとして活用し、コールドスタートデータセットを構築します。DeepSeek-V3に定理を高級な証明スケッチに分解するよう促し、同時にLean 4でこれらの証明ステップを形式化することで、一連のサブ目標を生成します。
より小さな70億パラメータモデルを使用して各サブ目標の証明探索を処理することで、関連する計算負荷を軽減します。困難な問題の分解ステップが解決され次第、完全な段階的な形式化証明とDeepSeek-V3からの対応する思考連鎖をペアにして、コールドスタート推論データを作成します。
合成コールドスタートデータを使用したサブ目標分解の強化学習
チームは、70億パラメータの証明器モデルではエンドツーエンドで解決できなかったものの、分解されたサブ目標はすべて成功したという、一連の挑戦的な問題を慎重に選択しました。
すべてのサブ目標の証明を組み合わせることで、元の問題に対する完全な形式化証明を構築しました。
次に、この証明をDeepSeek-V3の思考連鎖に添付し、対応する補題分解の概要を示し、これにより非形式的推論とその後の形式化を有機的に結合しました。
合成コールドスタートデータで証明器モデルをファインチューニングした後、強化学習段階を実行し、非形式的推論と形式化証明構築を結びつける能力をさらに強化します。推論モデルの標準的な訓練目標に従い、正解または不正解の二値フィードバックを主要な報酬監督形式として使用します。
具体的な訓練詳細
二段階訓練:
DeepSeek-Prover-V2は二段階で補完的な証明生成モードを確立します。
第一段階では効率的な非CoTモードを使用し、Lean証明コードの迅速な生成に焦点を当て、イテレーションとデータ収集を加速します。
第二段階では第一段階の成果に基づき、高精度な思考連鎖（CoT）モードを採用し、中間推論ステップを詳細に説明し、コールドスタートCoTデータで強化学習を行い、複雑な問題の推論能力を向上させます。
エキスパート反復:
非CoTモード訓練はエキスパート反復パラダイムに従い、最適な証明戦略を使用して難題の証明試行を生成し、Leanによる検証を経て、成功したものは教師ありファインチューニング（SFT）データセットに組み込まれます。以前のバージョンと比較して、訓練問題の分布が調整され、追加の問題とサブ目標分解によって生成された問題が導入されました。
教師ありファインチューニング:
DeepSeek-V3-Base-671Bに対して教師ありファインチューニングを行います。訓練コーパスは二つの補完的なソースからのデータを含んでいます：
一つはエキスパート反復によって収集された非CoTデータであり、これらのデータから生成されたLeanコードには中間推論ステップが含まれていませんが、主にLean定理証明エコシステムにおけるモデルの形式検証スキルを強化するために使用されます。
もう一つはコールドスタートCoTデータであり、これらのデータはDeepSeek-V3の高度な数学的推論プロセスを構造化された証明経路に精緻化し、数学的直感を形式証明構造に変換する認知プロセスを明確にシミュレートします。
強化学習:
GRPOアルゴリズムを採用します。従来のPPOとは異なり、GRPOは個別の批評家モデルを必要としません。それは、各定理プロンプトに対して候補証明のセットをサンプリングし、それらの相対的な報酬に基づいてポリシーを最適化することで機能します。
訓練プロセスでは二値報酬メカニズムが使用され、生成されたLean証明が正しく検証された場合は1、それ以外の場合は0の報酬が得られます。
学習効果を確実にするために、十分な挑戦性がありながらも教師ありファインチューニングされたモデルによって解決可能な問題のみを含むように、訓練プロンプトを慎重に選択しました。
DeepSeek-Prover-V2 7Bの蒸留
DeepSeek-Prover-V1.5-Base-7Bのコンテキストウィンドウを32768トークンに拡張し、DeepSeek-Prover-V2-671Bデータでファインチューニングを行い、非CoT証明データを組み込むことで、小さなモデルが簡潔な形式化出力を生成できるようにし、費用対効果の高い証明オプションを提供します。
さらに、DeepSeek-Prover-V2-7Bに対して、671Bモデルの訓練と同じ強化学習段階を実行し、そのパフォーマンスをさらに向上させます。
これにより得られたモデルProver-V2 671Bは、神経定理証明において最先端のパフォーマンスを達成し、miniF2Fテストで88.9%の合格率を記録し、プットナムテストでは49問を解決しました。Prover-V2がminiF2Fデータセットに対して生成した証明は別途ダウンロード可能です。
ProverBench：AIMEと教科書問題の形式化
Prover-V2と共にProverBenchという325問のベンチマークデータセットを発表します。そのうち15問は、最近のAIME（American Invitational Mathematics Examination 24および25）の数論と代数問題から形式化されたもので、現実的な高校競技レベルの課題を提供します。残りの310問は、厳選された教科書の例や教育チュートリアルから採取されたもので、多様で教育ニーズに基づいた形式化された数学問題のコレクションを構成しています。このベンチマークは、高校競技問題と学部レベルの数学問題をより包括的に評価することを目的としています。
DeepSeek-Prover-V2シリーズの3つのデータセットでの最終的な合計成績は以下の通りです：
DeepSeekオールスターラインナップ
Prover-V2の著者は合計18名で、共同第一著者のZ.Z. Ren、邵智宏、辛華剣は、V3、R1、およびProverシリーズの前作に参加した主力メンバーです。
著者リストには、これまでの二世代（Prover-V1、Prover-V1.5）の研究に参加していなかった何人かの研究者が登場しています。
例えば、清華大学の学部卒・修士であるShirong Maです。公開情報によると、彼は昨年卒業後すぐにDeepSeekに入社し、現在はDeepSeekの研究員を務めており、これまでにDeepSeek LLM v1からR1、DeepSeek-Coderなどの仕事に参加しています。
Zhe Fu、Yuxuan Liuもいます。
彼らはProver-V1、Prover-V1.5の著者リストには含まれていませんでしたが、いずれもDeepSeekのベテランメンバーです。
Prover-V1/V1.5と同時期に発表された《Fire-Flyer AI-HPC》研究でもその署名が見られます。
この研究で提案されたFire-Flyer AI-HPCアーキテクチャは、ソフトウェアとハードウェアの協調設計により訓練コストを削減し、従来のスーパーコンピュータアーキテクチャのAI訓練ニーズに対する不足を解決します。
ただし、今回のProver-V2の論文では、訓練または推論インフラストラクチャに関する具体的な最適化戦略については言及されていません。
最後に、新しい顔としてHongxuan Tangがいますが、具体的な情報については現時点では不明です。
Prover-V2発表後、コミュニティの注目を集め、GitHubリポジトリは12時間以内に350以上のスターを獲得しました。
X（旧Twitter）やHugging Faceなどのプラットフォームでは、ネットユーザーたちが熱烈な議論を繰り広げています。
Prover-V2のコア貢献者である邵智宏は、自身の個人アカウントで積極的に研究成果を宣伝しました。
Xのエンジニア@kacheは特に賞賛しました：
オープンサイエンス研究への献身に感謝します。
プリンストン大学助教授のChi Jin氏は次のように述べています：
この素晴らしい仕事に祝福を！miniF2Fで最後の10%-20%の問題を克服したことは、能力の重大な飛躍を示しています。現在の形式的数学分野の競争状況は激しく、Kiminaがわずか2週間SOTAを維持しただけでDeepSeekに追い越されたことは信じがたいです。
Kimina-Proverのコア貢献者である@Marco Dos Santosでさえ、祝福を送りに来ました：
DeepSeek AIチームがminiF2FタスクのSOTAを89%に引き上げたことをお祝いします！
長いCoTメソッドが他のチームによって独立して探索され、興味深い違いを示しているのを見るのは素晴らしいことです。形式的数学は今日、これまで以上に人気があります！
さらに、ネットユーザーたちの最も関心のある問題は依然として「R2はいつリリースされるのか？」ということです。
論文：
https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf
モデル：
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
DeepSeek-Prover
https://arxiv.org/abs/2405.14333
DeepSeek-Prover-V1.5
https://arxiv.org/abs/2408.08152
参考文献：
[1]https://trishullab.github.io/PutnamBench/leaderboard.html
[2]https://x.com/zhs05232838/status/1917600755936018715