Machine Learning for Automated Theorem Proving

点击翻译按钮获取中文摘要

How can automated theorem provers utilise machine learning techniques, todevelop more efficient methods of proof discovery, and to expand theircapabilities? This broader question is the subject of this research.Automated theorem provers (or ATP systems) provide means of exact logicalreasoning in artificial intelligence applications. For example, semanticreasoners can use ATP systems to draw logical conclusions from formalknowledge-bases. ATP systems are also commonly used in formal verification;without ATP, rigorous mathematical verification of complex systems would betedious, if not infeasible.ATP systems generate mathematical proofs using a combination of inferenceprocedures and heuristic search. The heuristics are complex and highlyparametrised. ATP systems have seen impressive improvements in theircapabilities over the years, and a corresponding increase in theirapplications. An example is the Flyspeck project, which formalised anextremely complex proof of the Kepler conjecture, the oldest problem indiscrete geometry (presented in 1611).The heuristics and their parameters in current ATP systems are manuallydeveloped and supported by large and tedious sets of experiments. It is easy(relatively speaking) to find theorems for which the proof evades such apre-determined system. Problem specific manual tuning is often required. Suchmanual tuning and heuristic development hinders applications of ATP systems.A promising alternative is the use of machine learning to select automaticallyfrom a wider range of parameters, to learn such parameters automatically, andto generate new heuristics. This is an encouraging area of research, with somerecent successes and plenty of open questions; some of which we hope to answerthrough this work.