摘要
大规模计算机可理解的证明由数百万个中间逻辑步骤组成。这些步骤中的绝大多数来源于针对中间目标手动选择和手动引导的启发式方法。迄今为止，机器学习通常未被用于筛选或生成这些步骤。在本文中，我们介绍了一个基于高阶逻辑（Higher-Order Logic, HOL）证明的新数据集，旨在开发新的基于机器学习的定理证明策略。该数据集已根据BSD许可证公开发布。我们提出了可以在该数据集上执行的各种机器学习任务，并讨论了它们对定理证明的意义。此外，我们还对一组适用于这些任务的简单基线机器学习模型（包括逻辑回归、卷积神经网络和递归神经网络）进行了基准测试。我们的基线模型的结果表明，将机器学习应用于HOL定理证明具有巨大的潜力。
基准测试
| 基准 | 方法 | 指标 |
|---|---|---|
| automated-theorem-proving-on-holstep | Siamese 1D CNN | Classification Accuracy: 0.82 |
| automated-theorem-proving-on-holstep | Siamese 1D CNN-LSTM | Classification Accuracy: 0.83 |
| automated-theorem-proving-on-holstep-1 | 1D CNN | Classification Accuracy: 0.83 |
| automated-theorem-proving-on-holstep-1 | 1D CNN-LSTM | Classification Accuracy: 0.83 |