Skip to main content

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/

Speaker bio

Katya Komendantskaya (BSc, MSc Moscow State University (2003), PhD University College Cork (2007)) is a Senior Lecturer at the School of Computing, University of Dundee. Her first postdoctoral project on induction/coinduction in Coq was conducted in INRIA Sophia Antipolis, France. After that, she held EPSRC Postdoctoral Fellowship in Theoretical Computer Science (2008-2011) and EPSRC First Grant (2012-2014) on the topics of interdisciplinary methods arising when merging symbolic and statistical methods in automated and interactive theorem proving.

Share this: