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


References in zbMATH (referenced in 23 articles , 1 standard article )

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. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  3. Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
  4. Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
  5. Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef: ProofWatch: watchlist guidance for large theories in E (2018)
  6. Piotrowski, Bartosz; Urban, Josef: ATPboost: learning premise selection in binary setting with ATP feedback (2018)
  7. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
  8. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef: TacticToe: learning to reason with HOL4 tactics (2017)
  9. Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
  10. Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
  11. Färber, Michael; Brown, Chad: Internal guidance for Satallax (2016)
  12. 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)
  13. Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
  14. Kaliszyk, Cezary; Urban, Josef: FEMaLeCoP: fairly efficient machine learning connection prover (2015)
  15. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
  16. Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
  17. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
  18. Kaliszyk, Cezary; Urban, Josef: Automated reasoning service for HOL Light (2013)
  19. Kaliszyk, Cezary; Urban, Josef: Lemma mining over HOL Light (2013)
  20. Urban, Josef; Vyskočil, Jiří: Theorem proving in large formal mathematics as an emerging AI field (2013)

1 2 next