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