MaSh: Machine Learning for Sledgehammer
| Autor: | Kühlwein, D., Blanchette, J., Kaliszyk, C., Urban, J., Blazy, S., Paulin-Mohring, C., Pichardie, D. |
|---|---|
| Přispěvatelé: | Blazy, S., Paulin-Mohring, C., Pichardie, D. |
| Rok vydání: | 2013 |
| Předmět: |
Computer science
Programming language business.industry Data Science Proof assistant HOL Context (language use) Mizar system Mathematical proof Machine learning computer.software_genre TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Filter (video) Server Lecture Notes in Computer Science Relevance (information retrieval) Artificial intelligence business computer |
| Zdroj: | Interactive Theorem Proving ISBN: 9783642396335 ITP Lecture Notes in Computer Science ; 7998, 35-50. Berlin : Springer STARTPAGE=35;ENDPAGE=50;TITLE=Lecture Notes in Computer Science ; 7998 Blazy, S.; Paulin-Mohring, C.; Pichardie, D. (ed.), Interactive Theorem Proving, pp. 35-50 |
| DOI: | 10.1007/978-3-642-39634-2_6 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|