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 conjectureaxiom 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 conjectureaxiom 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 dimensionalityreduced representation of premises. Equipped with these condensed data, we explore several neural network models: logistic regression, dense networks with one or two hidden layers, feedforward 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 bestcase scenario.
Date of Award  1 Aug 2020 

Original language  English 

Awarding Institution   The University of Manchester


Supervisor  Konstantin Korovin (Supervisor) & Ross King (Supervisor) 

 perceptron
 multilayer perceptron
 automated theorem proving
 residual connection
 logistic regression
 feedforward network
 contextual embedding
 recurrent neural network
 DeepMath
 TPTP
 Mizar project
 artificial neural network
 automated reasoning
 premise selection
 dimensionality reduction
An application of artificial neural networks to premise selection in automated reasoning
Kucik, A. (Author). 1 Aug 2020
Student thesis: Master of Philosophy