DeepSeek发布新开源模型：专注于形式化数学推理

近日，深度求索（DeepSeek）在 AI 开源社区 Hugging Face 上宣布推出其最新模型——DeepSeek-Prover-V2。这款模型特别聚焦于形式化数学推理，旨在解决复杂的数学定理问题，并为相关研究提供强大的工具支持。经过数月的研发，DeepSeek团队在4月30日正式发布了模型及其相关的研究论文，标志着在数学推理领域的重要进展。

DeepSeek-Prover-V2 基于早前的 DeepSeek-V3-0324 模型构建，使用了一种创新的方式来生成初始训练数据。具体该模型采用了递归定理证明管道，能够有效地将复杂的数学定理分解为一系列可管理的子目标（subgoals）。通过结合非形式化与形式化的数学推理，该模型具备了更强大的逻辑推理能力，能够在 Lean 4 上完成形式化证明的步骤。

值得一提的是，DeepSeek 团队还同时推出了两个模型，分别是结合 V3 基础模型的基本模型和经过增强的模型。这两个模型都采用了与 DeepSeek-V3-0324 相同的架构，但其应用领域并不涵盖常规对话或推理，主要针对形式化定理证明的需求进行优化。

在模型的训练过程中，DeepSeek 团队采取了一系列策略来提升其性能。通过将复杂的定理拆解为多个子目标，模型能够减少计算的复杂性，加速推理过程。团队使用一个较小的 7B 参数模型负责处理这些子目标的证明搜索，这样一来，可以显著降低计算负担，同时提高模型的响应速度。

通过整合这些子目标的证明，DeepSeek-Prover-V2 能够生成完整的形式化证明，从而与 DeepSeek-V3 的推理过程相结合。这一过程被称为“冷启动”数据的生成，这种数据增强了模型的能力，使得其在神经定理证明领域取得新的突破。在 PutnamBench 数据集中，DeepSeek-Prover-V2 成功解决了658个问题中的49个，创下了新的记录。

为了进一步评估和测试该模型的性能，DeepSeek团队还发布了 ProverBench 基准数据集，其中包含325个形式化数学问题。这些问题的难度水平覆盖了高中数学竞赛，涉及数论、代数、线性代数、微积分和概率等多个领域。特别地，该数据集中的15个问题来源于近期的 AIME 竞赛（AIME 24 和 25），代表了高校竞赛的挑战性，旨在为高中竞赛和本科数学提供更为全面的评估标准。

DeepSeek-Prover-V2 的推出，将对数学教育和研究领域产生深远影响。形式化数学推理模型的应用，将有助于提高学生对数学问题的理解深度和解决能力，进而促进数学教育的革新。借助这种强大的工具，研究者可以在形式化证明与算法设计方面展开更深入的探索，推动数学和计算机科学的交叉发展。

DeepSeek-Prover-V2 的发布不仅是深度求索团队的重大战略推广，也是形式化数学推理领域的一个标志性成果。该模型的成功，得益于团队扎实的研究基础和创造性的技术应用，为未来更多的研究与实践提供了广阔的前景和无限的可能。

随着AI技术的不断发展，数学推理模型所展现出的潜能将会激励更多的研究者参与到这一领域中来，在普及数学教育、提高学术水平、推动学术合作等方面发挥更加积极的作用。未来，我们期待借助 DeepSeek-Prover-V2 等工具，能够持续推动形式化数学推理技术的发展，为解决更多实际问题提供强有力的支持。