Learning to Prove Theorems by Learning to Generate Theorems
This addresses a key bottleneck in automated theorem proving for AI researchers, though it is an incremental improvement over existing deep learning methods.
The paper tackles the limited availability of human-written theorems and proofs for training automated theorem provers by proposing a neural generator to synthesize theorems and proofs, which improves the theorem prover and advances state-of-the-art results in Metamath.
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.