DeepSeek社、数学定理証明向けLLM「Prover-V2」をオープンソースで公開

原文リンク(2025-05-12)

DeepSeek社は、Lean 4における数学定理証明に特化した新しいオープンソースの大規模言語モデルDeepSeek-Prover-V2を公開した。このモデルは、同社の基盤モデルであるDeepSeek-V3を活用した再帰的定理証明パイプラインを基盤として構築されている。Lean 4は、Microsoft Researchが開発した最新バージョンのLean定理証明ツールであり、機械による検証が可能な形式的証明を数学者やコンピュータ科学者が記述できる対話型証明支援システムである。

このプロジェクトは、形式的な数学的推論と非形式的な数学的推論を結びつける一歩を示している。一般的なLLMの能力を活用し、形式的定理証明という構造化された領域に取り組むことを目指している。研究者によれば、このアプローチは複雑な定理をより扱いやすい構成要素に分解することで、人間の証明構築方法論を模倣しているという。

DeepSeekの研究チームは、形式的定理証明評価のために設計された新しいベンチマークコレクションを追加し、評価フレームワークを拡張した。

「標準的なベンチマークに加え、ProverBenchという325の形式化された問題を収録したコレクションを導入した。これには、最近のAmerican Invitational Mathematics Examination（AIME）競技会（24-25年度）から選ばれた15の問題が含まれている」と研究者は説明している。

図1 | 出典：ProverBench - AIMEおよび教科書問題の形式化

これらのAIME問題に対する初期テスト結果は、専門的な定理証明モデルの有望な性能を示している。チームによれば、DeepSeek-Prover-V2は15のAIME問題のうち6つを成功裏に解決し、一般的なDeepSeek-V3モデルは多数決技術を使用して8つを解決したという。

図2 | 出典：DeepSeek-Prover-V2のベンチマーク性能

図3 | 出典：補助定理ステートメントへの分解されたサブゴール

「一般的なモデルは完全なLean証明を生成するのに苦労することが知られているため、DeepSeek-V3には詳細を省略した高レベルの証明スケッチのみを生成するよう指示した。この結果として得られる思考の連鎖は、haveステートメントの一連で構成されるLean定理に結実し、それぞれが解決すべきサブゴールを示す残念なプレースホルダーで終了する。このアプローチは、人間の証明構築スタイルを模倣しており、複雑な定理をより扱いやすい補助定理の連続に段階的に還元するものだ」とチームは述べている。

システムはその後、証明の各構成要素に個別に取り組む方法論的な戦略を採用し、以前に確立された結果を基盤として構築する構造化された定理証明アプローチを作り上げている。

「DeepSeek-V3によって生成されたサブゴールを活用し、再帰的な解決戦略を採用して中間的な証明ステップを体系的に解決する。haveステートメントからサブゴール表現を抽出し、それを元の問題の目標に置き換え（図3(a)参照）、その後、前のサブゴールを前提として組み込む（図3(b)参照）。この構築により、後続のサブゴールが以前のステップの中間結果を使用して解決されることを可能にし、より局所化された依存構造を促進し、簡単な補助定理の開発を容易にする」と研究者は詳述している。

計算資源を最適化するため、システムは分解された補助定理を処理するために特化された小型の7Bパラメータモデルを採用しており、広範な証明検索の計算負担を管理している。このアプローチは、分解されたすべてのステップが成功裏に解決された場合に自動的に導出された完全な証明に結実する。

「アルゴリズムフレームワークは2段階で動作し、補完的な2つのモデルを活用する。DeepSeek-V3は補助定理を分解し、7Bプロバーモデルが対応する形式的証明の詳細を完成させる」と研究者は述べている。

このアーキテクチャは、形式的推論データを合成する自然な道筋を確立し、高度な数学的推論と厳密な形式的検証要件を効果的に統合している。

「7Bプロバーモデルがエンドツーエンドで解決できないが、分解されたすべてのサブゴールが成功裏に解決された難しい問題のサブセットを選定する。すべてのサブゴールの証明を構成することで、元の問題に対する完全な形式的証明を構築する」と研究者は説明している。

技術的な成果にもかかわらず、一部の専門家は実装の詳細について懸念を表明している。Epoch AIの主任数学者であるElliot Glazer氏は、研究に関する潜在的な問題を指摘している。

DeepSeek-Prover-V2論文に関していくつかの懸念があります。誤形式化された例の可能性、Lean zulipでの議論ではPutnamBenchの証明が無意味であり、暗黙の'sorry'（おそらくapply? tacticの中に隠れている）が使われていると示唆されていますが、それは彼らのREPL（読み取り・評価・出力ループ）には報告されていません。

これらの懸念は、形式的検証分野における課題を浮き彫りにしており、実装の詳細が結果の有効性に大きな影響を与える可能性があることを示している。

DeepSeek社は、Prover-V2を2つの異なるモデルサイズで公開している。7Bパラメータ版は、以前のProver-V1.5-Baseを基盤としており、最大32Kトークンの拡張コンテキスト長を特徴としている。一方、より大きな671Bパラメータ版は、DeepSeek-V3-Baseを基盤として訓練されている。両モデルは現在HuggingFaceで利用可能であり、325の形式化された問題を含む完全なProverBenchデータセットも提供されている。形式的定理証明に関心のある研究者や開発者は、これらのリソースにアクセスして、この技術の能力と限界を探求し、分野の専門家が提起した懸念に対処する可能性を模索できる。