Learning to Prove from Synthetic Theorems

• DOI: 10.48550/arxiv.2006.11259
• Publication Date: 2020-01-01
• Authors: Aygün, Eser; Ahmed, Zafarali; Anand, Ankit; Firoiu, Vlad; Glorot, Xavier; Orseau, Laurent; Precup, Doina; Mourad, Shibl
• Keywords: FOS: Computer and information sciences; Computer Science - Logic in Computer Science; Computer Science - Machine Learning; I.2.3; 01 natural sciences; 0105 earth and related environmental sciences; Logic in Computer Science (cs.LO); Machine Learning (cs.LG)

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.<br/>17 pages, 6 figures, submitted to NeurIPS 2020<br/>