刚刚！DeepSeek-Prover-V2-671B 发布，网友：DS 是假期终结者

以下文章来源于MaxAIBox，作者Max

DeepSeek 坏得很，假前给大家送劳动节礼物来了，不过这次不是 DeepSeek-R2。

4 月 30 日，DeepSeek 正式推出 DeepSeek-Prover-V2-671B，标志着 AI 数学推理能力迈入新纪元。

DeepSeek-Prover-V2-671B 是什么？

作为 DeepSeek 开源模型系列的新一代自动定理证明专家，该模型基于与 DeepSeek-V3 相同的 6710 亿参数混合专家（MoE）架构，专为 Lean 4 证明辅助框架中的证明生成与验证而优化。

其 MoE 设计采用动态参数激活机制，单次推理仅调用约 370 亿参数（根据 DeepSeek 官方 MoE 架构报告推测，例如 V3 的技术方案），在保持强大推理能力的同时显著提升计算效率。

核心突破价值

本次发布具有三大里程碑意义：

实现形式化数学的「GPT-4 级」突破：凭借超大规模参数量与约 128k tokens 的上下文窗口，可处理高阶数学证明中特有的复杂长逻辑链。

MoE 架构效能优势：相比稠密的 6710 亿参数模型，大幅降低内存需求并提升运算速度。该技术可能延续了 DeepSeek-V2 的多头潜在注意力机制（MLA），此前已实现 KV 缓存压缩与吞吐量突破。

开放商用许可：延续 DeepSeek Prover V1.5 等前代模型传统，预计在 Hugging Face 开源权重并允许商业应用，为学术与工业界提供普惠化支持。

实际应用场景

该模型为多个领域带来革新可能：

形式化验证：在密码学安全证明、芯片设计验证等自动化流程中实现严格数学检验

数学研究加速：协助数学家完成定理形式化、新猜想探索，乃至奥赛级数学难题的证明推导

智能教育工具：构建可验证步骤的交互式教学系统，引导学生掌握严谨的数学证明方法

关键系统安全：通过Lean集成，在软件部署前直接验证核心代码逻辑的正确性与不变性

技术架构解析

根据 DeepSeek-V3 等前代模型技术脉络，当前披露的核心规格如下：

网友评论

参考：

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B/discussions

https://deepseeksai.com/prover-v2-671b/