面向神经定理证明的 HyperTree 证明搜索
计算与语言
2022-05-24 v1 人工智能
摘要
我们提出一种基于 transformer 的自动定理证明器的在线训练流程。我们的方法利用了一种新的搜索算法——HyperTree 证明搜索（HTPS），其受 AlphaZero 近期成功的启发。我们的模型通过在线训练从先前的证明搜索中学习，使其能够泛化到远离训练分布的区域。我们通过在三个复杂度递增的环境上研究性能，对流程的主要组件进行了详细的消融实验。特别地，我们表明仅使用 HTPS，一个在标注证明上训练的模型就能证明 65.4% 的 Metamath 定理留出集，显著优于 GPT-f 先前 56.5% 的最优水平。对这些未证明定理的在线训练将准确率提升至 82.6%。在相似的计算预算下，我们将基于 Lean 的 miniF2F-curriculum 数据集上的最优证明准确率从 31% 提升至 42%。
引用
@article{arxiv.2205.11491,
title = {HyperTree Proof Search for Neural Theorem Proving},
author = {Guillaume Lample and Marie-Anne Lachaux and Thibaut Lavril and Xavier Martinet and Amaury Hayat and Gabriel Ebner and Aurélien Rodriguez and Timothée Lacroix},
journal= {arXiv preprint arXiv:2205.11491},
year = {2022}
}