Premise Selection for Theorem Proving by Deep Graph Embedding
This work addresses the challenge of automating mathematical theorem proving by improving premise selection accuracy, which is incremental but domain-specific.
The paper tackles the problem of premise selection for theorem proving by representing logic formulas as graphs and embedding them with a novel method that preserves edge ordering, achieving state-of-the-art results with an accuracy improvement from 83% to 90.3% on the HolStep dataset.
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%.