arXiv:2410.15748v2 宣告类型: 替换 摘要: 就即使是经验丰富的专家来说，编写形式证明也是非常具挑战性的。神经定理证明（NTP）的近期进展显示出加快这一过程的潜力。然而，互联网上可用的形式语料库相较于通用文本来说数量有限，这给NTP带来了显著的数据稀缺挑战。为了解决这个问题，本研究提出了Alchemy，一种一般性的数据合成框架，通过符号变异构建形式定理。具体而言，对于Mathlib中的每个候选定理，我们识别所有可调用的定理，这些定理可以用于重写或应用到该候选定理上。随后，我们通过用其等效形式或前提替换候选定理中的相应项来变异候选定理。结果，我们的方法将Mathlib中的定理数量提高了十倍，从110k增加到6M。此外，我们对这个扩充了的语料库进行了持续的预训练和监督微调，以改进大型语言模型。实验结果表明，我们的方法在Leandojo基准测试中实现了4.70%的绝对性能提升。此外，基于合成数据，我们的方法在out-of-distribution miniF2F基准测试中实现了2.47%的绝对性能提升。为了提供进一步的见解，我们对合成数据构成和训练范式进行了全面分析，为开发强大的定理证明器提供了宝贵的指导。