昨晚，DeepSeek又“偷偷”开源了一款专门针对数学领域的大模型V2。
V2一共有671B和7B两种参数，在超难数学评估测试MiniF2F中，671B通过率达到了88.9%，并且在PutnamBench的658个问题中解决49个，数学能力非常强。
值得一提的是，DeepSeek还开源了一个高水准的数学评估集ProverBench。
开源地址：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
评估数据集：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench
架构方面，V2-671B 是在 DeepSeek-V3-Base 的基础上进一步训练而成，而 V2-7B 是在 DeepSeek-Prover-V1.5-Base 的基础上构建，并扩展了上下文长度，最大可达 32K 个标记。
V2 构建了一个统一的数学推理框架，融合了非形式化和形式化数学推理。通过将复杂的数学问题分解为一系列子目标，并利用V3 的逐步推理能力，将非形式化的推理过程与形式化的证明过程相结合，从而实现了从问题分解到证明生成的无缝衔接。
为了生成冷启动数据， V2采用了一种递归定理证明管道。V3被用于将定理分解为高级别的证明草图，并同时在Lean4中形式化这些证明步骤，生成一系列子目标。
随后，一个较小的7B模型被用于处理每个子目标的证明搜索，这种方式有效减轻了计算负担。当一个复杂问题的分解步骤被解决后，完整的逐步形式化证明与DeepSeek-V3的链式思考过程相结合，生成了冷启动推理数据。这些数据为模型的初始训练提供了重要的基础。
在冷启动数据的基础上， V2进行了强化学习阶段。筛选出那些7B证明模型无法端到端解决的难题，但这些难题的所有分解子目标都已成功解决。
通过组合所有子目标的证明，构建出原始问题的完整形式化证明，并将其附加到V3的链式思考中，从而产生了非形式化推理与形式化证明的连贯合成。
在强化学习阶段，模型使用二元正确或错误反馈作为主要的奖励监督形式，进一步增强了其将非形式化推理与形式化证明构建相结合的能力。
为了更全面地评估模型的性能，DeepSeek开发了ProverBench基准测试数据集。该数据集包含325个问题，其中15个问题是从最近的AIME竞赛（AIME24和25）中的数论和代数问题形式化而来，提供了真实的高中竞赛水平挑战。
其余的310个问题则来自精选的教科书示例和教育教程，涵盖了从高中到本科水平的多样化数学问题，包括数论、初等代数、线性代数、抽象代数、微积分、实分析、复分析、泛函分析、概率等多个领域，为模型的性能评估提供了丰富的测试场景。
（文：AIGC开放社区）