权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Machine Learning for Automated Theorem Proving

用于自动定理证明的机器学习

基本信息

批准号：
1788755
负责人：
金额：
--
依托单位：
University of Cambridge
依托单位国家：
英国
项目类别：
Studentship
财政年份：
2016
资助国家：
英国
起止时间：
2016 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=studentship-1788755
关键词：
Machine Learning 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.

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