论文标题
学会通过学习生成定理来证明定理
Learning to Prove Theorems by Learning to Generate Theorems
论文作者
论文摘要
我们考虑自动定理证明的任务，这是一个关键的AI任务。深度学习已经显示出对培训定理掠夺者的希望，但是人工写的定理和可用于监督学习的证据有限。为了解决这一限制，我们建议学习一个神经发电机，该神经发电机自动合成定理和证明，以培训定理供者。对现实世界任务的实验表明，来自我们方法的合成数据可改善定理供者，并提高自动化定理的现状，证明在metamath中。代码可从https://github.com/princeton-vl/metagen获得。
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.
