DeepSeek发布了全新开源大模型，实现了数学能力的重大提升！

前天晚上，DeepSeek发布了最新的数学专用大模型V2。 该模型有两个版本，分别是671亿参数和7亿参数。在极具挑战性的数学评测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（第24届和第25届）竞赛中的数论和代数题，体现了真实高中竞赛的难度水平。

图片

其余的310道题目来源于精心挑选的教科书案例和教学资料，内容涵盖高中至大学阶段的多个数学领域，如数论、基础代数、线性代数、抽象代数、微积分、实分析、复分析、泛函分析以及概率论等，为对模型能力的评估提供了广泛且多样化的测试内容。