Applications of Machine Learning to Automated Reasoning

Abstract

Systems that can automate some aspects of logical reasoning are now very strong, through years of theoretical and practical development. Some progress has been made to have such systems learn from past experience. One extremely general and theoretically-favourable approach is to integrate learned guidance inside a system, biasing its internal search routines to explore promising areas earlier. Unfortunately, the approach has some barriers to practicality, notably the penalty on raw, inferences-per-second performance. We explore a number of approaches around this area designed to circumvent these barriers while making other trade-offs. The setting considered is automated theorem provers for first-order logic, but work is broadly applicable outside this area.

Date of Award	7 Jun 2021
Original language	English
Awarding Institution	The University of Manchester
Supervisor	Andrei Voronkov (Co Supervisor) & Giles Reger (Main Supervisor)