Gödel's Poetry

形式化、自动化的定理证明长期以来被视为对人工智能的一大挑战。本文提出了一种全新的计算机定理证明方法，该方法采用专为Lean4证明生成而设计的语言模型，并结合递归地将复杂定理分解为更简单的蕴含命题的方式。这些模型通过一个多智能体架构进行协调，该架构统筹管理自动形式化（如需要）、证明生成、将复杂定理递归分解为较简单命题，以及对这些命题进行递归证明（或进一步分解）的全过程。在不使用分解的情况下，我们的方法在miniF2F测试集上已达到90.4%的通过率；而引入分解机制后，性能得到显著提升。本研究的一项关键技术贡献在于，我们扩展了Kimina Lean服务器，为其增加了抽象语法树（AST）解析功能，从而支持自动化、递归式的证明分解。该系统已作为“goedels-poetry”发布至PyPI（https://pypi.org/project/goedels-poetry），其开源实现KellyJDavis/goedels-poetry（https://github.com/KellyJDavis/goedels-poetry）便于适配其他语言模型，并支持自定义功能的扩展。

论文试图解决形式化定理证明这一长期被视为人工智能挑战的问题，特别是如何提高自动化定理证明系统在复杂数学命题上的证明成功率。传统方法在处理高难度定理时往往受限于直接生成完整证明的能力，因此需要更智能的分解与协作机制。该问题虽非全新，但结合现代语言模型与多智能体协同进行递归分解的方法提出了新的解决路径。

提出一种新颖的多智能体架构，利用专用于Lean4的形式化语言模型，结合自动形式化、定理分解与递归证明机制。关键创新在于将复杂定理递归拆解为更简单的子命题，并通过扩展Kimina Lean Server支持AST解析以实现自动化分解。相比现有工作，该方法显著提升了miniF2F基准上的性能，尤其在引入分解策略后效果更为突出。

系统在miniF2F上实现了90.4%的通过率（无分解），并通过递归分解进一步大幅提升性能；设计了模块化的多智能体框架，支持灵活集成不同语言模型和功能扩展；开源代码发布于GitHub（KellyJDavis/goedels-poetry）并可通过PyPI安装（goedels-poetry），促进了可复现性与社区贡献；实验基于标准形式化数学基准miniF2F，具备可比性；未来可探索更高效的分解策略、更强的语言模型集成以及跨形式化系统的迁移能力。

1. LeanDojo: Decomposing Complex Theorems for Formal Reasoning (2023) 2. Proof Artifact Generation for Interactive Theorem Proving with Large Language Models (ICLR 2024) 3. NaturalProofs: Mathematical Theorem Proving in Natural Language (NeurIPS 2022) 4. Autoformalization with Large Language Models (arXiv:2210.12283, 2022) 5. Competitive Programming with Large Language Models and Program-Aided Prompting (PaLM, 2023)