Title: Premise Selection for Theorem Proving by Deep Graph Embedding,
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%.