LEGO-Prover: Neural Theorem Proving with Growing Libraries

📄 arXiv: 2310.00656v3 📥 PDF

作者: Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, Xiaodan Liang

分类: cs.AI

发布日期: 2023-10-01 (更新: 2023-10-27)

💡 一句话要点

提出LEGO-Prover以解决定理证明中的技能库限制问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 定理证明 动态技能库 大型语言模型 模块化推理 数学推理 自动定理证明 机器学习

📋 核心要点

  1. 现有的定理证明方法在处理中学水平定理时表现不佳，主要由于固定的定理库限制了其能力。
  2. LEGO-Prover通过构建一个动态扩展的技能库，允许在证明过程中生成和利用新的技能，从而增强了LLMs的推理能力。
  3. 实验结果显示，LEGO-Prover在miniF2F-valid和miniF2F-test上的通过率分别提高了9.0%和1.6%，并生成了超过20,000个新技能。

📝 摘要（中文）

尽管大型语言模型（LLMs）取得了成功，定理证明仍然是最具挑战性的推理任务之一。现有方法在证明中学水平定理时表现不佳，主要原因在于它们假设在整个证明过程中使用固定的定理库。为了解决这一问题，本文提出LEGO-Prover，通过构建一个不断扩展的技能库，利用经过验证的引理作为技能来增强LLMs的能力。LEGO-Prover支持模块化构建证明，使得LLMs能够在证明过程中检索现有技能并创造新技能。实验结果表明，LEGO-Prover在miniF2F-valid和miniF2F-test上的通过率显著提高，并生成了超过20,000个新技能，进一步丰富了技能库。

🔬 方法详解

问题定义：论文旨在解决定理证明中现有方法依赖固定定理库的局限性，这使得它们在处理复杂定理时能力不足。

核心思路：LEGO-Prover的核心思想是构建一个动态的技能库，允许在证明过程中不断添加和利用新技能，从而增强LLMs的推理能力。

技术框架：整体架构包括一个技能库模块、一个LLM模块和一个证明生成模块。技能库模块负责存储和管理引理，LLM模块用于推理和生成证明，而证明生成模块则负责将技能组合成完整的证明过程。

关键创新：LEGO-Prover的主要创新在于其动态技能库的构建与利用，允许模型在证明过程中不断学习和适应，这与传统方法的静态库形成鲜明对比。

关键设计：在设计上，LEGO-Prover采用了模块化的技能管理策略，设置了有效的提示机制以引导LLMs生成新技能，并通过不断的反馈循环来优化技能库的内容。具体的参数设置和损失函数设计在论文中详细描述。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

LEGO-Prover在miniF2F-valid和miniF2F-test上的通过率分别从48.0%提升至57.0%和从45.5%提升至47.1%。此外，模型在证明过程中生成了超过20,000个新技能，并通过新技能的引入将成功率从47.1%提升至50.4%。

🎯 应用场景

LEGO-Prover的研究成果在数学推理、自动定理证明和教育领域具有广泛的应用潜力。它可以帮助学生和研究人员更高效地解决复杂的数学问题，并促进数学理论的发展。未来，该方法还可能扩展到其他领域，如计算机科学和逻辑推理。

📄 摘要（原文）

Despite the success of large language models (LLMs), the task of theorem proving still remains one of the hardest reasoning tasks that is far from being fully solved. Prior methods using language models have demonstrated promising results, but they still struggle to prove even middle school level theorems. One common limitation of these methods is that they assume a fixed theorem library during the whole theorem proving process. However, as we all know, creating new useful theorems or even new theories is not only helpful but crucial and necessary for advancing mathematics and proving harder and deeper results. In this work, we present LEGO-Prover, which employs a growing skill library containing verified lemmas as skills to augment the capability of LLMs used in theorem proving. By constructing the proof modularly, LEGO-Prover enables LLMs to utilize existing skills retrieved from the library and to create new skills during the proving process. These skills are further evolved (by prompting an LLM) to enrich the library on another scale. Modular and reusable skills are constantly added to the library to enable tackling increasingly intricate mathematical problems. Moreover, the learned library further bridges the gap between human proofs and formal proofs by making it easier to impute missing steps. LEGO-Prover advances the state-of-the-art pass rate on miniF2F-valid (48.0% to 57.0%) and miniF2F-test (45.5% to 47.1%). During the proving process, LEGO-Prover also manages to generate over 20,000 skills (theorems/lemmas) and adds them to the growing library. Our ablation study indicates that these newly added skills are indeed helpful for proving theorems, resulting in an improvement from a success rate of 47.1% to 50.4%. We also release our code and all the generated skills.