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.
@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}
}