DeepSeekが数学的推論に特化した「DeepSeek-Prover-V2」をひっそりとリリース、複雑な定理の形式証明に対応

2025年05月01日 11時42分 ソフトウェア

中国のAI企業・DeepSeekが、数学的推論に特化したAI・Proverの第2世代モデルである「DeepSeek-Prover-V2」を、Hugging FaceとGitHubに公開しました。同社の大規模言語モデル「DeepSeek-V3」のアーキテクチャを基盤としたMixture-of-Experts(MoE)モデルで、定理証明支援言語のLean 4を使って形式化した定理証明の生成を自動化するように設計されています。

deepseek-ai/DeepSeek-Prover-V2-671B · Hugging Face

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

deepseek-ai/DeepSeek-Prover-V2 https://github.com/deepseek-ai/DeepSeek-Prover-V2

DeepSeek quietly updates open-source model that handles maths proofs | South China Morning Post

https://www.scmp.com/tech/tech-trends/article/3308566/deepseek-quietly-updates-open-source-model-handles-maths-proofs DeepSeek-Prover-V2は数学的推論に特化したAI・DeepSeek-Prover-V1.5の後継モデルで、DeepSeek-Prover-V1.5-Baseをベースにした7B(70億パラメーター)モデルと、DeepSeek-V3-Baseをベースにした671B(6710億パラメーター)モデルの2種類が提供されています。

7Bモデルは671Bモデルよりも性能面では劣りますが、デプロイと推論に必要なリソースが少なく済み、計算コストが低く実用的。前世代モデルがベースになっていますが、最大32Kトークンのコンテキスト長をサポートしており、長い証明や複雑な推論が必要な問題も扱えます。 671Bモデルの特徴は、DeepSeek-V3を基盤とした「再帰的定理証明パイプライン」で収集されたデータで学習している点です。この再帰的定理証明パイプラインでは、DeepSeek-V3で複雑な定理を分解しながらLean 4で形式化し、7Bモデルで分解した論理を個別に解決します。すべてを解決したら、DeepSeek-V3の非形式的な思考連鎖によって個別の証明を組み合わせ、元の複雑な定理の証明を構築します。671Bモデルはこのプロセスで生成されたデータを使ってファインチューニングが行われており、人間のような推論能力と厳密な形式的証明能力を兼ね備えているとのこと。

DeepSeekは、671Bモデルが数学オリンピックレベルの問題を収録したMiniF2F-testでのベンチマークで88.9％の合格率を達成し、定理証明アルゴリズムのベンチマークであるPutnamBenchで658問中49問を解決できたと報告しており、671Bモデルが定理証明において記事作成時点で最先端の性能を持っていることを示しているとアピールしています。

また、DeepSeekはアメリカの数学オリンピック出場資格認定に用いられるAIMEの試験問題を含む325問で構成された「ProverBench」という新しい定理証明ベンチマークも同時に発表しています。そのうち、2024年と2025年のAIMEで出題された問題15問を用いた性能比較では、671Bモデルは6問解決できたとのこと。DeepSeek-V3が同じAIME問題で8問解けたことを考えると、形式的証明と非形式的推論の性能差が大きく縮まっていることを示しているとDeepSeekは論じました。

DeepSeek-Prover-V2の671Bモデルと7Bモデルは、GitHubとHugging Faceで公開されています。また、Hugging FaceのTransformersライブラリを使用して直接推論を行うことが可能で、ユーザーは複雑なセットアップなしにモデルを簡単に利用開始できます。

DeepSeekは記事作成時点でDeepSeek-Prover-V2のリリースを公式に発表していませんが、香港の英字日刊紙であるSouth China Morning Postは「近日中に発表予定とされる新しい推論モデルのDeepSeek-R2に対する期待が高まる中でのリリースだ」と評しています。なお、South China Morning PostはDeepSeekにコメントを要請しましたが、返答はなかったそうです。