Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation
作者: Shaonan Wu, Shuai Lu, Yeyun Gong, Nan Duan, Ping Wei
分类: cs.AI
发布日期: 2024-10-21 (更新: 2025-04-03)
💡 一句话要点
Alchemy：通过符号变异增强定理证明能力
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 神经定理证明 数据增强 符号变异 形式化验证 大型语言模型
📋 核心要点
- 神经定理证明面临数据稀缺的挑战，现有形式化语料库规模有限，阻碍了模型性能的提升。
- 提出Alchemy框架，通过符号变异合成新的形式化定理，有效扩充训练数据，提升模型泛化能力。
- 实验表明，Alchemy在Leandojo和miniF2F基准测试中均取得了显著的性能提升，验证了其有效性。
📝 摘要（中文）
形式化证明的编写对经验丰富的专家来说也极具挑战性。神经定理证明（NTP）的最新进展显示了加速这一过程的希望。然而，与通用文本相比，互联网上可用的形式化语料库有限，这对NTP提出了严重的数据稀缺挑战。为了解决这个问题，本文提出了一种通用的数据合成框架Alchemy，该框架通过符号变异来构造形式化定理。具体来说，对于Mathlib中的每个候选定理，我们识别所有可调用的定理，这些定理可以用来重写或应用于它。随后，我们通过用其等价形式或前件替换语句中的相应项来变异候选定理。因此，我们的方法将Mathlib中的定理数量增加了一个数量级，从11万个增加到600万个。此外，我们对这个扩充的语料库进行持续的预训练和监督微调，用于大型语言模型。实验结果表明了我们方法的有效性，在Leandojo基准测试中实现了4.70%的绝对性能提升。此外，我们的方法在基于合成数据的分布外miniF2F基准测试中实现了2.47%的绝对性能提升。为了提供进一步的见解，我们对合成数据组成和训练范式进行了全面的分析，为开发强大的定理证明器提供了有价值的指导。
🔬 方法详解
问题定义：论文旨在解决神经定理证明（NTP）中数据稀缺的问题。现有的形式化语料库规模有限，不足以训练出高性能的定理证明模型。这限制了NTP在复杂定理证明任务中的应用。
核心思路：论文的核心思路是通过符号变异自动生成新的形式化定理，从而扩充训练数据集。通过对现有定理进行等价变换或应用相关定理，生成语义上等价但形式上不同的新定理。这样可以在不引入额外人工标注的情况下，显著增加训练数据的规模和多样性。
技术框架：Alchemy框架主要包含以下几个阶段：1) 从Mathlib等形式化库中选取候选定理；2) 识别可应用于候选定理的定理（可用于重写或应用）；3) 通过替换候选定理中的项（term）及其等价形式或前件，进行符号变异；4) 将生成的新定理加入训练数据集，用于模型的持续预训练和监督微调。
关键创新：Alchemy的关键创新在于其符号变异策略，它能够自动生成大量高质量的形式化定理。与传统的数据增强方法相比，Alchemy利用形式化系统的内在逻辑，保证了生成数据的正确性和一致性。此外，Alchemy是一个通用的框架，可以应用于不同的形式化系统和定理证明任务。
关键设计：Alchemy框架的关键设计包括：1) 如何高效地识别可应用于候选定理的定理；2) 如何选择合适的变异策略，以保证生成数据的质量和多样性；3) 如何平衡原始数据和合成数据在训练中的比例，以避免模型过拟合合成数据。论文中可能使用了启发式搜索或机器学习方法来解决这些问题，但具体细节未知。
🖼️ 关键图片
📊 实验亮点
实验结果表明，Alchemy在Leandojo基准测试中实现了4.70%的绝对性能提升，在分布外miniF2F基准测试中实现了2.47%的绝对性能提升。这些结果表明，通过符号变异合成数据可以有效提升神经定理证明器的泛化能力，使其能够处理更复杂的定理证明任务。
🎯 应用场景
该研究成果可应用于自动化定理证明、形式化验证、程序验证等领域。通过扩充训练数据，可以提升神经定理证明器的性能，使其能够自动证明更复杂的定理，从而提高软件和硬件系统的可靠性和安全性。未来，该技术有望应用于智能合约验证、AI安全等新兴领域。
📄 摘要（原文）
Formal proofs are challenging to write even for experienced experts. Recent progress in Neural Theorem Proving (NTP) shows promise in expediting this process. However, the formal corpora available on the Internet are limited compared to the general text, posing a significant data scarcity challenge for NTP. To address this issue, this work proposes Alchemy, a general framework for data synthesis that constructs formal theorems through symbolic mutation. Specifically, for each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. Subsequently, we mutate the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M. Furthermore, we perform continual pretraining and supervised finetuning on this augmented corpus for large language models. Experimental results demonstrate the effectiveness of our approach, achieving a 4.70% absolute performance improvement on Leandojo benchmark. Additionally, our approach achieves a 2.47% absolute performance gain on the out-of-distribution miniF2F benchmark based on the synthetic data.To provide further insights, we conduct a comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.