LIPIcs.ITP.2019.34.pdf
- Filesize: 353 kB
- 8 pages
Document
Hammering Mizar by Learning Clause Guidance (Short Paper)
Authors
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
Cite AsGet BibTex
Jan Jakubův and Josef Urban. Hammering Mizar by Learning Clause Guidance (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 34:1-34:8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.34
https://doi.org/10.4230/LIPIcs.ITP.2019.34
Abstract
We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated state-of-the-art machine learners into the E automated theorem prover, and developed methods that allow learning and efficient internal guidance of E over the whole Mizar library. The resulting trained system improves the real-time performance of E on the Mizar library by 70% in a single-strategy setting.
Subject Classification
ACM Subject Classification
- Theory of computation → Automated reasoning
- Computing methodologies → Theorem proving algorithms
- Computing methodologies → Machine learning
Keywords
- Proof automation
- ITP hammers
- Automated theorem proving
- Machine learning
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads