通过学习生成定理来学习证明定理

我们研究自动化定理证明这一关键的人工智能任务。深度学习在训练定理证明器方面展现出巨大潜力，但可用于监督学习的人工编写的定理与证明数据极为有限。为解决这一瓶颈，我们提出了一种神经生成模型，能够自动合成定理及其证明，用于训练定理证明器。在真实世界任务上的实验表明，基于本方法生成的合成数据显著提升了定理证明器的性能，并推动了Metamath平台下自动化定理证明技术的最新进展。相关代码已开源，地址为：https://github.com/princeton-vl/MetaGen。