让AI自己生成可复用的定理证明技巧库
DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent
- 采用唤醒-沉睡交替机制，自动发现并优化通用定理引理
- 在多个数学基准上提升证明成功率，且推理更简洁高效
- 适合研究形式化验证与自动化证明的学者和工程师
我们提出DreamProver，一种基于“唤醒-沉睡”程序归纳范式的智能体框架，用于发现可用于形式化定理证明的可复用引理。现有方法或依赖固定引理库（适应性差），或生成高度特定的中间引理（缺乏泛化性）。DreamProver通过迭代两阶段流程解决该问题：在唤醒阶段，利用当前引理库尝试证明训练集中的定理，并提出候选引理；在沉睡阶段，对这些候选引理进行抽象、精炼与整合，压缩并优化引理库。通过这一交替循环，DreamProver逐步演化出一组紧凑、高层、可迁移的引理，能有效用于相关领域未见过的定理证明。实验表明，DreamProver在多种数学基准上显著提升证明成功率，同时生成更短的证明路径并降低计算开销。
原文摘要 · Abstract (English)
We introduce DreamProver, an agentic framework that leverages a "wake-sleep" program induction paradigm to discover reusable lemmas for formal theorem proving. Existing approaches either rely on fixed lemma libraries, which limit adaptability, or synthesize highly specific intermediate lemmas tailored to individual theorems, thereby lacking generality. DreamProver addresses this gap through an iterative two-stage process. In the wake stage, DreamProver attempts to prove theorems from a training set using the current lemma library while proposing new candidate lemmas. In the "sleep" stage, it abstracts, refines, and consolidates these candidates to compress and optimize the library. Through this alternating cycle, DreamProver progressively evolves a compact set of high-level, transferable lemmas that can be effectively used to prove unseen theorems in related domains. Experimental results demonstrate that DreamProver substantially improves proof success rates across a diverse set of mathematical benchmarks, while also producing more concise proofs and reducing computational cost.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。