Towards Evolutionary Theorem Proving for Isabelle/HOL

TL;DR

This paper proposes an innovative approach using evolutionary computation to enhance heuristics for automatic proof search in Isabelle/HOL, addressing the challenge of multiple proof strategies and aiming to automate proof development more effectively.

Contribution

It introduces a novel evolutionary computation method to improve proof heuristics in Isabelle/HOL, overcoming limitations of existing supervised learning approaches.

Findings

Demonstrates improved proof search efficiency

Identifies multiple proof strategies for conjectures

Enhances automation in theorem proving

Abstract

Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers' expertise and remains labor intensive. Recently, researchers have extracted heuristics of interactive proof development from existing large proof corpora using supervised learning. However, such existing proof corpora present only one way of proving conjectures, while there are often multiple equivalently effective ways to prove one conjecture. In this abstract, we identify challenges in discovering heuristics for automatic proof search and propose our novel approach to improve heuristics of automatic proof search in Isabelle/HOL using evolutionary computation.