论文标题
学会从合成定理证明
Learning to Prove from Synthetic Theorems
论文作者
论文摘要
将机器学习应用于自动化定理证明的一个主要挑战是培训数据的稀缺性，这是培训成功的深度学习模型的关键要素。为了解决这个问题，我们提出了一种依赖于一组公理产生的合成定理训练的方法。我们表明，这种定理可以用来训练自动化的谚语，并且学识渊博的鄙视者成功地转移到了人类生成的定理中。我们证明，经过合成定理的训练者可以解决TPTP的大量问题，TPTP是一个基准数据集中的大量问题，用于比较最新的启发式鉴定。在大多数公理集中，我们的方法优于对人类产生的问题训练的模型，从而显示出使用合成数据执行此任务的希望。
A major challenge in applying machine learning to automated theorem proving is the scarcity of training data, which is a key ingredient in training successful deep learning models. To tackle this problem, we propose an approach that relies on training with synthetic theorems, generated from a set of axioms. We show that such theorems can be used to train an automated prover and that the learned prover transfers successfully to human-generated theorems. We demonstrate that a prover trained exclusively on synthetic theorems can solve a substantial fraction of problems in TPTP, a benchmark dataset that is used to compare state-of-the-art heuristic provers. Our approach outperforms a model trained on human-generated problems in most axiom sets, thereby showing the promise of using synthetic data for this task.
