MaSh: Machine Learning for Sledgehammer

Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban

Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013), Lecture Notes in Computer Science 7998, pp. 35 – 50, 2013.


Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the relevance filter, heuristically ranks the thousands of facts available and selects a subset, based on syntactic similarity to the current goal. We introduce MaSh, an alternative that learns from successful proofs. New challenges arose from our “zero-click” vision: MaSh should integrate seamlessly with the users’ workflow, so that they benefit from machine learning without having to install software, set up servers, or guide the learning. The underlying machinery draws on recent research in the context of Mizar and HOL Light, with a number of performance enhancements. MaSh outperforms the old relevance filter on large formalizations, and a particularly strong filter is obtained by combining the two filters.


  PDF |    doi:10.1007/978-3-642-39634-2_6  |  © Springer


author = "Daniel K{\"u}hlwein and Jasmin Christian Blanchette and
Cezary Kaliszyk and Josef Urban",
title = "{MaSh}: Machine Learning for {Sledgehammer}",
booktitle = "Proceedings of the 4th International Conference on Interactive Theorem Proving",
editor = "Sandrine Blazy and Christine Paulin-Mohring and David Pichardie",
series = "Lecture Notes in Computer Science",
volume = 7998,
pages = "35--50",
publisher = "Springer-Verlag",
year = 2013,
doi = "10.1007/978-3-642-39634-2_6"
Nach oben scrollen