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架构，每token激活约370亿参数。这种架构在保持强大推理能力的同时，显著降低了内存需求。

上下文长度：支持超长上下文，最大位置嵌入达163840，能够处理复杂的数学证明。

计算精度：支持BF16、FP8、F32等多种计算精度，方便模型更快、更省资源地训练和部署。

文件格式：使用更高效的safetensors文件格式。

量化技术：采用FP8量化，通过量化技术减小模型大小，提高推理效率。

关键优势

规模与复杂性：巨大的参数量和长上下文窗口（约128k tokens），能够处理更长、更复杂的数学证明逻辑链。

效率优化：采用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