Towards Evolutionary Theorem Proving for Isabelle/HOL
This work addresses the problem of automating theorem proving for engineers and mathematicians, but it appears incremental as it builds on existing methods with a new computational technique.
The paper tackles the challenge of discovering effective heuristics for automatic proof search in Isabelle/HOL, which is labor-intensive and limited by existing proof corpora, by proposing a novel approach using evolutionary computation to improve these heuristics.
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.