MizAR 40 献礼 Mizar 40
人工智能
2017-04-13 v1 数字图书馆
机器学习
计算机科学中的逻辑
数学软件
摘要
作为献给 Mizar 成立 40 周年的礼物，我们开发了一个 AI/ATP 系统，该系统在 14 核 CPU 机器上仅需 30 秒实时时间，即可自动证明最新官方版 Mizar 数学库 (MML) 中 40% 的定理。相较于此前在整个 MML 上测量的大型理论 AI/ATP 方法的性能，这是一个显著的改进。为实现这一目标，我们采用并进一步发展了一整套 AI/ATP 方法。我们高效地实现了最有用的方法，将其扩展至 MML 中的 150,000 个公式。这将语料库上的训练时间减少到 1-3 秒，从而使得这些方法能够简单地实际部署于面向 Mizar 用户的在线自动推理服务 (MizAR) 中。
引用
@article{arxiv.1310.2805,
title = {MizAR 40 for Mizar 40},
author = {Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:1310.2805},
year = {2017}
}