基于深度图嵌入的定理证明前提选择

我们提出了一种基于深度学习的方法来解决前提选择问题：即选择与证明给定猜想相关的数学陈述。我们将高阶逻辑公式表示为一个对变量重命名具有不变性的图，同时完全保留了其语法和语义信息。然后，通过一种新颖的嵌入方法将该图嵌入到向量中，该方法能够保留边的顺序信息。我们的方法在HolStep数据集上取得了最先进的结果，将分类准确率从83%提高到了90.3%。