DeepSeek-Prover-V2：弥合非正式和正式数学推理之间的差距

虽然 DeepSeek-R1 已经在非正式推理方面显著提高了 AI 的能力，但正式的数学推理仍然是 AI 面临的挑战。这主要是因为生成可验证的数学证明需要深入的概念理解和构造精确的、步骤式的逻辑论证。然而，最近，DeepSeek-AI 的研究人员已经在这方面取得了重大进展，推出了 DeepSeek-Prover-V2，这是一种开源的 AI 模型，能够将数学直觉转化为严格的、可验证的证明。本文将深入探讨 DeepSeek-Prover-V2 的细节，并探讨其对未来科学发现的潜在影响。

正式数学推理的挑战

数学家们通常使用直觉、启发式和高层次的推理来解决问题。这种方法使他们能够跳过看似明显的步骤或依赖于足以满足他们需求的近似值。然而，正式的定理证明需要一种不同的方法。它需要完全的精确性，每一步都明确地说明并且在逻辑上得到证明，没有任何模糊性。

最近在大型语言模型（LLM）方面的进展表明，它们可以使用自然语言推理来解决复杂的、竞争级别的数学问题。尽管取得了这些进展，LLM 仍然难以将直觉推理转化为正式的证明，这些证明可以被机器验证。这主要是因为非正式推理通常包括捷径和省略的步骤，这些步骤是正式系统无法验证的。

DeepSeek-Prover-V2 通过结合非正式和正式推理的优势来解决这个问题。它将复杂的问题分解为较小的、可管理的部分，同时仍然保持正式验证所需的精确性。这种方法使得弥合人类直觉和机器验证证明之间的差距变得更加容易。

定理证明的新方法

从本质上讲，DeepSeek-Prover-V2 采用了一种独特的数据处理流水线，它同时涉及非正式和正式推理。流水线从 DeepSeek-V3 开始，DeepSeek-V3 是一个通用的大型语言模型，它分析数学问题的自然语言，分解它们为较小的步骤，并将这些步骤翻译为机器可以理解的正式语言。

与其尝试一次解决整个问题，不如将其分解为一系列“子目标”——中间引理，它们作为达到最终证明的垫脚石。这种方法模仿了人类数学家解决困难问题的方式，即通过处理可管理的块，而不是尝试一次解决所有问题。

使这种方法特别创新的是它合成训练数据的方式。当一个复杂问题的所有子目标都成功解决后，系统将这些解决方案合并为一个完整的正式证明。然后，这个证明与 DeepSeek-V3 的原始推理链合并，创建高质量的“冷启动”训练数据用于模型训练。

数学推理的强化学习

在对合成数据进行初步训练后，DeepSeek-Prover-V2 采用 强化学习 来进一步增强其能力。模型获得关于其解决方案是否正确或不正确的反馈，并利用这些反馈来学习哪些方法最有效。

这里面存在的一个挑战是，生成的证明的结构并不总是与 推理链 所建议的引理分解相一致。为了解决这个问题，研究人员在训练阶段包含了一致性奖励，以减少结构上的不一致性，并强制在最终证明中包含所有分解的引理。这种一致性方法被证明对于需要多步骤推理的复杂定理尤其有效。

性能和实际能力

DeepSeek-Prover-V2 在已建立的基准测试上的性能表明了其出色的能力。该模型在 MiniF2F-test 基准测试上取得了令人印象深刻的结果，并成功解决了 PutnamBench 中的 49 个问题——威廉·洛厄尔·普特南数学竞赛中的问题集。

也许更令人印象深刻的是，当评估最近 美国邀请数学考试（AIME） 竞赛中的 15 个选定问题时，该模型成功解决了 6 个问题。值得注意的是，相比 DeepSeek-Prover-V2，DeepSeek-V3 使用多数投票解决了这 8 个问题。这表明正式和非正式数学推理之间的差距在大型语言模型中正在迅速缩小。然而，该模型在组合数学问题上的性能仍需要改进，这突出了一个未来研究可以关注的领域。

ProverBench：AI 数学的新基准

DeepSeek 研究人员还推出了一个新的基准数据集，用于评估大型语言模型的数学问题解决能力。这个基准数据集被命名为 ProverBench，它由 325 个正式化的数学问题组成，包括 15 个来自最近 AIME 竞赛的问题，以及来自教科书和教育教程的问题。这些问题涵盖了数论、代数、微积分、实分析等领域。引入 AIME 问题尤为重要，因为它评估了模型在需要不仅仅是知识回忆，还需要创造性问题解决的能力。

开源访问和未来影响

DeepSeek-Prover-V2 提供了一个令人兴奋的机会，其开源可用性使其成为一个广泛可用的工具。托管在 平台 上，如 Hugging Face，该模型对包括研究人员、教育工作者和开发人员在内的广泛用户开放。通过提供一个更轻量级的 7 亿参数版本和一个强大的 671 亿参数版本，DeepSeek 研究人员确保具有不同计算资源的用户仍然可以从中受益。这种开源访问鼓励实验，并使开发人员能够创建高级的 AI 工具用于数学问题解决。因此，该模型有潜力推动数学研究的创新，赋予研究人员解决复杂问题和在该领域发现新见解的能力。

对 AI 和数学研究的影响

DeepSeek-Prover-V2 的开发对数学研究和 AI 都有着重要的影响。该模型生成正式证明的能力可以帮助数学家解决困难的定理，自动化验证过程，甚至提出新的猜想。此外，用于创建 DeepSeek-Prover-V2 的技术可能会影响未来 AI 模型在其他依赖严格逻辑推理的领域（如软件和硬件工程）的开发。

研究人员旨在将该模型扩展到解决甚至更具挑战性的问题，例如国际数学奥林匹克（IMO）级别的问题。这可能会进一步提高 AI 在证明数学定理方面的能力。随着像 DeepSeek-Prover-V2 这样的模型继续演进，它们可能会重新定义数学和 AI 的未来，推动从理论研究到技术应用等领域的进步。

结论

DeepSeek-Prover-V2 是 AI 驱动的数学推理的一个重要发展。它结合非正式直觉和正式逻辑来分解复杂的问题并生成可验证的证明。其在基准测试上的令人印象深刻的性能表明了其支持数学家、自动化证明验证，甚至在该领域推动新发现的潜力。作为一个开源模型，它广泛可用，提供了在 AI 和数学领域创新和新应用的令人兴奋的可能性。其令人印象深刻的性能和开源可用性使其成为数学研究和 AI 领域的一个重要工具。