Online machine learning techniques for Coq: a comparison

DOI10.1007/978-3-030-81097-9_5zbMath1485.68288arXiv2104.05207OpenAlexW3186870373MaRDI QIDQ2128797

Josef Urban, Cezary Kaliszyk, Prokop Černỳ, Bartosz Piotrowski, Lasse Blaauwbroek, Liao Zhang

Publication date: 22 April 2022

Full work available at URL: https://arxiv.org/abs/2104.05207

zbMATH Keywords

online learningmachine learningrandom forestinteractive theorem provingCoqgradient boosted trees

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Online algorithms; streaming algorithms (68W27) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Tactician
• XGBoost
• ATPboost
• TacticToe
• ENIGMA
• HOList

Cites Work

• Unnamed Item
• Making data structures persistent
• ATPboost: learning premise selection in binary setting with ATP feedback
• TacticToe: learning to prove with tactics
• The Tactician. A seamless, interactive tactic learner and prover for Coq
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• A proof strategy language and proof script generation for Isabelle/HOL
• Random Forests for Premise Selection
• Multidimensional binary search trees used for associative searching
• TacticToe: Learning to Reason with HOL4 Tactics
• Random forests

This page was built for publication: Online machine learning techniques for Coq: a comparison