DeepSeekは数学定理証明の分野で専用モデルProver-V2を発表した。目標は、AIを用いてLean 4形式検証システム内で数学定理を自動証明することである。
この方向性が重要な理由
数学定理証明は、AI能力の究極のテストフィールドである。数学は「ほぼ正しい」を認めない。証明は完全に正しいか、間違っているかのどちらかであり、「95%正しい証明」というものは存在しない。
形式検証システム（Lean 4など）は、コンパイラが構文をチェックするように、推論の各ステップをチェックする。一歩でも間違えれば、証明全体がエラーとなる。これはAIの論理的推論能力にとって最も厳しい試練である。
Prover-V2の性能
miniF2Fベンチマークにおいて、Prover-V2は最新のトップ水準に近い、または同等の結果を達成した。その手法はサブゴール分解である。複雑な証明を一連のより小さなサブゴールに分解し、一つずつ攻略していく。
これは人間の数学者の考え方と似ている。難しい問題に直面したとき、「Aを証明するには、まずBとCを証明する必要があり、Bを証明するにはまずDを確認する必要がある…」と考える。
汎用推論モデルとの違い
汎用モデル（GPT、Claude、Gemini）は、数学的推論にChain-of-Thought（連鎖的思考）を用いる。本質的には「自然言語で段階的に推論する」方法である。この方法は単純な問題には効果的だが、複雑な証明ではどこかのステップで論理的欠陥が生じやすい。
Prover-V2は形式化されたルートを採用し、すべてのステップがLean 4によって検証される。利点は「幻覚（ハルシネーション）」が存在しないことだが、欠点は適用範囲が非常に狭く、形式化システム内でしか機能しないことである。
意義
数学定理証明は、一見ニッチに見えるが、影響力の大きい方向性である。AIが形式化システム内で複雑な定理を確実に証明できるようになれば、ソフトウェア検証、ハードウェア検証、暗号証明など、一連の重要な分野に応用できる。
DeepSeekがこの方向性に投資していることは、汎用大規模モデルのベンチマーク競争にのみ注力しているわけではなく、基礎的な科学ツールの構築にも真剣に取り組んでいることを示している。
出典：CocoLoop、DeepSeek Prover-V2論文