Can statistical machine learning advance mechanised proof technology?

Katya Komendantskaya ( University of Dundee )

Over the last few decades, theorem proving has seen major developments. Automated (first-order) theorem provers (e.g. E, Vampire, SPASS) and SAT/SMT solvers (e.g. CVC3, Yices, Z3) are becoming increasingly fast and efficient. Interactive (higher-order) theorem provers (e.g. Coq, Isabelle/HOL, AGDA) have been enriched with dependent types, (co)inductive types, type classes and provide rich programming environments. Communities working on development, implementation and applications of ATPs and ITPs have accumulated big corpora of electronic proof libraries. However, the size of the libraries, as well as their technical and notational sophistication often stand on the way of efficient knowledge re-use. Very often, it is easier to start a new library from scratch rather than search the existing proof libraries for potentially common heuristics and techniques. The main question I address in this talk is: Can statistical pattern recognition help in creation of more convenient and user-friendly proof environments, in which statistically significant proof patterns could be used as proof-hints? I will survey the most successful state-of-the art machine-learning tools for theorem proving, and will present the new tool ML4PG (“Machine-Learning for Proof General”) – an Emacs-based interface that allows Coq/SSReflect users to find interesting proof patterns interactively during the proof-development. I will show how ML4PG works for mathematical and industrial libraries. ML4PG tool is the main outcome of the EPSRC First Grant “Machine-Learning Automated Proofs”. The webpage of ML4PG with downloadable software and papers can be found here: http://www.computing.dundee.ac.uk/staff/katya/ML4PG/