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:

• EPSRC First Grant scheme; project title Machine-Learning Coalgebraic Automated Proofs, 2012-2014.

• SICSA Industrial "Proof of Concept" grant Machine-Learning for Industrial Theorem Proving, 2013-2014. J.Heras and E.Komendantskaya.

Related papers (ordered from newer to older):

• J.Heras and E.Komendantskaya, A note on using ML4PG in HoTT (Homotopy Type Theory Library), and its relation to Dependency graphs.
• J.Heras and E.Komendantskaya, Recycling Proof Patterns in Coq: Case Studies. Mathematics in Computer Science 8(1): 99-116 (2014).
• J.Heras, E.Komendantskaya, M.Johansson, and E.Maclean. Proof-Pattern Recognition and Lemma Discovery in ACL2 LPAR'13. LNCS 8312, pp. 389-406, 2013.
• J.Heras, E.Komendantskaya ML4PG in Computer Algebra Verification. Systems & Projects session of CICM 2013. LNCS 7961, pp. 66-81, 2013. Arxiv version.
• E.Komendantskaya, J.Heras. The ARW'13 Workshop abstract Statistical Proof Pattern Recognition: Automated or Interactive? (slides), the 20th Automated Reasoning Workshop (ARW'13), 11-12 April 2013.
• E.Komendantskaya, J.Heras and G.Grov. Machine Learning for Proof General: interfacing interfaces. EPTCS Post-proceedings of User Interfaces for Theorem Provers (UITP 2012). Arxiv version.

Related talks (ordered from newer to older):

• J.Heras. Proof-Pattern Recognition and Lemma Discovery in ACL2, St Andrews, Scottish Theorem Proving Seminar. 31 January 2014.
• J.Heras and K.Komendantskaya. Statistical Machine Learning in Interactive Theorem Proving, Leicester, 8 November 2013.
• K.Komendantskaya. Can statistical machine learning advance mechanised proof technology? Oxford University, 19 June 2013.
• E.Komendantskaya, J.Heras. Machine Learning for Proof General: Interfacing Interfaces. November - December 2012, U. Edinburgh and Strathclyde.
• E.Komendantskaya, J.Heras. The ARW'13 talk Statistical Proof Pattern Recognition: Automated or Interactive? 11 April, Dundee.

Requirements to install ML4PG:

• Proof General.
• Coq.
• SSReflect (optional).
• Weka.
• Matlab + Statistics toolbox (optional).

Download

• New version of ML4PG: this version includes all the improvements presented in the paper Proof Pattern Search in Coq/SSReflect.
• ML4PG Weka version: this version only includes the connection with Weka.
• ML4PG full version: this version includes the connection with Weka and Matlab. You need a Matlab license to run this version of ML4PG.

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 Mining with dependent types. These files can be compiled using Coq v.8.4 and SSReflect v.1.4.

• Mathematical libraries:
• The formalisation about nilpotent matrices.
• The Persistent Homology library can be downloaded here.
• The rest of the files are distributed in the SSReflect library.
• The SSReflect library.

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.

• User scenario 1. ML4PG for Detecting patterns in early-stages of the development.
• The SSReflect library.
• Complete analysis of the SSReflect library using clustering
• User scenario 2. ML4PG for detecting irrelevant libraries.
• The formalisation from the paper "A Constructive Approach to Sequential Nash Equilibria" can be downloaded from the author (R. Vestergaard) webpage.
• The formalisation from the paper "Acyclicity and finite linear exendability: a formal and constructive equivalence" can be downloaded from the author (S. Le Roux) webpage.
• The formalisation from the paper "Acyclic preferences and existence of sequential Nash equilibria: a formal and constructive equivalence" can be downloaded from the author (S. Le Roux) webpage.
• User scenario 3. ML4PG for a team-based development
• The formalisation about JVM byte code.

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.

• The formalisation about the inverse of triangular matrices with 1s in the diagonal.
• The CoqEAL library can be downloaded here.
• The rest of the files are distributed in the SSReflect library.

Contact

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