DeepSeek-Prover-V1（ディープシーク プルーバー ブイワン）
DeepSeek AIが2024年5月に発表した形式定理証明（Formal Theorem Proving）特化LLM。Lean 4形式言語でMathLibベースの数学定理を機械検証可能な形で証明し、miniF2F-testで64.2%・ProofNet-testで25.3%を達成。V1.5では88.9%まで向上。
DeepSeek-Prover-V1 とは
DeepSeek-Prover-V1は、DeepSeek AIが2024年5月に発表した形式定理証明（Formal Theorem Proving）に特化した大規模言語モデル。通常の数学LLMが「答えを出す」のに対し、ProverはLean 4という定理証明支援言語で証明を記述し、コンパイラが機械的に正しさを検証できる形式で証明を生成する点が根本的に異なる。
形式定理証明 vs 自然言語数学
自然言語数学（従来LLM）: 人間が読んで「正しそう」と判断するだけ。誤りが紛れ込む余地がある。
Lean 4形式定理証明:
theorem sqrt2_irrational : ¬ ∃ (p q : ℤ), q ≠ 0 ∧ Nat.sqrt 2 = p / q := by
-- コンパイラが100%確実に証明の正確性を検証
...
→ コンパイラが通過すれば数学的に完全に正しいことが保証される。
Lean 4 と MathLib
- Lean 4: Microsoftが主導する定理証明支援システム兼プログラミング言語
- MathLib: Lean 4向けの数学ライブラリ（10万以上の定理・補題を収録）
- DeepSeek-Prover-V1はMathLibの証明済み補題を組み合わせて新しい定理を証明する
パイプライン
- 形式化: 自然言語の数学問題をLean 4構文に変換
- 証明生成: LLMがLean 4戦術（
ring,norm_num,apply,simp等）を生成 - コンパイラ検証: Lean 4が証明を検証。通過しなければ再試行
性能指標
| バージョン | miniF2F-test | ProofNet-test |
|---|---|---|
| DeepSeek-Prover-V1 | 64.2% | 25.3% |
| 従来最良（COPRA等） | ~47% | ~14% |
| DeepSeek-Prover-V1.5 | 88.9% | - |
miniF2F: 高校数学（AMC/AIME/数学オリンピック相当）244問 ProofNet: 学部レベルの分析・代数・位相数学
V1.5への発展
DeepSeek-Prover-V1.5（2024年8月）:
- RMaxTS（MCTS統合）: 証明探索にモンテカルロ木探索を採用
- Process Reward Model: 証明ステップの品質評価
- miniF2F-testで88.9%に到達（V1比+24.7pt）
応用と意義
- AI for Mathematics: LLMが「確実に正しい数学」を生成できる第一歩
- ソフトウェア検証: 形式証明技術はプログラムの正確性検証にも転用可能
- 2025年AI-IMO: 形式定理証明を用いたAIの数学オリンピック挑戦が注目
FAQ
Q: DeepSeek-Prover-V1のパラメータ数は？ A: 7Bパラメータ。ベースはDeepSeekMath-7B-Base。
Q: Lean 4を知らないとDeepSeek-Proverを使えないか？ A: 自然言語入力を形式化するパイプラインが内蔵されている。ただし出力解釈にLean 4の基礎知識があると望ましい。
Q: 一般LLMとの根本的な違いは？ A: 一般LLMは「もっともらしい答え」を生成するが誤りも多い。DeepSeek-Proverは「コンパイラが検証した確実に正しい証明」のみを出力する。ただしLean 4で表現できる問題ドメインに限定される。