E-MaLeS
E-MaLeS 1.1. Picking the right search strategy is important for the success of automatic theorem provers. E-MaLeS is a meta-system that uses machine learning and strategy scheduling to optimize the performance of the first-order theorem prover E. E-MaLeS applies a kernel-based learning method to predict the run-time of a strategy on a given problem and dynamically constructs a schedule of multiple promising strategies that are tried in sequence on the problem. This approach has significantly improved the performance of E 1.6, resulting in the second place of E-MaLeS 1.1 in the FOF divisions of CASC-J6 and CASC$@$Turing.
Keywords for this software
References in zbMATH (referenced in 12 articles )
Showing results 1 to 12 of 12.
Sorted by year (- Holden, Edvard K.; Korovin, Konstantin: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (2021)
- Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
- Rawson, Michael; Reger, Giles: A neurally-guided, parallel theorem prover (2019)
- Jakubův, Jan; Urban, Josef: Hierarchical invention of theorem proving strategies (2018)
- Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
- Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
- Jan Jakubuv, Josef Urban: BliStrTune: Hierarchical Invention of Theorem Proving Strategies (2016) arXiv
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kühlwein, Daniel; Urban, Josef: MaLeS: a framework for automatic tuning of automated theorem provers (2015)
- Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei: Cooperating proof attempts (2015)
- Bonacina, Maria Paola (ed.): Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings (2013)
- Kühlwein, Daniel; Schulz, Stephan; Urban, Josef: E-MaLeS 1.1 (2013)