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.
@InProceedings{jakubuv_et_al:LIPIcs.ITP.2019.34, author = {Jakub\r{u}v, Jan and Urban, Josef}, title = {{Hammering Mizar by Learning Clause Guidance}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {34:1--34:8}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.34}, URN = {urn:nbn:de:0030-drops-110898}, doi = {10.4230/LIPIcs.ITP.2019.34}, annote = {Keywords: Proof automation, ITP hammers, Automated theorem proving, Machine learning} }
Feedback for Dagstuhl Publishing