Machine Learning in Proof General: Interfacing Interfaces

Abstract

We present ML4PG - a machine learning extension for Proof General. It allows users to gather proof statistics related to shapes of goals, sequences of applied tactics, and proof tree structures from the libraries of interactive higher-order proofs written in Coq and SSReflect. The gathered data is clustered using the state-of-the-art machine learning algorithms available in MATLAB and Weka. ML4PG provides automated interfacing between Proof General and MATLAB/Weka. The results of clustering are used by ML4PG to provide proof hints in the process of interactive proof development.

In Proceedings UITP 2012, arXiv:1307.1528

References in corpus (1)

• A formal proof of the four color theorem

Cited by in corpus (18)

• GamePad: A Learning Environment for Theorem Proving
• QED at Large: A Survey of Engineering of Formally Verified Software
• TacticToe: Learning to Prove with Tactics
• Passport: Improving Automated Formal Verification Using Identifiers
• Tactic Learning and Proving for the Coq Proof Assistant
• The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
• Learning to Reason with HOL4 tactics
• Predicting SMT Solver Performance for Software Verification
• Learning Guided Automated Reasoning: A Brief Survey
• A Study of Continuous Vector Representationsfor Theorem Proving
• Towards Automated Proof Strategy Generalisation
• On Learning to Prove
• ML + FV = $♡$? A Survey on the Application of Machine Learning to Formal Verification
• Deep Generation of Coq Lemma Names Using Elaborated Terms
• Recycling Proof Patterns in Coq: Case Studies
• First Experiments with Neural cvc5
• PaMpeR: Proof Method Recommendation System for Isabelle/HOL
• HoTT formalisation in Coq: Dependency Graphs \& ML4PG