Premise Selection for Theorem Proving by Deep Graph Embedding

TL;DR

This paper introduces a deep learning method that represents higher-order logic formulas as graphs and embeds them into vectors, significantly improving premise selection accuracy for theorem proving.

Contribution

It presents a novel graph embedding technique that preserves syntactic, semantic, and edge ordering information, advancing premise selection in automated theorem proving.

Findings

Achieved 90.3% classification accuracy on HolStep dataset

Outperformed previous methods with 83% accuracy

Introduced a variable-renaming invariant graph representation

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%.