Machine Learning for Automated Theorem Proving

自动定理证明器如何利用机器学习技术，开发更有效的证明发现方法，并扩展其能力？这个更广泛的问题是这项研究的主题。自动定理证明器(或ATP系统)在人工智能应用中提供了精确逻辑推理的手段。例如，语义推理者可以使用ATP系统从形式知识库中得出逻辑结论。ATP系统也通常用于形式验证；如果没有ATP，对复杂系统的严格数学验证将是最好的，如果不是不可行的话。ATP系统使用推理过程和启发式搜索的组合来生成数学证明。启发式算法很复杂，而且参数很高。多年来，ATP系统的性能有了令人印象深刻的改进，其应用也相应增加。一个例子是Flyspeck项目，它正式证明了开普勒猜想的一个极其复杂的证明，开普勒猜想是离散几何学中最古老的问题(提出于1611年)。当前ATP系统中的启发式算法及其参数是手动开发的，并由大量繁琐的实验支持。(相对而言)很容易找到证明避开这种预先确定的系统的定理。通常需要针对特定问题进行手动调整。这种手动调整和启发式开发阻碍了ATP系统的应用。一个有前途的替代方案是使用机器学习从更广泛的参数中自动选择，自动学习这些参数，并生成新的启发式。这是一个令人鼓舞的研究领域，取得了一些成功，也提出了许多悬而未决的问题；我们希望通过这项工作回答其中一些问题。

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.