TY - JOUR
T1 - Learning to prove theorems by learning to generate theorems
AU - Wang, Mingzhe
AU - Deng, Jia
N1 - Funding Information:
Acknowledgements This work is partially supported by the National Science Foundation under Grant IIS-1903222 and the Office of Naval Research under Grant N00014-20-1-2634.
Publisher Copyright:
© 2020 Neural information processing systems foundation. All rights reserved.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85106646313&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85106646313&partnerID=8YFLogxK
M3 - Conference article
AN - SCOPUS:85106646313
SN - 1049-5258
VL - 2020-December
JO - Advances in Neural Information Processing Systems
JF - Advances in Neural Information Processing Systems
T2 - 34th Conference on Neural Information Processing Systems, NeurIPS 2020
Y2 - 6 December 2020 through 12 December 2020
ER -