Machine Learning for Automated Theorem Proving

Lead Research Organisation: University of Cambridge
Department Name: Computer Laboratory

Abstract

How can automated theorem provers utilise machine learning techniques, to
develop more efficient methods of proof discovery, and to expand their
capabilities? This broader question is the subject of this research.

Automated theorem provers (or ATP systems) provide means of exact logical
reasoning in artificial intelligence applications. For example, semantic
reasoners can use ATP systems to draw logical conclusions from formal
knowledge-bases. ATP systems are also commonly used in formal verification;
without ATP, rigorous mathematical verification of complex systems would be
tedious, if not infeasible.

ATP systems generate mathematical proofs using a combination of inference
procedures and heuristic search. The heuristics are complex and highly
parametrised. ATP systems have seen impressive improvements in their
capabilities over the years, and a corresponding increase in their
applications. An example is the Flyspeck project, which formalised an
extremely complex proof of the Kepler conjecture, the oldest problem in
discrete geometry (presented in 1611).

The heuristics and their parameters in current ATP systems are manually
developed and supported by large and tedious sets of experiments. It is easy
(relatively speaking) to find theorems for which the proof evades such a
pre-determined system. Problem specific manual tuning is often required. Such
manual tuning and heuristic development hinders applications of ATP systems.

A promising alternative is the use of machine learning to select automatically
from a wider range of parameters, to learn such parameters automatically, and
to generate new heuristics. This is an encouraging area of research, with some
recent successes and plenty of open questions; some of which we hope to answer
through this work.

Publications

10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509620/1 30/09/2016 29/09/2022
1788755 Studentship EP/N509620/1 30/09/2016 30/03/2020 Chaitanya Mangla
 
Description We have published work that shows how machine learning can be used to optimise SMT solvers. Such solver are actively used in industry for safety and security of engineered systems. Our contributions should eventually materialise in society as improvements in safety and security of computer systems and other manufactured products.