MaSh: Machine Learning for Sledgehammer. 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 enhancements. MaSh outperforms the old relevance filter on large formalizations, and a particularly strong filter is obtained by combining the two filters.

References in zbMATH (referenced in 16 articles )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Komendantskaya, Ekaterina; Heras, Jónathan: Proof mining with dependent types (2017)
  2. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  3. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  4. Färber, Michael; Kaliszyk, Cezary: Random forests for premise selection (2015)
  5. Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
  6. Kaliszyk, Cezary; Urban, Josef: FEMaLeCoP: fairly efficient machine learning connection prover (2015)
  7. Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
  8. Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
  9. Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène: Formalizing physics: automation, presentation and foundation issues (2015)
  10. Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří: Lemmatization for stronger reasoning in large theories (2015)
  11. Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev: Mining state-based models from proof corpora (2014)
  12. Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen: Hipster: integrating theory exploration in a proof assistant (2014)
  13. Heras, Jónathan; Komendantskaya, Ekaterina: ML4PG in computer algebra verification (2013)
  14. Kaliszyk, Cezary; Urban, Josef: Lemma mining over HOL light (2013)
  15. Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef: MaSh: machine learning for Sledgehammer (2013)
  16. Della Dora, Jean; Maignan, Aude; Mirica-Ruse, Mihaela; Yovine, Sergio: Hybrid computation (2001)