ImProver: Agent-Based Automated Proof Optimization

📄 arXiv: 2410.04753v1 📥 PDF

作者: Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, Sean Welleck

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

发布日期: 2024-10-07

备注: 19 pages, 21 figures

💡 一句话要点

ImProver：基于Agent的自动化定理证明优化方法，提升证明质量。

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

关键词: 自动化定理证明 形式化验证 大型语言模型 Agent 证明优化

📋 核心要点

  1. 现有方法难以优化形式化证明，使其满足特定标准（如长度、可读性），人工编写的证明也可能不适合学习任务。
  2. ImProver利用大型语言模型作为Agent，通过重写证明来优化用户自定义的指标，解决自动化证明优化问题。
  3. 实验表明，ImProver能够显著缩短、模块化和提高真实数学定理证明的可读性，优于直接应用LLM的方法。

📝 摘要（中文）

大型语言模型（LLMs）已被用于在Lean等证明助手中生成数学定理的形式化证明。然而，我们常常需要根据各种标准优化形式化证明，这取决于其下游用途。例如，我们可能希望证明符合某种风格，或者具有可读性、简洁性或模块化结构。拥有经过适当优化的证明对于学习任务也很重要，特别是因为人工编写的证明可能并非为此目的而优化。为此，我们研究了一个新的自动化证明优化问题：重写证明，使其正确并针对任意标准（如长度或可读性）进行优化。作为自动化证明优化的第一种方法，我们提出了ImProver，这是一个大型语言模型Agent，它可以重写证明，以优化Lean中任意用户定义的指标。我们发现，简单地将LLM应用于证明优化效果不佳，因此我们将各种改进融入到ImProver中，例如在新颖的Chain-of-States技术中使用符号Lean上下文，以及错误纠正和检索。我们在重写真实的本科生、竞赛和研究级别的数学定理上测试了ImProver，发现ImProver能够重写证明，使其更短、更模块化和更具可读性。

🔬 方法详解

问题定义：论文旨在解决形式化证明的自动化优化问题。现有的形式化证明可能冗长、难以理解或不符合特定风格，人工编写的证明也未必是最优的。直接应用大型语言模型（LLM）进行证明优化效果不佳，无法有效提升证明的质量。

核心思路：论文的核心思路是将LLM作为一个Agent，通过迭代地重写证明来优化用户定义的指标。Agent通过与Lean证明助手交互，不断探索和改进证明，最终得到满足优化目标的证明。这种方法允许根据不同的标准（如长度、可读性、模块化）定制优化过程。

技术框架：ImProver的技术框架主要包含以下几个模块：1) LLM Agent：负责生成新的证明步骤和策略。2) Lean证明助手：用于验证证明的正确性，并提供环境信息。3) Chain-of-States：一种新颖的技术，利用符号Lean上下文来指导LLM Agent的证明过程。4) 错误纠正机制：用于修复LLM Agent生成的错误证明。5) 检索机制：用于从已有的证明中检索相关的策略和步骤。

关键创新：论文的关键创新在于：1) 提出了基于Agent的自动化证明优化框架。2) 引入了Chain-of-States技术，利用符号Lean上下文来提高LLM Agent的证明能力。3) 集成了错误纠正和检索机制，增强了ImProver的鲁棒性和效率。与现有方法相比，ImProver能够更有效地优化证明，并生成更短、更模块化和更具可读性的证明。

关键设计：Chain-of-States技术通过维护一个符号Lean上下文，记录了证明的状态和目标。LLM Agent可以根据这个上下文生成更准确和有效的证明步骤。错误纠正机制利用Lean证明助手的反馈信息，自动修复LLM Agent生成的错误证明。检索机制从已有的证明库中检索相关的策略和步骤，加速了证明过程。具体的参数设置和损失函数等技术细节在论文中没有详细描述，属于未知信息。

📊 实验亮点

ImProver在重写真实世界的本科生、竞赛和研究级别的数学定理时表现出色，能够显著缩短证明的长度，提高证明的模块化程度和可读性。具体性能数据和提升幅度在摘要中有所提及，但未给出具体数值，属于未知信息。

🎯 应用场景

该研究成果可应用于自动化定理证明、形式化验证、程序合成等领域。通过优化形式化证明，可以提高数学定理的可理解性和可验证性，促进数学知识的传播和应用。此外，该方法还可以用于教育领域，帮助学生学习和理解数学证明。

📄 摘要（原文）

Large language models (LLMs) have been used to generate formal proofs of mathematical theorems in proofs assistants such as Lean. However, we often want to optimize a formal proof with respect to various criteria, depending on its downstream use. For example, we may want a proof to adhere to a certain style, or to be readable, concise, or modularly structured. Having suitably optimized proofs is also important for learning tasks, especially since human-written proofs may not optimal for that purpose. To this end, we study a new problem of automated proof optimization: rewriting a proof so that it is correct and optimizes for an arbitrary criterion, such as length or readability. As a first method for automated proof optimization, we present ImProver, a large-language-model agent that rewrites proofs to optimize arbitrary user-defined metrics in Lean. We find that naively applying LLMs to proof optimization falls short, and we incorporate various improvements into ImProver, such as the use of symbolic Lean context in a novel Chain-of-States technique, as well as error-correction and retrieval. We test ImProver on rewriting real-world undergraduate, competition, and research-level mathematics theorems, finding that ImProver is capable of rewriting proofs so that they are substantially shorter, more modular, and more readable.