用AI自动优化数学证明，让证明更短更清晰。
ImProver: Agent-Based Automated Proof Optimization
- 设计智能体通过链式状态分析重构证明
- 实测可使证明缩短、结构更模块化
- 适合数学教育与自动化推理研究者
大型语言模型（LLMs）已被用于在形式化证明助手（如Lean）中生成数学定理的正式证明。然而，根据下游用途，我们常需对证明进行优化，例如遵循特定风格、提升可读性、简洁性或模块化程度。合适的优化证明对学习任务尤为重要，因为人类编写的证明未必适用于训练需求。为此，我们提出自动化证明优化的新问题：在保证正确性的前提下，重写证明以满足任意用户定义的目标，如长度或可读性。作为首个解决方案，我们提出ImProver——一个基于大模型的智能体，在Lean中根据用户自定义指标重写证明。发现直接应用LLMs效果不佳，因此引入多项改进，包括创新的符号化上下文链式状态技术、错误修正与检索机制。我们在真实世界中的本科、竞赛及科研级数学定理上测试ImProver，结果表明其能显著生成更短、更模块化、更易读的证明。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。