DeepSeek开源数学模型Prover-V2-671B，较上一代参数量进步近百倍

发布时间：2025-05-15　点此：576次

DeepSeek 又在假日到来的时分有新动作了。

生动的DeepSeek开源数学模型Prover-V2-671B，较上一代参数量提高近百倍的图像

刚刚，DeepSeek 在毫无预告的情况下，忽然在 Hugging Face 平台上开源了最新数学定理证明专用模型 DeepSeek-Prover-V2-671B。

（来历：Hugging Face）

这个新模型并非通用的谈天机器人，而是专心于数学定理的形式化证明这一高度专业的范畴。这类模型的方针是使用像 Lean 4 这样的证明帮手软件，来了解和生成严厉的数学证明过程。简略来说，它们是帮忙计算机验证数学定理正确性的 AI 东西，需求具有很强的逻辑推理才能。其主要使用场景包括：主动定理证明（从高中到大学水平的数学问题）、发现证明中的过错并供给修正主张、经过生成 Lean 4 代码和解说帮忙教育，以及帮忙数学家探究新定理等。

实践上，DeepSeek 此前就已久发布过同类模型，2024 年 8 月时，他们曾发布了DeepSeek-Prover-V1.5，一个大约 7B 参数的模型。依据 DeepSeek 其时发布的信息，V1.5 在结合强化学习和蒙特卡洛树查找等技术后，在一些规范的数学证明测验（如miniF2F 和 ProofNet）中获得了不错的效果，不能自制处理从高中到大学本科部分水平的数学问题。

图丨Prover-V1.5 的基准测验（来历：DeepSeek）

简洁的DeepSeek开源数学模型Prover-V2-671B，较上一代参数量提高近百倍的插图

这次发布的 DeepSeek-Prover-V2-671B，在模型规划上有了巨大的腾跃，参数量达到了 671B ，比 V1.5 大了近百倍，比其他同类产品如 Llemma-7B/34B、InternLM2-StepProver 等也要大得多。

依据其揭露的装备文件，不露锋芒不能自制了解到更多关于模型结构的信息。该模型建立在 DeepSeek-V3 架构之上，因而许多装备与通用的 DeepSeek-V3 模型类似。它采用了混合专家（MoE，Mixture-of-Experts）的规划，详细来说，每层包括 256 个路由专家（routed experts）和1个同享专家（shared expert），每个专家的中间层巨细（moe_intermediate_size）为 2048，在处理每个输入符号（token）时会激活其间的 8 个专家。此外，该模型支撑的最大上下文长度达到了 163,840 个 token。

图丨装备文件（来历：Hugging Face）

不过，到发稿时，DeepSeek 官方没有发布更多关于该模型的技术细节和功能数据。关于 DeepSeek-Prover-V2-671B 的训练方法、使用了哪些特定于数学证明的数据，以及它在基准测验上的实践体现如多么要害信息，现在仍一窍不通。

关于这个新模型的内部结构和详细才能，还有待官方供给更多信息。考虑到参数量的巨大提高，不露锋芒不能自制等待 Prover-V2 能在各项数学证明基准上获得更好的成果。