Learning to Prove Theorems by Learning to Generate Theorems
arXiv:2002.07019
Abstract
We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited human-written theorems and proofs available for supervised learning. To address this limitation, we propose to learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover and advances the state of the art of automated theorem proving in Metamath. Code is available at https://github.com/princeton-vl/MetaGen.
References in corpus (12)
- Adam: A Method for Stochastic Optimization
- Intrinsic Motivation and Automatic Curricula via Asymmetric Self-Play
- DeepMath - Deep Sequence Models for Premise Selection
- Generative Language Modeling for Automated Theorem Proving
- Holophrasm: a neural Automated Theorem Prover for higher-order logic
- Learning to Prove Theorems via Interacting with Proof Assistants
- Hammering Mizar by Learning Clause Guidance
- Learning to Reason in Large Theories without Imitation
- Learning Goal Embeddings via Self-Play for Hierarchical Reinforcement Learning
- Mathematical Reasoning in Latent Space
- On Learning to Prove
- Learning dynamic polynomial proofs