从合成定理中学习证明
计算机科学中的逻辑
2020-06-22 v1 机器学习
摘要
将机器学习应用于自动定理证明的一大挑战是训练数据的稀缺，而训练数据是训练成功深度学习模型的关键要素。为应对此问题，我们提出一种依赖于从一组公理生成的合成定理进行训练的方法。我们表明此类定理可用于训练自动证明器，且所学证明器能成功迁移至人类生成的定理。我们证明，仅在合成定理上训练的证明器可解决 TPTP（一个用于比较最先进启发式证明器的基准数据集）中相当比例的题目。我们的方法在大多数公理集上优于在人类生成问题上训练的模型，从而展示了合成数据用于该任务的前景。
引用
@article{arxiv.2006.11259,
title = {Learning to Prove from Synthetic Theorems},
author = {Eser Aygün and Zafarali Ahmed and Ankit Anand and Vlad Firoiu and Xavier Glorot and Laurent Orseau and Doina Precup and Shibl Mourad},
journal= {arXiv preprint arXiv:2006.11259},
year = {2020}
}
备注
17 pages, 6 figures, submitted to NeurIPS 2020