图表示在高阶逻辑和定理证明中的应用

本文首次将图神经网络（GNNs）应用于高阶证明搜索，并展示了GNNs在该领域的性能优于现有最佳方法。交互式高阶定理证明器可以形式化大多数数学理论，但对深度学习而言，它们构成了一个重大挑战。高阶逻辑具有很高的表达能力，尽管其语法和语义定义明确且结构良好，但目前仍缺乏一种公认的方法将其公式转换为基于图的表示。在本文中，我们考虑了几种高阶逻辑的图表示方法，并针对高阶定理证明的HOList基准进行了评估。