Learning-Assisted Automated Reasoning with Flyspeck
Learning-Assisted Automated Reasoning with Flyspeck
复制标题
DOI：
10.1007/s10817-014-9303-3
复制
发表时间：
2014-08-01
期刊：
影响因子：
--
通讯作者：
Urban, Josef
中科院分区：
文献类型：
--
作者：
Kaliszyk, Cezary;Urban, Josef
Flyspeck项目编码的大量数学知识与外部自动定理抛弃（ATP）和机器学习前提选择方法结合使用，该方法在Flyspeck证明上训练，生成了能够自动证明广泛数学猜想的AI系统。每次仅使用先前的定理和证明，都会在一个自举的场景中评估该体系结构的性能，从而模拟Flyspeck从公理到最后定理的开发。结果表明，在14185个定理中，有39％可以在14个CPU工作站的30秒内实时以按钮模式（无需任何高级建议和用户互动）证明。必要的工作涉及：（i）HOL LIGHT逻辑向ATP形式主义的声音翻译实现：未型的一阶，多态性键入一阶和键入的高阶，（ii）从HOL Light导出依赖关系信息和机器学习者的ATP证明，以及（iii）选择合适的表示形式和方法，以从以前的证明中学习，以及他们作为HOL Light的顾问的整合。在此处描述和讨论了这项工作，并对完全自动发现的证据体进行了初步分析。
The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the Flyspeck proofs, producing an AI system capable of proving a wide range of mathematical conjectures automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39 % of the 14185 theorems could be proved in a push-button mode (without any high-level advice and user interaction) in 30 seconds of real time on a fourteen-CPU workstation. The necessary work involves: (i) an implementation of sound translations of the HOL Light logic to ATP formalisms: untyped first-order, polymorphic typed first-order, and typed higher-order, (ii) export of the dependency information from HOL Light and ATP proofs for the machine learners, and (iii) choice of suitable representations and methods for learning from previous proofs, and their integration as advisors with HOL Light. This work is described and discussed here, and an initial analysis of the body of proofs that were found fully automatically is provided.