MaSh

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 23 articles )

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

1 2 next

  1. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  2. England, Matthew; Florescu, Dorian: Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition (2019)
  3. Raggi, Daniel; Stockdill, Aaron; Jamnik, Mateja; Garcia Garcia, Grecia; Sutherland, Holly E. A.; Cheng, Peter C.-H.: Inspection and selection of representations (2019)
  4. Rawson, Michael; Reger, Giles: A neurally-guided, parallel theorem prover (2019)
  5. England, Matthew: Machine learning for mathematical software (2018)
  6. Komendantskaya, Ekaterina; Heras, Jónathan: Proof mining with dependent types (2017)
  7. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  8. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  9. Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
  10. Färber, Michael; Kaliszyk, Cezary: Random forests for premise selection (2015)
  11. Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
  12. Kaliszyk, Cezary; Urban, Josef: FEMaLeCoP: fairly efficient machine learning connection prover (2015)
  13. Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
  14. Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
  15. Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène: Formalizing physics: automation, presentation and foundation issues (2015)
  16. Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří: Lemmatization for stronger reasoning in large theories (2015)
  17. Schulz, Stephan; Sutcliffe, Geoff: Proof generation for saturating first-order theorem provers (2015)
  18. Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev: Mining state-based models from proof corpora (2014)
  19. Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen: Hipster: integrating theory exploration in a proof assistant (2014)
  20. Heras, Jónathan; Komendantskaya, Ekaterina: ML4PG in computer algebra verification (2013)

1 2 next