Alchemy：通过符号突变放大定理证明能力
人工智能
2025-04-04 v2
摘要
形式化证明即使对于经验丰富的专家来说也具有挑战性。最近的神经定理证明（NTP）取得的进展在加速这一过程方面显示出前景。然而，互联网上可获得的形式语料库相对于一般文本而言有限，为 NTP 带来了显著的数据稀缺挑战。为此，本工作提出 Alchemy，一个用于数据合成的通用框架，通过符号突变构建形式定理。具体而言，对于每个候选定理，我们识别所有可调用的定理，这些定理可用于重写或应用该定理。随后，我们通过替换其等价形式或先决条件来突变候选定理。结果是，我们的方法将 Mathlib 中的定理数量提高了一个数量级，从 11 万增加到 600 万。此外，我们对这个增强后的语料库进行持续预训练和监督式微调，以获得大型语言模型。实验结果表明，我们的方法有效， 在 Leandojo 基准上实现了 4.70% 的绝对性能提升。此外，我们的方法在基于合成数据的 out-of-distribution miniF2F 基准上实现了 2.47% 的绝对性能提升。为提供进一步见解，我们对合成数据组成和训练范式进行了全面分析，为开发强大的定理证明器提供了有价值的指导。
关键词
引用
@article{arxiv.2410.15748,
title = {Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation},
author = {Shaonan Wu and Shuai Lu and Yeyun Gong and Nan Duan and Ping Wei},
journal= {arXiv preprint arXiv:2410.15748},
year = {2025}
}