FEMaLeCoP

FEMaLeCoP: fairly efficient machine learning connection prover. FEMaLeCoP is a connection tableau theorem prover based on leanCoP which uses efficient implementation of internal learning-based guidance for extension steps. Despite the fact that exhaustive use of such internal guidance can incur a significant slowdown of the raw inferencing process, FEMaLeCoP trained on related proofs can prove many problems that cannot be solved by leanCoP. In particular on the MPTP2078 benchmark, FEMaLeCoP adds 90 (15.7 %) more problems to the 574 problems that are provable by leanCoP. FEMaLeCoP is thus the first AI/ATP system convincingly demonstrating that guiding the internal inference algorithms of theorem provers by knowledge learned from previous proofs can significantly improve the performance of the provers. This paper describes the system, discusses the technology developed, and evaluates the system.


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

Showing results 1 to 14 of 14.
Sorted by year (citations)

  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. Rawson, Michael; Reger, Giles: A neurally-guided, parallel theorem prover (2019)
  6. Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef: ProofWatch: watchlist guidance for large theories in E (2018)
  7. Piotrowski, Bartosz; Urban, Josef: ATPboost: learning premise selection in binary setting with ATP feedback (2018)
  8. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
  9. Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
  10. Loos, Sarah; Irving, Geoffrey; Szegedy, Christian; Kaliszyk, Cezary: Deep network guided proof search (2017)
  11. Färber, Michael; Brown, Chad: Internal guidance for Satallax (2016)
  12. Otten, Jens: Nanocop: a non-clausal connection prover (2016)
  13. Davis, Martin (ed.); Fehnker, Ansgar (ed.); McIver, Annabelle (ed.); Voronkov, Andrei (ed.): Logic for programming, artificial intelligence, and reasoning. 20th international conference, LPAR-20 2015, Suva, Fiji, November 24--28, 2015. Proceedings (2015)
  14. Kaliszyk, Cezary; Urban, Josef: FEMaLeCoP: fairly efficient machine learning connection prover (2015)