An application of artificial neural networks to premise selection in automated reasoning

Abstract

In this thesis, we present how machine learning can be deployed in the automated reasoning ambience. In particular, we show that artificial neural networks can help with the premise selection problem when it is expressed as a binary classification task. Given a conjecture and a set of axioms, one can label each conjecture-axiom pair as a positive example, if it is known that a proof, which relies on the axiom, can be constructed for the conjecture, or, if it is not the case, as a negative example. A neural network can then be constructed, which takes some representation of the conjecture-axiom pairs as its input, and outputs a probability that a given pair is a positive example. The representation of premises (axioms and conjectures), which we consider, are obtained by extracting functional symbols from the premises' corpora and forming contextual distribution vectors of symbols, which coexist in some circumstances. These vectors can then be exploited in order to procure a dimensionality-reduced representation of premises. Equipped with these condensed data, we explore several neural network models: logistic regression, dense networks with one or two hidden layers, feed-forward networks with one or two residual blocks, recurrent neural networks (simple, LSTM, GRU) in unidirectional and bidirectional setting, optionally having a dense hidden layer preceding the classifier. The accuracy, which we obtain, oscillates around 72%, exceeding 75% in the best-case scenario.

Date of Award	1 Aug 2020
Original language	English
Awarding Institution	The University of Manchester
Supervisor	Konstantin Korovin (Supervisor) & Ross King (Supervisor)