Learning proof heuristics by adapting parameters

Matthias Fuchs
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, 67653 Kaiserslautern
Germany
E-mail: fuchs@informatik.uni-kl.de

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.

Keywords
automated reasoning, machine learning, theorem proving

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1995/
file: Fuchs.SR-95-02.ps.gz