Learning proof heuristics by adapting parameters

Abstract

We present a method for learning heuristics employed by an automated prover to control its inference machine. The hub of the method is the adaptation of the parameters of a heuristic. Adaptation is accomplished by a genetic algorithm. The necessary guidance during the learning process is provided by a proof problem and a proof of it found in the past. The objective of learning consists in finding a parameter configuration that avoids redundant effort w.r.t. this problem and the particular proof of it. A heuristic learned (adapted) this way can then be applied profitably when searching for a proof of a similar problem. So, our method can be used to train a proof heuristic for a class of similar problems. A number of experiments (with an automated prover for purely equational logic) show that adapted heuristics are not only able to speed up enormously the search for the proof learned during adaptation. They also reduce redundancies in the search for proofs of similar theorems. This not only results in finding proofs faster, but also enables the prover to prove theorems it could not handle before.