Machine Learning for Automated Theorem Proving
Lead Research Organisation:
University of Cambridge
Department Name: Computer Science and Technology
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.
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.
Organisations
Publications
Mangla C
(2020)
Bayesian Optimisation of Solver Parameters in CBMC
Mangla C.
(2020)
Bayesian optimisation of solver parameters in CBMC
in CEUR Workshop Proceedings
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. |