基于学习的Flyspeck自动推理
人工智能
2021-12-03 v3 数字图书馆
机器学习
计算机科学中的逻辑
摘要
将Flyspeck项目编码的大量数学知识与外部自动定理证明器（ATP）以及基于证明训练的机器学习前提选择方法相结合，产生了一个能够自动回答广泛数学查询的人工智能系统。该架构的性能在一个模拟Flyspeck从公理到最后一个定理开发的引导场景中进行了评估，每次仅使用之前的定理和证明。结果表明，在14个CPU的工作站上，14185个定理中有39%可以在30秒的实时时间内以按钮模式（无需任何高级建议和用户交互）得到证明。必要的工作包括：（i）将HOL Light逻辑可靠翻译为ATP形式（无类型一阶、多态类型一阶和类型高阶）的实现；（ii）从HOL Light和ATP证明中导出依赖信息以供机器学习使用；（iii）选择适当的表示和方法从先前的证明中学习，并将其作为顾问与HOL Light集成。本文描述并讨论了这项工作，并提供了对完全自动发现的证明主体的初步分析。
引用
@article{arxiv.1211.7012,
title = {Learning-Assisted Automated Reasoning with Flyspeck},
author = {Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:1211.7012},
year = {2021}
}