Training a First-Order Theorem Prover from Synthetic Data
arXiv:2103.03798
Abstract
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 purely with synthetically generated theorems, without any human data aside from axioms. We use these theorems to train a neurally-guided saturation-based prover. Our neural prover outperforms the state-of-the-art E-prover on this synthetic data in both time and search steps, and shows significant transfer to the unseen human-written theorems from the TPTP library, where it solves 72\% of first-order problems without equality.
References in corpus (8)
- Language Models are Few-Shot Learners
- Scaling Laws for Neural Language Models
- A Generalization of Transformer Networks to Graphs
- Generative Language Modeling for Automated Theorem Proving
- Automated curricula through setter-solver interactions
- Learning to Prove Theorems via Interacting with Proof Assistants
- HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
- Proof Artifact Co-training for Theorem Proving with Language Models