团队赶放假，DeepSeek-Prover V2 671B开源发布

来源——AMP实验室

幻方量化又做空了

DeepSeek 昨日下午，在 AI 开源社区 Hugging Face 发布了一个名为 DeepSeek-Prover-V2-671B 的新模型。

DeepSeek-Prover-V2-671B 使用了更高效的 safetensors 文件格式，并支持 BF16、FP8、F32 等多种计算精度，方便模型更快、更省资源地训练和部署。

从命名上看，这款参数高达 6710 亿的模型可能是去年发布的数学 AI 模型 Prover-V1.5 的升级版。

DeepSeek-Prover 是由 DeepSeek 团队开发的开源数学大模型系列，其核心功能是专注于形式化数学定理的自动证明与验证，尤其是在数学推理的严谨性和逻辑性上具有显著优势。相较之下，通用模型（如 GPT-4）虽在广泛任务中表现优异，但缺乏内置验证机制，难以保证数学证明的精确性。

最新的V2-671B版本则在多个方面实现了突破，其参数量跃升至 6710 亿，采用混合专家架构（MoE），每层包含 256 个路由专家和 1 个共享专家，支持动态分配计算资源，显著提升复杂逻辑的解析效率。

此外，V2-671B引入多头潜注意力（MLA）架构压缩键值缓存（KV Cache），降低推理内存占用，结合 FP8 量化技术提升计算效率超 40%，并扩展上下文窗口至 163,840 tokens，覆盖长证明流程。

最后是算法升级，新V2强化 RMaxTS 算法驱动探索多样性证明路径，优化截断-恢复机制平衡生成与验证效率，并通过三阶段训练（预训练、监督微调、强化学习）增强领域适配性，尤其在形式化语言（如 Lean 4）的生成稳定性上表现突出。这些改进使其在学术研究、工业验证等场景中展现出更强的专业性与实用性。