Learning to Prove Theorems by Learning to Generate Theorems
Published in
Neural Information Processing Systems(2020)External Links:
TL
TL;DR
This work proposes to learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover, and demonstrates that synthetic data from this approach improves the theorem provers and advances the state of the art of automated theorem proving in Metamath.
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.
References49 items
1
Generative Language Modeling for Automated Theorem Proving
2
First Neural Conjecturing Datasets and Experiments
3
Mathematical Reasoning in Latent Space
4
Learning dynamic polynomial proofs
5