ML4PG Introduction:

We present ML4PG, a machine-learning extension for Proof General. It allows 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 machine-learning environmnents 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.

Related Projects and Grants:

Related papers (ordered from newer to older):

Related talks (ordered from newer to older):

Requirements to install ML4PG:

Download

Installation

After downloading ML4PG, unzip the file and follow the instructions of the user manual.

Code used in different papers:

The code related to the paper Proof Pattern Search in Coq/SSReflect is available here. These files can be compiled using Coq v.8.4 and SSReflect v.1.4.

The code related to the paper Recycling Proof Patterns in Coq: Case Studies is available here, and organised by sections. These files can be compiled using Coq v.8.4 and SSReflect v.1.4.

The code related to the paper ML4PG in Computer Algebra Verification. is available here. These files can be compiled using Coq v.8.4 and SSReflect v.1.4.

Contact

Please address any queries about ML4PG to katya at computing.dundee.ac.uk