摘要
我们提出了一种基于深度学习的方法来解决前提选择问题：即选择与证明给定猜想相关的数学陈述。我们将高阶逻辑公式表示为一个对变量重命名具有不变性的图，同时完全保留了其语法和语义信息。然后，通过一种新颖的嵌入方法将该图嵌入到向量中，该方法能够保留边的顺序信息。我们的方法在HolStep数据集上取得了最先进的结果，将分类准确率从83%提高到了90.3%。
代码仓库
princeton-vl/FormulaNet
官方
pytorch
基准测试
| 基准 | 方法 | 指标 |
|---|---|---|
| automated-theorem-proving-on-holstep | FormulaNet-basic | Classification Accuracy: 0.891 |
| automated-theorem-proving-on-holstep | FormulaNet | Classification Accuracy: 0.903 |
| automated-theorem-proving-on-holstep-1 | FormulaNet-basic | Classification Accuracy: 0.890 |
| automated-theorem-proving-on-holstep-1 | FormulaNet | Classification Accuracy: 0.900 |