借助数百万引理的学习辅助定理证明
人工智能
2014-02-17 v1 数字图书馆
机器学习
计算机科学中的逻辑
摘要
大型形式化数学库包含数百万个原子推理步骤，这些步骤产生了相应数量的已证明陈述（引理）。与非形式化的数学实践类似，这些陈述中只有极小一部分被形式化数学家命名并在后续证明中重用。在这项工作中，我们提出并实现了定义 HOL Light 引理在证明进一步定理时的估计有用性的标准。我们使用这些标准来挖掘 HOL Light 和 Flyspeck 库中引理的大型推理图，将多达数百万个最佳引理添加到可在后续证明中重用的陈述池中。我们表明，结合基于学习的相关性过滤，这些方法显著增强了在大型形式化数学库（如 Flyspeck）上对新猜想的自动定理证明。
引用
@article{arxiv.1402.3578,
title = {Learning-assisted Theorem Proving with Millions of Lemmas},
author = {Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:1402.3578},
year = {2014}
}
备注
journal version of arXiv:1310.2797 (which was submitted to LPAR conference)