Solving Formal Math Problems by Decomposition and Iterative Reflection

📄 arXiv: 2507.15225v1 📥 PDF

作者: Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, Haocheng Wang, Luong Trung, Rong Ye, Phan Nhat Hoang, Huishuai Zhang, Peng Sun, Hang Li

分类: cs.AI, cs.LG, cs.LO

发布日期: 2025-07-21

💡 一句话要点

Delta Prover：利用通用LLM通过分解和迭代反思解决形式化数学问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化证明 大型语言模型 定理证明 Lean 4 代理框架

📋 核心要点

  1. 现有方法在Lean 4等形式化语言中生成证明面临挑战，需要大量数据和训练成本进行模型特化。
  2. Delta Prover框架利用通用LLM的反思和推理能力，通过分解和迭代修复在Lean 4中交互构建证明。
  3. Delta Prover在miniF2F-test上达到95.9%的SOTA成功率，超越现有方法，并展现更强的测试时缩放性。

📝 摘要（中文）

通用大型语言模型（LLM）在智能领域取得了显著成功，在诸如编码和数学推理等复杂推理任务上表现堪比人类专家。然而，在诸如Lean 4等专用语言中生成形式化证明仍然是这些模型面临的重大挑战，限制了它们在复杂定理证明和自动验证中的应用。目前的方法通常需要通过在专用形式化语料库上进行微调来专门化模型，从而导致高昂的数据收集和训练成本。本文介绍了一种基于代理的框架 extbf{Delta Prover}，它协调通用LLM和Lean 4证明环境之间的交互。Delta Prover利用通用LLM的反思和推理能力，以交互方式在Lean 4中构建形式化证明，从而避免了模型专门化的需要。该代理的核心集成了两个新颖的、相互依赖的组件：用于反思分解和迭代证明修复的算法框架，以及构建在Lean 4之上的自定义领域特定语言（DSL），用于简化子问题管理。 extbf{Delta Prover在miniF2F-test基准测试中实现了95.9%的最先进的成功率，超过了所有现有方法，包括那些需要模型专门化的方法。}此外，与标准的Best-of-N证明策略相比，Delta Prover表现出明显更强的测试时缩放规律。至关重要的是，我们的研究结果表明，通用LLM在有效的代理结构的指导下，具有巨大的未开发的定理证明能力。这为在形式化环境中进行鲁棒的自动推理提供了一种计算效率高的替代方案，而无需专门的模型。

🔬 方法详解

问题定义：论文旨在解决通用LLM在形式化数学证明方面的不足，特别是在Lean 4等专用语言中生成形式化证明的难题。现有方法通常依赖于在特定数据集上微调LLM，这需要大量的数据收集和训练，成本高昂，且泛化能力可能受限。

核心思路：Delta Prover的核心思路是利用通用LLM强大的推理和反思能力，通过一个精心设计的代理框架，使其能够与Lean 4证明环境进行交互，从而逐步构建形式化证明。这种方法避免了对LLM进行专门化的微调，降低了成本，并提高了模型的通用性。

技术框架：Delta Prover采用基于代理的框架，包含以下主要模块：1) 反射分解模块：将复杂的证明问题分解为更小的、易于管理的子问题。2) 迭代证明修复模块：根据Lean 4环境的反馈，迭代地修复和完善证明。3) 领域特定语言（DSL）：提供一套简化的指令，用于在Lean 4环境中管理子问题和执行证明步骤。LLM作为核心推理引擎，负责生成证明步骤和响应环境反馈。整个过程通过迭代循环进行，直到找到完整的证明或达到预设的迭代次数。

关键创新：Delta Prover的关键创新在于其代理框架的设计，它能够有效地引导通用LLM进行形式化证明。通过反射分解和迭代修复，Delta Prover将复杂的证明任务分解为一系列更简单的子任务，从而降低了LLM的推理难度。此外，自定义的DSL简化了LLM与Lean 4环境的交互，提高了证明效率。与现有方法相比，Delta Prover无需对LLM进行专门化的微调，降低了成本，并提高了模型的通用性。

关键设计：Delta Prover的关键设计包括：1) 反射分解策略：如何将原始问题分解为合适的子问题，需要平衡子问题的复杂度和数量。2) 迭代修复机制：如何根据Lean 4环境的反馈，有效地修复和完善证明。3) DSL的设计：DSL需要足够简洁，易于LLM理解和使用，同时也要能够表达Lean 4环境中的关键操作。论文中可能还涉及到一些超参数的设置，例如迭代次数、子问题数量等，这些参数会影响Delta Prover的性能。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

Delta Prover在miniF2F-test基准测试中取得了95.9%的成功率，显著超过了所有现有的方法，包括那些需要模型专门化的方法。此外，Delta Prover还表现出比标准Best-of-N证明策略更强的测试时缩放规律，表明其具有更好的泛化能力和鲁棒性。

🎯 应用场景

Delta Prover在自动定理证明、形式化验证、软件可靠性等领域具有广泛的应用前景。它可以帮助研究人员和工程师更高效地验证数学定理和软件代码的正确性，提高软件系统的可靠性和安全性。未来，Delta Prover可以扩展到其他形式化语言和领域，例如硬件验证、智能合约验证等。

📄 摘要（原文）

General-purpose Large Language Models (LLMs) have achieved remarkable success in intelligence, performing comparably to human experts on complex reasoning tasks such as coding and mathematical reasoning. However, generating formal proofs in specialized languages like Lean 4 remains a significant challenge for these models, limiting their application in complex theorem proving and automated verification. Current approaches typically require specializing models through fine-tuning on dedicated formal corpora, incurring high costs for data collection and training. In this work, we introduce \textbf{Delta Prover}, an agent-based framework that orchestrates the interaction between a general-purpose LLM and the Lean 4 proof environment. Delta Prover leverages the reflection and reasoning capabilities of general-purpose LLMs to interactively construct formal proofs in Lean 4, circumventing the need for model specialization. At its core, the agent integrates two novel, interdependent components: an algorithmic framework for reflective decomposition and iterative proof repair, and a custom Domain-Specific Language (DSL) built upon Lean 4 for streamlined subproblem management. \textbf{Delta Prover achieves a state-of-the-art 95.9\% success rate on the miniF2F-test benchmark, surpassing all existing approaches, including those requiring model specialization.} Furthermore, Delta Prover exhibits a significantly stronger test-time scaling law compared to standard Best-of-N proof strategies. Crucially, our findings demonstrate that general-purpose LLMs, when guided by an effective agentic structure, possess substantial untapped theorem-proving capabilities. This presents a computationally efficient alternative to specialized models for robust automated reasoning in formal environments.