MaLeCoP
MaLeCoP Machine Learning Connection Prover. Probabilistic guidance based on learned knowledge is added to the connection tableau calculus and implemented on top of the lean-CoP theorem prover, linking it to an external advisor system. In the typical mathematical setting of solving many problems in a large complex theory, learning from successful solutions is then used for guiding theorem proving attempts in the spirit of the MaLARea system. While in MaLA Rea learning-based axiom selection is done outside unmodified theorem provers, in MaLeCoP the learning-based selection is done inside the prover, and the interaction between learning of knowledge and its application can be much finer. This brings interesting possibilities for further construction and training of self-learning AI mathematical experts on large mathematical libraries, some of which are discussed. The initial implementation is evaluated on the MPTP Challenge large theory benchmark
Keywords for this software
References in zbMATH (referenced in 15 articles , 1 standard article )
Showing results 1 to 15 of 15.
Sorted by year (- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
- Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
- Färber, Michael; Brown, Chad: Internal guidance for Satallax (2016)
- Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol; Urban, Josef: Mizar: state-of-the-art and beyond (2015)
- Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
- Kaliszyk, Cezary; Urban, Josef: FEMaLeCoP: fairly efficient machine learning connection prover (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
- Kaliszyk, Cezary; Urban, Josef: Automated reasoning service for HOL light (2013)
- Kaliszyk, Cezary; Urban, Josef: Lemma mining over HOL light (2013)
- Urban, Josef; Vyskočil, Jiří: Theorem proving in large formal mathematics as an emerging AI field (2013)
- Alama, Jesse; Kühlwein, Daniel; Urban, Josef: Automated and human proofs in general mathematics: an initial comparison (2012)
- Kühlwein, Daniel; van Laarhoven, Twan; Tsivtsivadze, Evgeni; Urban, Josef; Heskes, Tom: Overview and evaluation of premise selection techniques for large theory mathematics (2012)
- Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr: MaLeCoP. Machine learning connection prover (2011)