用大模型自动生成定理并自我学习，提升数学定理发现效率。
Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
- 通过迭代生成猜想并用已证定理作上下文，实现无参数策略优化。
- 在硬核定理上发现率显著高于传统同步生成方法。
- 适合对自动化定理证明感兴趣的科研人员和形式化验证开发者。
大型语言模型在形式化定理证明中展现出巨大潜力。本文研究了大模型发现新定理并生成可验证证明的能力。提出名为猜想-证明循环（CPL）的流水线，通过迭代生成数学猜想并在 Lean 4 中尝试证明。其关键特征是每轮都利用之前生成的定理及其形式化证明作为上下文，实现无需参数更新的证明策略改进。理论与实验均表明，相较于同时生成命题与证明的框架，CPL 显著提升了难以证明定理的发现率。实验还显示，重复使用模型自身的形式化验证输出作为上下文，持续提升后续证明成功率，验证了自生成上下文学习在神经定理证明中的有效性。代码开源于 https://github.com/auto-res/ConjecturingProvingLoop。
原文摘要 · Abstract (English)
Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving. In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called Conjecturing-Proving Loop (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4. A key feature of CPL is that each iteration conditions the LLM on previously generated theorems and their formal proofs, enabling parameter-free improvement of proof strategies via in-context learning. We provide both theoretical and experimental evidence that CPL increases the discovery rate of hard-to-prove theorems compared to frameworks that generate statements and proofs simultaneously. Moreover, our experiments show that reusing the LLM's own formally verified outputs as context consistently improves subsequent proof success, demonstrating the effectiveness of self-generated in-context learning for neural theorem proving. The source code is available at https://github.com/auto-res/ConjecturingProvingLoop.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。