Premise selection with neural networks and distributed representation of features

TL;DR

This paper introduces a neural network-based method for premise selection in automated theorem proving, using distributed embeddings of functional signatures to improve accuracy and efficiency.

Contribution

It proposes a novel approach that employs dimensionality reduction and distributed representations of premise features, enhancing premise selection performance.

Findings

Achieved 76.45% accuracy in premise selection.

Used 512-dimensional embeddings for conjecture-axiom pairs.

Demonstrated effectiveness of simple neural networks with feature embeddings.

Abstract

We present the problem of selecting relevant premises for a proof of a given statement. When stated as a binary classification task for pairs (conjecture, axiom), it can be efficiently solved using artificial neural networks. The key difference between our advance to solve this problem and previous approaches is the use of just functional signatures of premises. To further improve the performance of the model, we use dimensionality reduction technique, to replace long and sparse signature vectors with their compact and dense embedded versions. These are obtained by firstly defining the concept of a context for each functor symbol, and then training a simple neural network to predict the distribution of other functor symbols in the context of this functor. After training the network, the output of its hidden layer is used to construct a lower dimensional embedding of a functional signature (for each premise) with a distributed representation of features. This allows us to use 512-dimensional embeddings for conjecture-axiom pairs, containing enough information about the original statements to reach the accuracy of 76.45% in premise selection task, only with simple two-layer densely connected neural networks.