【普林斯顿博士论文】深度学习在自动定理证明中的应用, 95页pdf

https://dataspace.princeton.edu/handle/88435/dsp014j03d298b自动定理证明是一项基本的AI任务，它对数学的形式化、软件和硬件的验证以及程序合成都有广泛的应用。深度学习已经成为指导定理证明器的一个有希望的方法。在这篇论文中，我们介绍了我们在开发深度学习方法用于自动定理证明方面的工作。首先，我们提出了FormulaNet，这是一个基于深度学习的问题前提选择方法。FormulaNet将逻辑公式表示为一个对变量重命名保持不变的图，然后通过一种新颖的图嵌入方法将图嵌入到向量中，该方法保留了边排序的信息。我们的方法在HolStep数据集上达到了最先进的结果，将分类精度从83%提高到了90.3%。接下来，我们提出了MetaGen，一个自动生成定理和证明以训练定理证明器的神经生成器。在实际任务中，我们证明了我们的方法产生的合成数据改进了定理证明器，并且推进了Metamath中自动定理证明的最新技术状态。最后，我们将我们的定理生成器扩展到交互式定理证明器Lean上。我们提出了TermGen，一个自动在Lean中合成定理和证明的神经生成器，通过直接构建证明项来实现。我们还提出了一种专家迭代的方法，用于训练TermGen合成短定理。最后，我们通过一个基于规则的定理生成器，展示了生成while循环程序的形式规范的案例研究。