Can statistical machine learning advance mechanised proof technology?
Katya Komendantskaya ( University of Dundee )
- 11:30 19th June 2013 ( week 9, Trinity Term 2013 )051
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/