突破形式化数学证明的边界：字节跳动Delta Prover如何让通用大模型具备顶尖定理证明能力

论文名称：Solving Formal Math Problems by Decomposition and Iterative Reflection
论文地址：https://arxiv.org/pdf/2507.15225v1

在人工智能领域，形式化数学证明长期以来被视为衡量机器推理能力的"珠穆朗玛峰"。从古希腊几何公理到现代数学的复杂定理，人类依靠逻辑演绎构建了宏伟的知识大厦，而让机器掌握这种精密推理能力一直是AI研究的核心目标。近期，字节跳动Seed团队发布的Delta Prover框架在这一领域取得了突破性进展——无需专门训练，仅通过通用大模型与Lean 4证明环境的智能协作，就在miniF2F-test基准测试中实现了95.9%的成功率，超越了所有需要模型专门化的现有方法。这一成果不仅刷新了自动定理证明的性能纪录，更揭示了通用大模型在有效引导下蕴藏的巨大潜能。本文将深入解析Delta Prover的创新架构、技术细节与实验成果，探讨这一突破对AI推理和数学研究的深远影响。

形式化数学证明：AI推理的终极挑战

数学证明的形式化表达与验证是人工智能领域的重要前沿。与自然语言数学推理不同，形式化证明要求每一步逻辑演绎都必须严格遵循形式语言的语法规则和公理系统，确保绝对正确性。这种严格性使得形式化证明成为验证复杂系统（从软件算法到硬件设计）的理想工具，但同时也为AI系统带来了独特挑战。

当代形式化证明系统如Lean、Isabelle和Coq已经成为数学家和计算机科学家的重要工具。以Lean 4为例，它不仅是一个定理证明器，还是一种函数式编程语言，允许用户以精确的形式化语言定义数学概念并构建证明。这些系统的核心优势在于其自动验证能力——通过内置的"内核"（kernel）可以机械地检查每一步推理是否符合逻辑规则，从根本上消除了自然语言证明中常见的模糊性和错误隐患。

然而，让AI系统掌握形式化证明技术面临双重困境。首先，形式化语言与通用编程语言存在显著差异，其独特的语法结构和逻辑范式使得主要训练于通用代码的大模型难以直接生成正确的形式化证明代码。数据稀缺性加剧了这一问题：目前最大的Lean 4代码库LEAN-GitHub仅包含0.13B tokens，仅占典型代码语料库的0.1%，导致通用大模型在形式化语言上的熟练度严重不足。

其次，现有方法通常依赖于专门训练的模型，这需要大量高质量的标注数据和巨额计算资源。获取形式化证明数据尤其困难，因为它要求标注者同时具备高级数学知识和特定形式化语言的专业技能。这种数据瓶颈使得专用模型的开发成本高昂，且难以推广到更广泛的数学领域。

传统的形式化定理证明方法存在明显局限性。早期工作如GPT-f展示了生成式预训练在定理证明中的潜力，但性能受限；后续方法如DeepSeek Prover和Kimina Prover通过大规模微调实现了性能提升，但需要持续的专业数据标注和计算投入。更重要的是，这些方法大多采用并行采样策略（Best-of-N），通过生成多个独立的证明尝试并选择有效的结果，但这种方式无法充分利用大模型的推理和反思能力，导致测试时的效率和扩展性不佳。

正是在这一背景下，字节跳动Seed团队提出了Delta Prover框架，开辟了一条基于通用大模型构建高效形式化证明系统的新路径。他们的核心 insight 是：通用大模型已经具备强大的推理和反思能力，关键在于设计有效的框架来引导这些能力在形式化证明环境中发挥作用，而非通过昂贵的专门训练来"硬编码"形式化推理能力。

Delta Prover架构：通用大模型的形式化推理赋能框架

Delta Prover的革命性突破源于其创新的代理式架构（agent-based framework），该架构巧妙地协调通用大模型与Lean 4证明环境的交互，无需任何模型微调即可实现顶尖的形式化证明能力。这一架构的核心是将大模型从被动的证明生成器转变为主动的推理代理，通过反思和迭代优化过程构建正确的形式化证明。

整体框架设计

Delta Prover的架构围绕两个相互依存的核心组件构建：反射式分解（reflective decomposition）与迭代式证明修复（iterative proof repair）的算法框架，以及基于Lean 4构建的专用领域特定语言（DSL）。这种设计使系统能够将复杂定理分解为可管理的子问题，并通过持续反馈逐步修正证明错误，最终整合为完整的形式化证明。

图1：Delta Prover的核心组件包括反射式分解与迭代式证明修复过程，二者通过专用DSL协同工作

系统的工作流程体现了明显的"代理"特性：面对一个形式化定理，Delta Prover首先尝试直接证明；若直接证明失败，则启动反射式分解过程，将原问题拆解为一系列子问题；每个子问题通过迭代式证明修复机制独立解决；最后，系统将所有子问题的证明自动整合为原定理的完整证明。这种分而治之的策略大幅降低了复杂定理的证明难度，同时充分利用了大模型的问题分解能力。

迭代式证明修复：错误驱动的精细化优化

迭代式证明修复是Delta Prover的基础机制，旨在通过持续反馈和修正来完善证明尝试。与传统的一次性生成策略不同，这一机制建立了大模型与Lean 4环境之间的紧密反馈循环，使系统能够从错误中学习并逐步改进证明。

该过程的工作原理可概括为以下步骤：

算法1展示了迭代式证明修复的伪代码实现。该机制的核心优势在于其利用大模型反思能力进行错误修正的能力，通过聚焦于错误点而非重新生成整个证明，显著提高了证明效率。实验数据表明，在固定预算下，增加修复次数（n）比增加独立尝试次数（m）能带来更高的成功率，这验证了反思能力在形式化证明中的关键价值。

反射式分解：复杂问题的结构化拆解

对于直接证明难以解决的复杂定理，Delta Prover引入了反射式分解机制，将原问题系统地分解为更简单的子问题，通过解决子问题来间接构建原定理的证明。这一过程受到人类数学家证明复杂定理时常用策略的启发：将大问题分解为引理，逐一证明后再整合。

反射式分解的实现包含三个关键步骤：

算法2详细描述了这一过程。反射式分解的核心创新在于其"反射"特性——系统不仅分解问题，还能根据子问题的求解情况反思分解策略的有效性并进行动态调整。这种自适应能力使系统能够处理传统分解方法难以应对的复杂问题。

领域特定语言（DSL）：子问题管理的技术支柱

为支持反射式分解和证明整合，Delta Prover构建了基于Lean 4元编程能力的专用DSL。该DSL在Lean 4的TacticM基础上引入了PlayM monad层，用于记录和管理中间证明状态，最终通过Lean 4的delaborator转换为有效的Lean 4证明脚本。

DSL提供了四个关键战术，支撑起完整的子问题管理生命周期：

• Suppose战术：用于引入新的假设到证明环境中，允许假设任意Lean 4类型作为前提而无需指定具体值。
• Define战术：支持引入任意Lean 4表达式并自动推断其类型，例如定义从整数到整数的函数或自然数上的有限集。
• ShowBy战术：在PlayM和TacticM之间建立接口，允许明确提出子目标并记录其证明过程，为后续整合做准备。
• Conclude战术：负责证明整合，利用记录的所有子问题证明和依赖关系图，生成原定理的完整证明。

图3展示了DSL如何支持从问题分解到证明整合的全过程。通过这些专用战术，DSL有效解决了Lean 4原生语法在高级证明草图设计、子问题上下文隔离和证明自动整合方面的不足，为反射式分解提供了坚实的技术基础。

整体工作流程

算法3描述了Delta Prover的完整工作流程，整合了上述所有组件：

这种分层策略确保了系统的效率和鲁棒性：简单问题可以通过直接证明快速解决，而复杂问题则通过分解降低难度。整个过程无需任何模型微调，完全依赖通用大模型在框架引导下的推理能力，显著降低了系统构建和维护的成本。

实验验证：刷新形式化证明性能纪录

为验证Delta Prover的有效性，字节跳动团队进行了全面的实验评估，在标准基准测试上与现有最先进方法进行了系统比较，并通过消融实验量化了各核心组件的贡献。实验结果不仅展示了Delta Prover的卓越性能，更揭示了通用大模型在形式化推理中的巨大潜力。

实验设置

实验采用Gemini 2.5 Pro 05-06作为基础大模型，这是一种未经过形式化证明专门训练的通用大模型。选择该模型旨在验证通用大模型在有效框架引导下的形式化证明能力，而非依赖模型的专门化训练。采样参数设置为temperature=1，符合通用大模型的典型使用场景。

评估主要基于两个标准基准：

• miniF2F-test：这是miniF2F基准的测试集，包含244个来自数学竞赛和MATH数据集的问题，涵盖不同难度级别。实验使用其Lean 4版本，并修正了陈述中的错误以确保公平比较。
• miniF2F-test-IMO：从miniF2F-test中提取的国际数学奥林匹克（IMO）问题子集，代表更具挑战性的形式化证明任务。

这些基准被广泛用于评估自动定理证明系统的性能，提供了与现有方法的直接比较基础。

基准性能比较

表1展示了Delta Prover与现有最先进方法在miniF2F-test上的性能比较。结果显示，Delta Prover以95.9%的成功率创下新的性能纪录，显著超越了所有现有方法，包括需要大量专门训练的模型。

值得注意的是，Delta Prover是唯一无需额外训练的方法。相比之下，此前的最佳方法Kimina Prover 72B虽然达到92.2%的成功率，但需要专门的微调训练和高达42000的样本预算；DeepSeek-Prover-V2 671B的成功率为88.9%，同样依赖于专门训练。更令人印象深刻的是，当使用相同的Gemini 2.5 Pro模型但采用标准的Best-of-N策略时，成功率仅为49.1%，这充分证明了Delta Prover框架对释放大模型能力的关键作用。

在更具挑战性的miniF2F-test-IMO基准上，Delta Prover同样表现出色，达到85%的成功率，超过了此前DeepSeek-Prover-V2等方法的性能，展示了其处理高难度数学问题的能力。这一结果尤为重要，因为IMO问题历来被视为自动定理证明的重大挑战，需要深刻的数学洞察力和复杂的推理链。

测试时缩放特性

除了绝对性能外，测试时的缩放特性（scaling law）是评估证明系统实用性的另一关键指标，它反映了系统随计算资源增加而提升性能的能力。图4展示了Delta Prover在两个基准上的测试时缩放曲线，结果表明其缩放特性显著优于传统的Best-of-N策略。

这种优势源于Delta Prover的迭代优化机制：系统能够基于先前尝试的反馈不断改进证明，而不是生成独立的证明尝试。随着计算预算的增加，这种累积改进效应使得性能提升更加显著。相比之下，Best-of-N策略的性能很快趋于饱和，因为独立样本之间无法共享信息或相互学习。

Delta Prover的样本预算计算方式也值得注意：系统记录每个问题成功解决所需的API调用次数，最终预算取所有已解决问题中的最大值。这种方式确保了预算估计的保守性，更真实地反映了实际使用场景中的资源需求。

消融实验：核心组件的贡献分析

为量化各核心组件的贡献，研究团队进行了系统的消融实验，分别评估了迭代式证明修复和反射式分解的单独影响。

迭代式证明修复的影响实验通过两种设置比较：固定总预算为1024，改变每轮修复次数（n）和轮数（m）；以及比较纯修复策略（m=1）与纯采样策略（n=1）的性能差异。

左图结果显示，在固定总预算下，增加修复次数（n）比增加独立轮数（m）能带来更高的成功率。这一发现与传统的探索-利用权衡直觉相反，表明当代大模型具有强大的自我修正能力，通过深入优化单个证明轨迹比探索多个独立轨迹更有效。

右图比较了迭代修复（m=1）与Best-of-N采样（n=1）的性能，结果清晰地表明迭代修复策略在所有预算水平上都优于采样策略，且优势随预算增加而扩大。这验证了迭代反馈循环在释放大模型推理能力中的关键作用。

反射式分解的影响实验选取了IMO 2019 Problem 1作为测试案例，这一问题对现有自动证明器极具挑战性，包括DeepSeek-Prover-V2在内的方法均未能解决。

实验对比了两种策略：仅使用迭代式证明修复的基线方法，以及完整的Delta Prover（包含反射式分解）。结果显示，基线方法在1024次API调用后仍未能找到解决方案；而Delta Prover通过将问题分解为83个子问题，平均每个子问题仅需4次API调用，总共约332次调用即成功解决了问题。这一结果不仅证明了反射式分解对处理复杂问题的有效性，也展示了其显著的效率优势。

分解后的子问题覆盖了从基础引理到关键步骤的各个方面，形成了层次化的证明结构。例如，系统首先建立了函数的基本性质（如f(2a)的表达式），然后推导出递归关系，最终通过分类讨论确定函数形式。这种结构化分解完美体现了人类数学家解决复杂问题的策略，展示了大模型在框架引导下模拟高级数学推理的能力。

典型案例分析

为进一步理解Delta Prover的工作机制，研究团队分析了多个典型案例，揭示了系统在面对不同类型挑战时的应对策略。

检索增强修复案例展示了系统如何处理定理名称错误。在一个求和问题中，大模型最初使用了错误的定理名称AntitoneOn.sum_le_integral_Icc，系统的检索机制基于这一错误名称找到了正确的定理AntitoneOn.sum_le_integral_Ico及其签名，并将其作为提示提供给大模型，最终成功完成证明。这一过程展示了检索增强在弥补大模型知识缺口方面的关键作用。

多步迭代修复案例展示了系统的复杂错误修正能力。在一个代数问题中，大模型首先尝试使用mul_div_cancel_left定理失败；反思后转而使用simp战术，但Lean反馈simp无法完成数值简化；大模型再次调整策略，明确调用norm_num完成数值简化，最终成功。这一过程展示了系统通过多轮反思逐步逼近正确解的能力。

复杂问题分解案例详细分析了IMO 2019 P1的分解过程。系统将这一挑战性问题分解为83个子问题，涵盖从基本替换到最终结论的各个步骤。例如，通过设置特定变量值（a=0或b=0）推导关键方程，建立递归关系，求解递归得到函数形式，最后通过分类讨论完成证明。这种精细分解使原本难以直接证明的复杂问题变得可解，充分展示了反射式分解的威力。

这些案例共同证明了Delta Prover框架的鲁棒性和适应性，能够处理形式化证明中常见的各种挑战，从简单的语法错误到复杂的策略调整。

意义与展望：重新定义 AI 形式化推理的未来

Delta Prover 的突破性成果不仅刷新了自动定理证明的性能纪录，更在方法论上为 AI 形式化推理开辟了新路径，其意义与影响值得深入探讨。
对 AI 推理研究的启示

Delta Prover 最深远的贡献在于证明了通用大模型在适当框架引导下，无需专门训练即可在高度专业化的形式化证明任务中达到甚至超越专门模型的水平。这一发现挑战了 “领域专精必须依赖领域微调” 的传统认知，表明通用大模型的推理和反思能力已经发展到可以通过有效引导来掌握高度专业化技能的阶段。

研究结果凸显了 “框架设计” 而非 “模型训练” 在释放 AI 能力中的关键作用。Delta Prover 通过构建反射式分解与迭代修复的协同机制，创造了一种 “思考 – 尝试 – 修正 – 再思考” 的闭环推理过程，这与人脑解决复杂问题的认知模式高度相似。这种 agentic 架构为设计下一代 AI 推理系统提供了重要参考：未来的重点可能不在于训练更专业的模型，而在于构建更智能的推理框架。

此外，Delta Prover 展示了通用大模型强大的子问题分解能力。在 IMO 2019 Problem 1 的案例中，系统能够自主将复杂定理分解为 83 个有序依赖的子问题，形成层次化的证明结构。这种能力表明大模型不仅能进行步骤推理，还具备全局规划能力，为解决更广泛的复杂问题提供了可能。
对数学研究与教育的潜在影响

形式化数学证明技术的进步对数学研究和教育具有深远意义。对于研究而言，Delta Prover 等先进证明系统有望成为数学家的得力助手，承担繁琐的细节验证工作，让研究者能够专注于核心创意和战略规划。特别是在复杂定理的证明中，系统可以自动检查引理的正确性并探索可能的证明路径，加速数学发现过程。

在教育领域，高性能形式化证明系统可以作为个性化学习工具，为学生提供即时反馈和证明指导。通过分析学生的形式化证明尝试，系统可以准确识别理解误区并提供针对性建议，这比传统教学方式更高效、更个性化。此外，系统生成的详细证明步骤也可作为学习资源，帮助学生理解复杂数学概念的推理过程。

值得注意的是，Delta Prover 在处理 IMO 级别的问题上取得的突破（85% 成功率），表明 AI 系统已经开始接近人类数学竞赛选手的水平。这不仅为数学教育提供了新工具，也可能重新定义人类与机器在数学创造力方面的协作模式。
技术局限性与未来方向

尽管取得了显著成功，Delta Prover 仍存在技术局限性，这些挑战也指明了未来的研究方向。

当前系统在处理需要高度创造性的数学洞察方面仍有不足。虽然反射式分解能够处理已知策略范围内的问题，但面对需要全新证明思路的问题时，性能可能大幅下降。此外，系统对形式化语言的理解仍依赖于提示工程而非真正的语义理解，这可能导致在复杂场景下的误解和错误。

针对这些局限性，研究团队提出了未来工作的几个重要方向：

探索更精细的测试时技术：如引入进化算法（FunSearch、AlphaEvolve 等）实现动态证明搜索优化，超越当前预定义的工作流程。这种方法可以让系统在证明过程中自主发现新的策略和技巧，提高创造性问题解决能力。
基于代理工作流的强化学习：通过强化学习让代理不断优化证明策略，使其能够从大量证明经验中学习有效的问题分解和修复模式。这种方法可以进一步提升系统的自适应能力和长期性能。
扩展 DSL 能力：增强领域特定语言对更复杂数学结构的支持，如高阶逻辑、范畴论等，扩大系统的应用范围。同时优化子问题管理机制，提高分解效率和整合能力。
多模态证明辅助：结合自然语言理解、图表识别和形式化推理，构建更全面的数学问题解决系统。这将使系统能够处理更广泛的输入形式，包括教科书问题、研究论文中的猜想等。
更广泛的 AI 代理研究启示

Delta Prover 的成功不仅限于数学证明领域，更为通用 AI 代理研究提供了重要启示。其核心经验 —— 通过有效的框架设计释放通用大模型的能力 —— 可以推广到其他复杂任务中。

系统展示的反射式分解和迭代修复机制代表了一种通用的问题解决范式：将复杂任务分解为子任务，通过持续反馈优化子任务解决方案，最终整合为整体结果。这种范式可应用于代码生成、科学发现、复杂决策等多个领域，推动 AI 系统从单一任务执行者向多功能问题解决者转变。

此外，Delta Prover 无需专门训练的特性大幅降低了技术应用的门槛。企业和研究机构无需投入巨额资源进行模型微调，只需构建适当的代理框架即可将通用大模型应用于特定领域，这将加速 AI 技术的普及和创新。

在 AI 伦理和可解释性方面，Delta Prover 的透明工作流程也具有优势。系统的每个分解步骤和修复决策都可以被追踪和解释，这比黑箱式的大型模型更易于理解和审计。这种可解释性对于高风险领域的 AI 应用至关重要。
结论：形式化推理的新时代

Delta Prover 的问世标志着形式化数学推理进入了一个新的时代。通过创新性地将通用大模型与形式化证明环境相结合，字节跳动 Seed 团队不仅实现了性能突破，更开辟了一条资源高效的技术路径。系统在 miniF2F-test 上 95.9% 的成功率和在 IMO 问题上 85% 的成功率，不仅刷新了纪录，更证明了通用智能与形式化推理结合的巨大潜力。

这一成果的核心意义在于：它展示了通用大模型在有效引导下能够掌握高度专业化的技能，挑战了 “领域专精必须依赖领域数据” 的传统观念。通过反射式分解与迭代修复的协同工作，以及专用 DSL 的技术支撑，Delta Prover 构建了一个模拟人类问题解决过程的 AI 代理，为复杂推理任务提供了新的解决方案。

展望未来，Delta Prover 及其背后的设计理念将推动 AI 形式化推理技术向更广泛的数学领域扩展，为数学研究和教育提供强大工具。同时，其代理架构思想将启发更通用的 AI 问题解决系统开发，推动 AI 从专项能力向综合智能迈进。

在这个 AI 快速发展的时代，Delta Prover 提醒我们：技术突破不仅来自更大的模型和更多的数据，更来自巧妙的框架设计和对问题本质的深刻理解。通过构建能够充分发挥通用智能潜力的系统，我们正逐步接近实现真正的人工智能问题解决者的目标，这不仅将改变数学和计算机科学的研究方式，更将推动整个社会的技术进步和创新。