投稿者: 中国の AI 企業 DeepSeek は、数学的推論と定理証明に特化したオープンソースの大規模言語モデル「 DeepSeek-Prover-V2 」を公開しました。このモデルは、非形式的な数学的推論と Lean 4 を用いた形式的な定理証明を組み合わせることで、複雑な数学の定理証明の自動化を実現し、最先端の性能を達成しています。
DeepSeek-Prover-V2 には、70 億パラメータの「 7B モデル」と 6710 億パラメータの「 671B モデル」の 2 種類があります。特に 671B モデルは DeepSeek-V3 を基盤とした Mixture-of-Experts （ MoE ）アーキテクチャを採用し、効率的かつ高精度に複雑な数学的タスクを処理します。このモデルは GitHub および Hugging Face でオープンソースとして公開されており、 MIT ライセンスの下で利用可能です。
このモデルの特筆すべき技術的アプローチとして、「再帰的定理証明パイプライン」と呼ばれるプロセスを採用しています。これは複雑な定理をより小さなサブタスクに分解し、それぞれを解決した後に統合する手法です。また、「 non-Chain-of-Thought モード」と「 Chain-of-Thought モード」の 2 つの証明生成モードをサポートし、効率と精度のバランスを取っています。
ベンチマークテストでは、 MiniF2F-test で 88.9% の合格率を達成し、 Putnam Bench の 658 問中 49 問を解決。さらに、新たに導入された ProverBench に含まれる AIME 問題 15 問中 6 問の解決に成功しました。
DeepSeek はこのモデルの公式発表を行っていませんが、 Alibaba が競合モデル「 Qwen3 」を発表した翌日に静かに公開され、同社の次世代モデル「 DeepSeek-R2 」への期待が高まる中での動きとして注目されています。