Breeding Theorem Proving Heuristics with Genetic Algorithms

          Simon Schaefer & Stephan Schulz

First-order theorem provers have to search for proofs in an infinite
space of possible derivations. Proof search heuristics play a vital
role for the practical performance of these systems. In the current
generation of saturation-based theorem provers like SPASS, E, Vampire
or Prover~9, one of the most important decisions is the selection of
the next clause to process with the given clause algorithms. Provers
offer a wide variety of basic clause evaluation functions, which can
often be parameterized and combined in many different ways. Finding
good strategies is usually left to the users or developers, often
backed by large-scale experimental evaluations. We describe a way to
automatize this process using genetic algorithms, evaluating a
population of different strategies on a test set, and applying
mutation and crossover operators to good strategies to create the next
generation. We describe the design and experimental set-up, and report
on first promising results.