Solving Formal Math Problems by Decomposition and Iterative Reflection

通用大语言模型（LLMs）在智能方面取得了显著成功，在诸如编程和数学推理等复杂推理任务上的表现已能与人类专家相媲美。然而，使用这些模型在Lean 4等专业语言中生成形式化证明仍然是一个重大挑战，这限制了它们在复杂定理证明和自动化验证中的应用。目前的方法通常需要通过对专门的形式化语料库进行微调来定制模型，从而带来高昂的数据收集和训练成本。本文中，我们提出了**Delta Prover**，这是一种基于智能体的框架，用于协调通用大语言模型与Lean 4证明环境之间的交互。Delta Prover利用通用大语言模型的反思与推理能力，以交互方式构建Lean 4中的形式化证明，从而避免了对模型定制的需求。该智能体的核心集成了两个新颖且相互依赖的组件：一个用于反思性分解和迭代证明修复的算法框架，以及一个基于Lean 4构建的定制领域特定语言（DSL），用于简化子问题的管理。**Delta Prover在miniF2F-test基准测试中实现了95.9%的成功率，达到当前最先进的水平，超越了包括需要模型定制在内的所有现有方法。** 此外，与标准的Best-of-N证明策略相比，Delta Prover在测试时展现出显著更强的扩展规律。关键在于，我们的研究结果表明，当受到有效的智能体结构引导时，通用大语言模型具备尚未被充分开发的定理证明潜力。这为在形式化环境中实现强大而自动化的推理提供了一种计算效率更高的替代方案，相较于专门化的模型更具优势。

论文旨在解决通用大语言模型（LLMs）在专业形式化语言（如Lean 4）中生成形式化证明的挑战，这一问题在当前研究中仍然存在显著瓶颈，尤其是在复杂定理证明和自动化验证领域。

论文提出了一种基于智能体的框架 Delta Prover，通过将通用LLM与Lean 4证明环境进行交互式协同，利用LLM的反思与推理能力逐步构建形式化证明，无需对模型进行专门的微调或训练。

1. Delta Prover 在 miniF2F-test 基准上达到了 95.9% 的成功率，超越所有现有方法，包括需要模型专业化的方法。 2. 引入了反射式分解与迭代证明修复的算法框架，以及基于 Lean 4 的 DSL 来高效管理子问题。 3. 实验表明 Delta Prover 的测试时扩展规律显著优于标准的 Best-of-N 证明策略。 4. 展示了通用 LLM 在有效智能体结构引导下，具备强大的未被充分挖掘的定理证明能力。 5. 提供了一种计算效率更高的替代方案，避免了为特定领域训练专用模型的高昂成本。

1. Proof Generation with Large Language Models (2023) 2. Formal Mathematics Statement Curriculum Learning (2022) 3. Lean Chat: Interactive Theorem Proving with Large Language Models (2023) 4. Measuring Mathematical Problem Solving Ability of Language Models (2023) 5. Autoformalization with Large Language Models (2023)