Machine learning for inductive theorem proving

Abstract

Over the past few years, machine learning has been successfully combined with automated theorem provers (ATPs) to prove conjectures from various proof assistants. However, such approaches do not usually focus on inductive proofs. In this work, we explore a combination of machine learning, a simple Boyer-Moore model and ATPs as a means of improving the automation of inductive proofs in HOL Light. We evaluate the framework using a number of inductive proof corpora. In each case, our approach achieves a higher success rate than running ATPs or the Boyer-Moore tool individually. An attempt to add the support for non-recursive type to the Boyer-Moore waterfall model is made by looking at proof automation for finite sets. We also test the framework in a program verification setting by looking at proofs about sorting algorithms in Hoare Logic.