University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Machine Learning for Interactive Theorem Proving: Revisit, Reuse and Recycle your Proofs

Machine Learning for Interactive Theorem Proving: Revisit, Reuse and Recycle your Proofs

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact info@newton.ac.uk.

BPRW01 - Computer-aided mathematical proof

Interactive theorem proving has seen major development in the past decade,  and is being  widely adopted in formalisation of mathematics and in verification. Further growth and dissemination of interactive theorem proving  require more intelligent tools that can make this technology more user friendly and convenient. As full automation of interactive provers is impossible, it is important to  develop better heuristics that enable
to data mine the existing libraries and  reuse existing proof strategies when writing new proofs.

In this talk, I will talk about several projects devoted to Machine Learning for Interactive Theorem Proving (in Coq and ACL2 )  that I participated in in the last 5 years.
I will give a light survey of a variety of machine learning methods that have already been employed in these provers, and will discuss, with some help from the audience, which of those methods bear more promise for the future. 

In the technical part, I will also talk about ML4PG —  the machine learning extension to Proof general, that I have developed in collaboration with  my colleagues, its recent extension Coq-PR3 and the plans to re-incarnate these tools in the upcoming new version of Proof General currently developed by INRIA and at MIT .    

Based on the joint work with G.Grov,  T.Gransden,  J.Heras, M.Johansson, E.McLean, N.Walkinshaw.

This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity