Premise Selection for Theorem Proving by Deep Graph Embedding
Artificial Intelligence
2017-10-09 v1 Machine Learning
Logic in Computer Science
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%.
Cite
@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}
}
Comments
Mingzhe Wang and Yihe Tang contributed equally