Skip to main content

Learning to Prove Theorems by Learning to Generate Theorems

Author(s): Wang, Mingzhe; Deng, Jia

To refer to this page use:
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.
Publication Date: 2020
Citation: Wang, Mingzhe, and Jia Deng. "Learning to Prove Theorems by Learning to Generate Theorems." In Advances in Neural Information Processing Systems 33 (2020).
ISSN: 1049-5258
Type of Material: Conference Article
Journal/Proceeding Title: Advances in Neural Information Processing Systems
Version: Final published version. Article is made available in OAR by the publisher's permission or policy.

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.