Template-Based Conjecturing for Automated Induction in Isabelle/HOL

TL;DR

This paper introduces a template-based conjecturing method to automate the generation of auxiliary lemmas for inductive proofs in Isabelle/HOL, significantly improving success rates in proof automation.

Contribution

It presents a novel approach called template-based conjecturing that automates auxiliary lemma generation for inductive proofs in Isabelle/HOL.

Findings

40 percentage point improvement in success rates

Effective automation of auxiliary lemma generation

Enhanced proof automation for intermediate difficulty problems

Abstract

Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human engineers often have to provide auxiliary lemmas manually. We automate this laborious process with template-based conjecturing, a novel approach to generate auxiliary lemmas and use them to prove final goals. Our evaluation shows that our working prototype, TBC, achieved 40 percentage point improvement of success rates for problems at intermediate difficulty level.