Machine Learning for Heuristic Optimisation and Premise Selection in Automated Theorem Proving

Abstract

Automated Theorem Provers are essential tools for constructing formal and rigorous proofs. Unambiguous and mechanically verifiable proofs have numerous applications for mathematics and for software and hardware verification. State-of-the-art theorem provers are sophisticated and mature systems implementing multiple calculi and a long list of preprocessing and redundancy elimination techniques. Nevertheless, theorem proving is a challenging and complex process as the proof search quickly results in a combinatorial explosion of the search space. Consequently, most proofs are either found quickly or not at all. This makes solving hard problems that are expected to require more ``thinking'' exceedingly challenging, especially as problems are diverse and no search strategy fits all problems. The solution proposed in this work is twofold: i) tune the prover to specific instances to avoid unnecessary exploration of the search space, and ii) reduce the initial problem to only the indispensable elements to prolong a manageable search space. First, I developed a method for automatically discovering efficient configurations and constructing heuristic schedules over sets of heterogeneous problems. The result is a reduction of the average solving time by 54.4% and a 14.8% increase in the number of solved compared with our baseline. Further, I combined graph neural networks with a sequential language model via transfer learning to remove superfluous formulae. The approach significantly outperforms related machine learning methods and increases the number of solved problems by 17.7% over the baseline.

Date of Award	13 Jun 2023
Original language	English
Awarding Institution	The University of Manchester
Supervisor	Konstantin Korovin (Main Supervisor) & Ross King (Co Supervisor)