DeepSeek 发布 Prover-V2：671B 参数的数学定理证明模型

DeepSeek 于 2025 年 4 月 30 日发布 DeepSeek-Prover-V2-671B，一款锁定“数学定理证明”的专用模型。它构建于支撑 DeepSeek-V3 的 671B 参数混合专家（MoE）架构之上，任务聚焦在 Lean 4 这套形式化证明辅助工具框架中，自动生成并验证数学证明的正确性。官方公布的基准测试显示，该模型在 MiniF2F-test 测试集上达到 88.9% 的通过率，并在难度更高的 PutnamBench 题库（收录美国大学生数学竞赛 Putnam 的题目）658 题中解出 49 题。模型以开源形式发布于 Hugging Face，并附带允许商业使用的授权条款。

技术意义：MoE 架构把“推理成本”压下来

模型总参数量高达 671B，但采用 MoE 设计，每次生成一个 token 时只实际启用约 370 亿参数，其余专家模块保持休眠。这种“按需唤醒”机制让 DeepSeek 得以维持大规模知识容量，同时把单次推理成本压低到接近中型模型的水平。对形式化证明这种需要反复尝试、验证、回溯的任务而言，推理效率直接决定模型能在有限时间内探索多少条证明路径，这也是 Prover-V2 敢于挑战 Putnam 级别题目的底气所在。

与前代及同类模型的比较

形式化定理证明是相对窄但技术门槛极高的 AI 应用领域，此前形式化证明领域的先进成果多集中在少数顶尖实验室。DeepSeek 此次选择以开源、可商用授权的方式发布 Prover-V2，等于是把原本集中在少数实验室的能力，以低成本方式开放给全球研究者与企业使用。这延续了 DeepSeek 自 R1 以来一贯的策略：用开源模型快速抢占特定垂直技术领域的话语权，而非只做通用对话模型的军备竞赛。

业界反应：开源策略持续施压

Prover-V2 发布的时间点，正好落在 DeepSeek 酝酿下一代旗舰模型“R2”之前，被外界解读为技术实力的预热动作。对其他 AI 厂商而言，DeepSeek 一再以开源、免费商用的形式发布高规格模型，持续压缩闭源模型厂商的定价与差异化空间，也让“数学推理能力”成为继代码生成之后，另一个开源阵营急起直追的战场。

对管理者的意义

Prover-V2 本身是高度学术化的工具，多数管理者不会直接使用，但它反映的趋势值得留意：AI 在“需要严谨逻辑、可验证正确性”的任务上正快速进步，未来财务模型审核、合同条款一致性检查、工程规格验算等讲求“零错误”的管理场景，都可能出现对应的 AI 辅助工具，值得持续关注同类技术何时走向企业应用。