AIwiki

DeepSeek-Prover-V2

ファインチューニング
開発者
DeepSeek AI
ライセンス
DeepSeek Model License
リリース日
2025/4/30
コンテキスト長
163,840 トークン
対応言語
en, lean4
知識カットオフ
2025-Q2
ベースモデル
deepseek-v3
officialtheorem-provinglean4formal-verificationlong-contextopen-source

DeepSeek AIの第2世代定理証明器。2025年4月公開。Lean 4形式言語対応。163,840トークンの超長コンテキスト。7Bと671Bの2サイズ展開。MiniF2F 88.9%達成。

HuggingFace論文GitHub

ベンチマーク

minif2f
88.9

ソース: https://arxiv.org/abs/2504.21801

技術仕様

アーキテクチャ

Formal theorem proving for Lean 4, Ultra-long context

パラメータバリエーション

DeepSeek-Prover-V2-7B(7B)

HuggingFace

7B軽量版定理証明器。32Kコンテキスト。

VRAM4GB

GGUFファイルは登録されていません

DeepSeek-Prover-V2-671B(671B)

HuggingFace

671Bフルサイズ定理証明器。MiniF2F 88.9%達成。

MoEアクティブパラメータ: 37B
VRAM369GB

GGUFファイルは登録されていません

関連モデル

DeepSeek-LLM

4 バリエーション

DeepSeek-Coder

7 バリエーション

DeepSeekMoE

2 バリエーション

DeepSeek-Math

3 バリエーション

DeepSeek-VL

2 バリエーション

DeepSeek-V2

4 バリエーション

DeepSeek-Coder-V2

4 バリエーション

DeepSeek-Prover

1 バリエーション

DeepSeek-V2.5

1 バリエーション

DeepSeek-V3

2 バリエーション

DeepSeek-VL2

3 バリエーション

DeepSeek-R1

8 バリエーション

Janus

3 バリエーション

DeepSeek-R1-0528

1 バリエーション

DeepSeek-V3.1

1 バリエーション

DeepSeekMath-V2

1 バリエーション

DeepSeek-V3.2

1 バリエーション

家系図

現在のモデル: DeepSeek-Prover-V2