NeurIPS 2017spotlight184 citations
Premise Selection for Theorem Proving by Deep Graph Embedding
Mingzhe Wang, Yihe Tang, Jian Wang, Jia Deng
Abstract
We propose a deep learning-based approach to the problem of premise selection: selecting mathematical statements relevant for proving a given conjecture. We represent a higher-order logic formula as a graph that is invariant to variable renaming but still fully preserves syntactic and semantic information. We then embed the graph into a vector via a novel embedding method that preserves the information of edge ordering. Our approach achieves state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%.
BibTeX
@inproceedings{NIPS2017_18d10dc6,
author = {Wang, Mingzhe and Tang, Yihe and Wang, Jian and Deng, Jia},
booktitle = {Advances in Neural Information Processing Systems},
editor = {I. Guyon and U. Von Luxburg and S. Bengio and H. Wallach and R. Fergus and S. Vishwanathan and R. Garnett},
pages = {},
publisher = {Curran Associates, Inc.},
title = {Premise Selection for Theorem Proving by Deep Graph Embedding},
url = {https://proceedings.neurips.cc/paper_files/paper/2017/file/18d10dc6e666eab6de9215ae5b3d54df-Paper.pdf},
volume = {30},
year = {2017}
}