Online machine learning techniques for Coq: a comparison

DOI10.1007/978-3-030-81097-9_5MaRDI QIDQ2128797zbMATH OpenOpenAlexFDO

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

Publication date 22 April 2022

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

zbMATH Keywords

machine learningrandom forestonline learningCoqinteractive theorem provinggradient 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)

Abstract: We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs. Learning happens in an online manner, meaning that Tactician's machine learning model is updated immediately every time the user performs a step in an interactive proof. This has important advantages compared to the more studied offline learning systems: (1) it provides the user with a seamless, interactive experience with Tactician and, (2) it takes advantage of locality of proof similarity, which means that proofs similar to the current proof are likely to be found close by. We implement two online methods, namely approximate k-nearest neighbors based on locality sensitive hashing forests and random decision forests. Additionally, we conduct experiments with gradient boosted trees in an offline setting using XGBoost. We compare the relative performance of Tactician using these three learning methods on Coq's standard library.

Recommendations

• The Tactician. A seamless, interactive tactic learner and prover for Coq
• TacticToe: learning to reason with HOL4 tactics
• scientific article; zbMATH DE number 6528605
• MaSh: machine learning for Sledgehammer
• Machine learning for first-order theorem proving

Cites work

• A proof strategy language and proof script generation for Isabelle/HOL
• ATPboost: learning premise selection in binary setting with ATP feedback
• Approximate nearest neighbor: towards removing the curse of dimensionality
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Making data structures persistent
• Multidimensional binary search trees used for associative searching
• Random forests
• Random forests for premise selection
• TacticToe: learning to prove with tactics
• TacticToe: learning to reason with HOL4 tactics
• The Tactician. A seamless, interactive tactic learner and prover for Coq

Cited in

(4)

• Learning Proof Transformations and Its Applications in Interactive Theorem Proving
• scientific article; zbMATH DE number 6528605 (Why is no real title available?)
• Machine-learned premise selection for Lean
• The Tactician. A seamless, interactive tactic learner and prover for Coq

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2128797)