DeepSeek发布DeepSeek-Prover-V2-671B：6710亿参数的数学AI模型，推动定理证明自动化

DeepSeek在今天悄悄地升级了其专注于数学定理证明和推理的 AI 模型DeepSeek-Prover。最新版本
DeepSeek-Prover-V2-671B已于今天在Hugging Face 上发布。这一升级标志着 DeepSeek 在形式化数学和逻辑推理领域的进一步突破。

• 模型：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

Prover-V2 的技术亮点

Prover-V2 是基于 DeepSeek 的 V3 模型构建的，拥有 6710 亿参数，并采用了混合专家（MoE）架构。这种架构通过将复杂任务分解为多个子任务，并交由专门的“专家”组件处理，从而显著提升了模型的效率和能力。

Prover-V2 的基础是 DeepSeekMath-Base，这是一个专为数学任务设计的模型。经过针对数学定理证明任务的强化训练，Prover-V2 不仅能够解决复杂的数学问题，还能自动生成完整的数学证明过程。这使得它在形式化定理证明和数学推理领域表现尤为突出。

解决了哪些关键问题？

在传统数学研究中，验证定理的正确性和形式化证明一直面临诸多挑战：

1. 人工验证低效且易出错：定理的正确性高度依赖人工逻辑推理，这种方法耗时耗力，且容易因人为疏忽导致错误。
2. 形式化证明门槛高：形式化证明虽然能提高数学的严谨性，但手工编写形式化证明的过程极其繁琐，对研究人员的技术要求也很高。
3. 现有 AI 模型缺乏逻辑推导能力：尽管一些 AI 模型可以生成答案，但它们往往无法提供可验证的逻辑推导过程，难以满足数学研究的严格需求。

Prover-V2 的出现有效缓解了这些问题。它不仅能快速生成答案，还能以形式化的方式输出完整的逻辑推导过程，确保每一步都经得起验证。

从 Prover 到 Prover-V2：持续进化

DeepSeek 上一次更新 Prover 是在去年 8 月，当时的版本被描述为一个“用于形式化定理证明和数学推理的定制开放 AI 模型”。此次发布的 V2 版本显然是对其前代的一次重大升级，不仅在参数规模上大幅提升，还在任务分解和逻辑推导能力上有了质的飞跃。

值得注意的是，DeepSeek 并未详细披露 Prover-V2 的训练数据和具体优化方法，但从其性能表现来看，这一模型无疑代表了当前数学 AI 领域的前沿水平。