用AI自动生成数学定理证明，通过分解难题提升成功率。
Gödel's Poetry
- 用多智能体系统分解复杂定理为简单命题，逐层求证。
- 在miniF2F数据集上无分解时通过率达90.4%，分解后显著提升。
- 开源可扩展，适配不同语言模型，适合形式化验证研究者。
形式化自动定理证明长期被视为人工智能的挑战。本文提出一种新方法，利用针对Lean4的专用语言模型生成证明，并通过递归分解复杂定理为更简单的蕴含命题。系统采用多智能体架构，协调自动形式化（如需）、证明生成、定理分解及递归求证（或再分解）。无分解时，在miniF2F数据集上达到90.4%的通过率；引入分解后性能显著提升。关键技术贡献在于扩展Kimina Lean Server，增加抽象语法树（AST）解析能力，实现自动化递归证明分解。系统已在PyPI发布为goedels-poetry，开源实现见GitHub：KellyJDavis/goedels-poetry，支持替换语言模型与自定义功能扩展。
原文摘要 · Abstract (English)
Formal, automated theorem proving has long been viewed as a challenge to artificial intelligence. We introduce here a new approach to computer theorem proving, one that employs specialized language models for Lean4 proof generation combined with recursive decomposition of difficult theorems into simpler entailing propositions. These models are coordinated through a multi-agent architecture that orchestrates autoformalization (if required), proof generation, decomposition of difficult theorems into simpler entailing propositions, and recursive proof (and/or decomposition) of these propositions. Without decomposition, we achieve a 90.4% pass rate on miniF2F. With decomposition, this is significantly improved. A key technical contribution lies in our extension of the Kimina Lean Server with abstract syntax tree (AST) parsing capabilities to facilitate automated, recursive proof decomposition. The system is made available on PyPI as goedels-poetry (at https://pypi.org/project/goedels-poetry ), and the open-source implementation KellyJDavis/goedels-poetry (at https://github.com/KellyJDavis/goedels-poetry ) facilitates both adaptation to alternative language models and extension with custom functionality.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。