脚本プランナー▸ 
AIアプリ 
AIニュース DeepSeekがDeepSeek-Prover-V2-671Bを発表：6710億パラメータのMoEアーキテクチャを採用した次世代自動定理証明モデル
小编 ·
DeepSeekがDeepSeek-Prover-V2-671Bを発表：6710億パラメータのMoEアーキテクチャを採用した次世代自動定理証明モデル
DeepSeek ai は2025年4月30日にDeepSeek-Prover-V2-671Bを発表しました。これは6710億パラメータのMoEアーキテクチャに基づく次世代の自動定理証明モデルで、Lean 4フレームワーク内で証明の生成と検証を行います。その利点には、形式数学を「GPT-4レベル」の規模に引き上げること、MoEによる効率向上、オープンソースで商用利用が可能な点などがあります。V1.5バージョンと比較して、パラメータ数、コンテキスト長、合格率などが大幅に向上しています。miniF2Fなどのベンチマークテストで優れた性能を発揮することが期待され、形式検証や数学研究の加速などの分野で利用可能です。使用時はHugging Faceから重みをダウンロードし、必要な設定を行う必要があります。
技術的な特徴
パラメータ数とアーキテクチャ：モデルの総パラメータ数は6710億で、MoEアーキテクチャを採用しており、1トークンあたり約370億パラメータが活性化されます。このアーキテクチャは強力な推論能力を維持しながら、メモリ要件を大幅に削減します。
コンテキスト長：超長コンテキストをサポートし、最大位置埋め込みは163840に達し、複雑な数学的証明を処理できます。
計算精度：BF16、FP8、F32など複数の計算精度をサポートし、モデルのより高速で省リソースなトレーニングとデプロイを容易にします。
ファイル形式：より効率的なsafetensorsファイル形式を採用しています。
量子化技術：FP8量子化を採用し、量子化技術によりモデルサイズを縮小し、推論効率を向上させます。
主な優位性
規模と複雑さ：巨大なパラメータ数と長いコンテキストウィンドウ（約128kトークン）により、より長く複雑な数学的証明の論理チェーンを処理できます。
効率の最適化：MoEアーキテクチャを採用しており、全結合の6710億パラメータモデルと比較して、メモリ要件を大幅に削減し、推論速度を向上させます。
オープンソースとライセンス：モデルはオープンソースで、重みはHugging Faceで取得可能であり、商用利用も可能と予想されます。
応用シナリオ
形式検証：暗号化のセキュリティ証明やチップ設計の正当性証明における厳密なチェック。
数学研究の加速：数学者が既存の定理を形式化し、新しい予想を探求し、オリンピックレベルの数学問題を解決するのを支援します。
高度な教育ツール：学生が形式証明を完成させるのを指導するインタラクティブな個別指導システムを作成します。
安全性が重要なシステム：コード展開前に、Lean統合を通じて重要なソフトウェアの属性と不変条件を検証します。
クイックスタート手順
モデルの取得：Hugging Faceから重みをダウンロード：deepseek-ai/DeepSeek-Prover-V2-671B。
Leanのセットアップ：Lean 4（推奨：≥4.5バージョン）とmathlib4ライブラリをインストールします。
ハードウェアの確認：ハードウェア構成が最低要件を満たしていることを確認します（高性能構成を推奨）。
推論エンジンのインストール：vLLMやその他のMoE互換フレームワークなどをセットアップします。
サンプルの探索：モデルリポジトリ内の評価スクリプトやサンプルノートブックを確認します。
よくある質問
オープンソースですか？商用利用は可能ですか？
はい、DeepSeek-Prover-V2-671Bはオープンソースで（Hugging Faceで重みを取得可能）、ライセンス契約により学術および商用利用が可能と予想されます。
NVIDIA 4090で動作しますか？
初期報告によると、MoE、MLA、量子化などの最適化技術により、このモデルは単一のNVIDIA 4090 GPUで動作可能とされています。特に、十分なRAMと高速なNVMe SSDを動的ロードに使用できる場合は有効です。具体的な構成によってパフォーマンスは異なります。
関連リンク
Hugging Face：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
Github：https://github.com/deepseek-ai/DeepSeek-Prover-V1.5
詳細紹介：https://deepseeksai.com/prover-v2-671b/
論文：https://arxiv.org/pdf/2408.08152
