DeepSeek、DeepSeek-Prover-V2を発表：再帰的証明検索と新しいベンチマークによるニューラル定理証明の進展

DeepSeek AIは、Lean 4環境での形式定理証明向けに設計されたオープンソース大規模言語モデルDeepSeek-Prover-V2のリリースを発表しました。この最新版は、革新的な再帰的定理証明パイプラインを導入し、DeepSeek-V3の力を活用して高品質な初期化データを生成します。結果として得られたモデルはニューラル定理証明で最先端の性能を達成し、数学的推論能力を評価するための新しいベンチマークProverBenchも併せて公開されました。

先駆的なコールドスタート推論データ生成

DeepSeek-Prover-V2の重要な革新点は、独自のコールドスタート訓練手順にあります。このプロセスでは、まず強力なDeepSeek-V3モデルに複雑な数学定理を一連の管理しやすいサブゴールに分解するよう促します。同時に、DeepSeek-V3はこれらの高レベル証明ステップをLean 4で形式化し、サブ問題の構造化シーケンスを効果的に作成します。

各サブゴールの計算集約的な証明検索を処理するために、研究者らはより小規模な7Bパラメータモデルを採用しました。難しい問題のすべての分解ステップが正常に証明されると、完全なステップバイステップの形式証明がDeepSeek-V3の対応する思考連鎖推論とペアリングされます。この巧妙なアプローチにより、モデルは非形式的な高レベル数学推論と厳密な形式証明の両方を統合した合成データセットから学習でき、その後の強化学習のための強力なコールドスタートを提供します。

強化された推論のための強化学習

合成コールドスタートデータに基づき、DeepSeekチームは7B証明器がエンドツーエンドで解決できないが、すべてのサブゴールが正常に処理された挑戦的な問題を厳選しました。これらのサブゴールの形式証明を組み合わせることで、元の問題の完全な証明が構築されます。この形式証明は、補題分解を概説するDeepSeek-V3の思考連鎖とリンクされ、非形式的推論と形式化を統合した統一訓練例を作成します。

証明器モデルはこの合成データで微調整され、その後強化学習段階に入ります。この段階では、バイナリの正誤フィードバックを報酬信号として使用し、非形式的数学的直感と正確な形式証明構築の間のギャップを埋めるモデルの能力をさらに洗練します。

最先端のパフォーマンス

この革新的な訓練プロセスの成果は、6710億パラメータを持つDeepSeek-Prover-V2–671Bです。このモデルは顕著な結果を達成し、ニューラル定理証明で最先端の性能を示しています。MiniF2Fテストで88.9%の合格率を達成し、PutnamBenchの658問題のうち49問題を解決しました。DeepSeek-Prover-V2がminiF2Fデータセット用に生成した証明は公開ダウンロード可能で、さらなる精査と分析が可能です。

ProverBenchの導入：新たな評価基準

モデルリリースに加えて、DeepSeek AIは325問題からなる新しいベンチマークデータセットProverBenchを導入しました。このベンチマークは、さまざまな難易度レベルの数学的推論能力のより包括的な評価を提供することを目的としています。

ProverBenchには、最近のAIME（アメリカ招待数学試験）コンテスト（AIME 24および25）から形式化された15問題が含まれており、高校コンテストレベルの本格的な課題を提供します。残りの310問題は、厳選された教科書の例と教育的チュートリアルから引用されており、さまざまな分野にわたる多様で教育学的一貫性のある形式化された数学問題のコレクションを提供します。

ProverBenchは、挑戦的なコンテスト問題と基礎的な学部レベルの数学の両方にわたるニューラル定理証明器のより徹底的な評価を促進することを目的としています。

入手可能性

DeepSeek AIは、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のリリースとProverBenchの導入は、ニューラル定理証明の分野における重要な前進を示しています。再帰的証明検索パイプラインを活用し、挑戦的な新しいベンチマークを導入することで、DeepSeek AIはコミュニティが形式数学のためのより洗練され能力の高いAIシステムを開発し評価できるように力を与えています。