MaSh: Machine Learning for Sledgehammer. Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the relevance ﬁlter, 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’ workﬂow, so that they beneﬁt 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 enhancements. MaSh outperforms the old relevance ﬁlter on large formalizations, and a particularly strong ﬁlter is obtained by combining the two ﬁlters.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
- Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen: Hipster: integrating theory exploration in a proof assistant (2014)
- Heras, Jónathan; Komendantskaya, Ekaterina: ML4PG in computer algebra verification (2013)