“Learning to Prove Theorems by Learning to Generate Theorems”, Mingzhe Wang, Jia Deng2020-02-17 (math, model-based RL; backlinks; similar)⁠:

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 Github.

Backlinks:

Similar Links: