Typed meta-interpretive learning for proof strategies

Colin Farquhar, Gudmund Grov, Andrew Cropper, Stephen Muggleton, Alan Bundy

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Formal verification of computer programs is increasingly used in industry. A popular technique is interactive theorem proving, used for instance by Intel in HOL light. The ability to learn and re-apply proof strategies from a small set of proofs would significantly increase the productivity of these systems, and make them more cost-effective to use. Previous learning attempts have had limited success, which we believe is a result of missing key goal properties in the strategies. Capturing such properties requires predicate invention, and the only state-of-the-art ILP technique which supports this is meta-interpretive learning (MIL). We show that MIL is applicable to this problem, but that without type information it offers limited improvements in quality over previous work. We then extend MIL with types and give preliminary results indicating that this extension learns better-quality strategies with suitable goal properties. We also show that the quality of the learned strategies can be further enhanced through the use of dependent learning.
Original languageEnglish
Title of host publicationLate-breaking papers proceedings of ILP 2015 (LBP-ILP 2015)
PublisherCEUR Workshop Proceedings (CEUR-WS.org)
Number of pages16
Publication statusPublished - 13 Jul 2016
EventLate-breaking papers proceedings of ILP 2015 (LBP-ILP 2015) - Kyoto, Japan
Duration: 20 Aug 201522 Aug 2015


ConferenceLate-breaking papers proceedings of ILP 2015 (LBP-ILP 2015)
Abbreviated titleLBP-ILP 2015
Internet address


Dive into the research topics of 'Typed meta-interpretive learning for proof strategies'. Together they form a unique fingerprint.

Cite this