Machine Learning for Automated Theorem Proving

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.