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 20 articles , 1 standard article )
Showing results 1 to 20 of 20.
Sorted by year (- Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
- Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
- Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef: ProofWatch: watchlist guidance for large theories in E (2018)
- Piotrowski, Bartosz; Urban, Josef: ATPboost: learning premise selection in binary setting with ATP feedback (2018)
- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
- Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef: TacticToe: learning to reason with HOL4 tactics (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: HOL(y)Hammer: online ATP service for HOL Light (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: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
- Kaliszyk, Cezary; Urban, Josef: Lemma mining over HOL Light (2013)
- Kaliszyk, Cezary; Urban, Josef: Automated reasoning service for 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)