DeepSeek推出了DeepSeek-Prover-V2，这是一个开创性的开源大型语言模型(LLM)，它经过精心设计，用于 Lean 4 框架内复杂的形式化定理证明领域。这个新模型利用递归定理证明流水线，充分利用了DeepSeek最先进的DeepSeek-V3基础模型。Lean 4是Lean定理证明器的最新版本，是由微软研究院开发的交互式证明助手。这种复杂的函数式编程语言和交互式定理证明系统使数学家和计算机科学家能够构建具有无与伦比的机器检查验证的形式化证明。
该项目标志着弥合形式和非形式数学推理之间差距的巨大进步。通过利用通用LLM的固有能力，它旨在有效地解决高度结构化的形式化定理证明领域。DeepSeek研究团队认为，他们创新的方法反映了人类数学家在构建证明时所采用的认知过程，即将复杂的定理分解为更易于管理和理解的组成部分。
扩展评估框架：介绍ProverBench
为了提高研究的严谨性，DeepSeek团队通过引入ProverBench，显著扩展了他们的评估框架。ProverBench是一个全新的基准集合，专为全面评估形式化定理证明能力而精心设计。这个全面的集合是评估LLM在形式数学背景下性能的宝贵资源。
"除了传统的基准之外，我们自豪地推出ProverBench，这是一个精心策划的包含325个形式化问题的集合，以丰富我们的评估过程。该集合包括15个精心挑选的问题，直接来自近期的美国数学邀请赛(AIME)竞赛，具体来说是24-25年的竞赛，"研究人员详细说明。
将AIME问题纳入ProverBench数据集尤其值得关注，因为它引入了一组具有挑战性和完善的数学问题，这些问题在数学界得到广泛认可。这为评估DeepSeek-Prover-V2的性能并将其与其他方法进行比较提供了标准化和严格的基础。
前景广阔的初步结果：解决AIME问题
对这些具有挑战性的AIME问题进行严格测试的初步结果显示，他们精心设计的专用定理证明模型表现出了卓越的性能。DeepSeek团队自豪地报告说，DeepSeek-Prover-V2展示了其强大的能力，成功解决了提交给它的15个AIME问题中的6个。相比之下，通用DeepSeek-V3模型在使用多数投票技术时，成功解决了8个问题。
这些发现突显了专用LLM和通用LLM在解决复杂数学问题方面的潜力。虽然通用模型在这个特定基准中表现出稍高的成功率，但专用定理证明模型展示了其在形式数学推理方面的熟练程度。
模仿人类证明构造：一种链式思考方法
"鉴于通用模型在尝试生成完整的Lean证明时经常遇到的众所周知的挑战，我们有策略地指示DeepSeek-V3仅生成一个高层次的证明草图，故意省略了复杂的细节。由此产生的链式思考最终形成了一个由一系列have语句组成的Lean定理，每个语句都通过sorry占位符精心结尾，有效地表明需要解决的子目标。这种创新的方法优雅地模仿了人类的证明构建风格，在这种风格中，复杂的定理被逐步简化为一系列更易于管理的引理，"DeepSeek团队详细阐述。
这种生成高层次证明草图的创新方法与数学家通常处理复杂证明的方式相一致。通过关注整体结构和关键步骤，该模型可以有效地指导后续的完善和完成证明。
一种有条不紊的策略：单独处理每个证明组件
然后，该系统有条不紊地采用一种有条理和结构化的策略来处理证明的每个单独组件。这种系统的方法确保了证明的每个方面都得到仔细考虑，并以逻辑一致的方式解决。该系统创建了一种高度结构化的定理证明方法，在先前建立的结果的基础上，为每个后续步骤奠定坚实的基础。
"利用DeepSeek-V3生成的子目标，我们采用递归求解策略来系统地解决每个中间证明步骤。我们从have语句中提取子目标表达式，用它们来代替给定问题中的原始目标，然后将前面的子目标作为前提纳入。这种构造使后续的子目标能够使用早期步骤的中间结果来解决，从而促进更局部的依赖结构并促进更简单的引理的开发，"研究人员详细说明。
递归求解策略是该系统处理复杂证明能力的关键方面。通过将问题分解为更小、更易于管理的子目标，该系统可以有效地将其推理能力应用于每个单独的组件。
优化计算资源：一种专门的7B参数模型
为了有效地优化计算资源并确保高效处理，该系统有策略地采用了一种更小、高度专门的7B参数模型来处理分解的引理。这种方法对于有效管理与广泛证明搜索相关的计算需求至关重要，确保系统可以高效运行，而不会被搜索空间的复杂性所淹没。当所有分解步骤都成功解决时，该方法最终会得到自动导出的完整证明。
"该算法框架在两个不同的阶段运行，利用两个互补的模型：DeepSeek-V3用于引理分解，一个7B证明器模型用于完成相应的形式证明细节，"研究人员描述道。
这种两阶段方法允许系统利用大型通用模型和较小型专用模型的优势。大型模型用于生成高层次证明草图，而较小型模型用于填充细节并完成形式证明。
合成形式推理数据：一条自然的途径
这种精心设计的架构有效地建立了一条自然而直观的途径，用于合成形式推理数据，将高层次数学推理与形式验证的严格要求无缝融合。这种集成对于确保系统结果的可靠性和可信度至关重要。
"我们策划了一个具有挑战性的问题子集，这些问题无法通过7B证明器模型以端到端的方式解决，但所有分解的子目标都已成功解决。通过组合所有子目标的证明，我们为原始问题构建了一个完整的形式证明，"研究人员解释道。
这种方法允许系统从错误中学习并提高解决复杂问题的能力。通过识别导致困难的特定子目标，系统可以将其工作重点放在提高其在这些领域的表现上。
关注和挑战：实施细节受到审查
尽管DeepSeek-Prover-V2展示了不可否认的技术成就，但该领域的一些专家已经对某些实施细节提出了相关问题。Epoch AI的首席数学家Elliot Glazer是一位备受尊敬的人物，他指出了值得进一步调查的潜在问题。
关于DeepSeek-Prover-V2论文的一些担忧。潜在的错误形式化示例，关于Lean zulip的讨论表明，PutnamBench证明是无意义的，并且使用了隐式的sorry（可能隐藏在apply?策略中），这未在他们的read-eval-print-loop中报告。
这些担忧生动地突出了形式验证领域固有的持续挑战，即使是最细微和看似无关紧要的实施细节也会对结果的整体有效性和可靠性产生不成比例的巨大影响。形式验证过程需要对细节的坚定关注和对已建立标准的严格遵守。
错误形式化示例的可能性以及PutnamBench证明中隐藏的“sorry”策略的可能性，提出了关于验证过程的严格性和完整性的重要问题。这些担忧突显了对结果进行持续审查和独立验证的必要性。
可用性和资源：普及形式化定理证明的访问
DeepSeek提供了两种不同模型尺寸的Prover-V2，以满足各种计算资源和研究目标。第一个版本是基于他们之前的Prover-V1.5-Base构建的7B参数模型，具有高达32K token的扩展上下文长度。第二个版本是在DeepSeek-V3-Base上训练的更大的671B参数模型。这两种模型现在都可以在HuggingFace上轻松访问，HuggingFace是一个用于共享和协作开发机器学习模型的领先平台。
除了模型本身之外，DeepSeek还在HuggingFace上提供了完整的ProverBench数据集，其中包含325个经过精心形式化的评估问题。这个全面的数据集为研究人员和开发人员提供了宝贵的资源，用于评估其模型的性能并将其与DeepSeek-Prover-V2进行比较。
通过免费提供这些资源，DeepSeek正在普及对形式化定理证明技术的访问，并促进研究社区内的协作。这种开源方法可能会加速该领域的进展，并导致在自动推理和验证方面取得新的突破。
这种发布为研究人员和开发人员提供了深入研究这项技术的功能和局限性所需的资源。通过开放对模型和ProverBench数据集的访问，DeepSeek鼓励进一步探索和协作努力，以解决该领域专家提出的担忧。这种协作方法是解开形式化定理证明的复杂性并巩固这些突破性进展的可靠性的关键。