基于深度图嵌入的定理证明前提选择
人工智能
2017-10-09 v1 机器学习
计算机科学中的逻辑
摘要
我们提出了一种基于深度学习的方法来解决前提选择问题：即选择与证明给定猜想相关的数学陈述。我们将高阶逻辑公式表示为对变量重命名不变但仍完全保留语法和语义信息的图。然后，我们通过一种保留边顺序信息的新型嵌入方法将该图嵌入到向量中。我们的方法在 HolStep 数据集上取得了 SOTA 结果，将分类准确率从 83% 提高到了 90.3%。
关键词
引用
@article{arxiv.1709.09994,
title = {Premise Selection for Theorem Proving by Deep Graph Embedding},
author = {Mingzhe Wang and Yihe Tang and Jian Wang and Jia Deng},
journal= {arXiv preprint arXiv:1709.09994},
year = {2017}
}
备注
Mingzhe Wang and Yihe Tang contributed equally