Learning from Previous Proof Experience
Townsville, Australia
July 13th, 1997
Description of motivation and content
Over the years, automated deduction has reached an impressive level of
performance. This is partly due to very efficient inference engines,
and partly due to sophisticated search-guiding heuristics.
Nevertheless, automated theorem provers still cannot rival
mathematicians when it comes to tackling challenging problems. One
major reason for this deficiency of current automated deduction
systems is the fact that, unlike mathematicians, they do not make use
of past experiences. Instead, they start from scratch each time a
theorem has to be proved. For a mathematician, however, learning is a
continuous process that has a crucial influence on his or her
proficiency. It plays a vital, though often unconscious role in human
problem solving.
The potential of learning in automated theorem proving was
acknowledged very early. But progress in several areas of AI (and
automated deduction) was necessary to produce first convincing
solutions. This progress was partially enabled by three projects
funded by the DFG, namely Optimizing proof search by methods of
machine learning (TH Darmstadt), Learning of search
heuristics for theorem proving (U. Kaiserslautern) and
Learning of heuristics for automated deduction (TU
München). Learning Methods and deduction systems used in these
projects were quite different, and covered a wide spectrum. By
comparing these different approaches it is now possible to identify
central topics of research, open problems, and strength and weaknesses
of many solutions.
Learning from previous experience in automated deduction encompasses a
variety of problems. First there are problems concerning the learning
process itself:
- What or whom to learn from?
- What to learn?
- How to represent and store the learned knowledge?
Then there are problems concerning the usage of learned knowledge.
- How to detect applicable knowledge?
- How to apply knowledge?
- How to detect and deal with misleading knowledge?
- How to combine knowledge from different sources?
- Which concepts of similarity are helpful?
The answers to each of these questions can be arranged along multiple
axes. Provers can learn from successful proofs (generated by the proof
system itself, other provers, or possibly provided
by human users), from both contributing and superfluous
inferences in successful proof searches, or
even from proof searches that fail. The learning process can aim at
selecting a single source proof to guide the
search, or at utilizing common features
from multiple proof searches. Learning
procedures can use a set of simple features or
operate directly on recursive structures like terms and
clauses, and they can employ
numerical, connectionist or
symbolic learning algorithms. Knowledge can be
represented in the form of original source proofs and at
various levels of abstraction, from second order patterns
with or without proof context, to
precomputed evaluation functions.
The detection of applicable knowledge can be based on higher-order
matches or measures of similarity, or it can be left to the user.
Learning can be used for the classification or evaluation of clauses,
inferences or inference sequences, the
reproduction of decision sequences of proofs, or even to
reuse complete proofs. The distinction between knowledge
that advances the proof process and misleading knowledge can be based
on retrospective criteria that judge the impact a certain piece of
knowledge had so far, but also on similarity-based comparisons with
known proofs. Measures of similarity can
involve structural criteria, criteria that take the calculus of the
prover into account or use built-in theories, or use subsymbolic
encodings. The combination of learned knowledge can
be based on pre-defined hierarchical structures, but also on the
cooperation of provers using different ``chunks'' of
knowledge.
Possible combinations of these solutions and their application to
various aspects of a learning theorem prover result in a spectrum that
describes the learning capabilities of theorem provers.
These provers range from very specialized, but very efficient provers (for relatively
small problem classes), to very flexible, but
not quite as efficient provers (for larger problem classes).
Depending on the problems a user wants to solve, the appropriate region in this
spectrum has to be located and suitable instantiations of the
different aspects have to be selected. In other words, depending on
the problems that are to be solved, the most useful learning methods
for a prover must be identified.
In this introductory tutorial we will present the problems that must
be addressed in order to build learning theorem provers and the
various solutions to these problems that are inspired by research
in other areas of AI (e.g., machine learning,
case-based reasoning, or planning). We will characterize the region of
the described spectrum a particular solution is located in, and we
will provide a classification and some empirical studies for existing
learning theorem provers. We will also discuss the utility of certain
solutions for certain types of provers. That is, we will point out for
which types of calculi which problem solutions are well-suited and
which other solutions only cause much more problems.
The tutorial is intended for designers and implementers of automated
theorem provers who want to upgrade their provers by adding learning
capabilities. It is also intended for users of provers who want to
present their problems in a ``learnable'' way and therefore are
interested in the requirements on domains of interest that are
necessary for a successful use of learning provers. Naturally, the
tutorial is also of interest to people who explore connections of
automated deduction to other disciplines of AI and computer science.
Tutors
Jörg Denzinger
Computer Science Department,
University of Kaiserslautern
Postfach 3049, 67653 Kaiserslautern, Germany
FAX: +49-631-205-3558
Phone: +49-631-205-2181
Email:
denzinge@informatik.uni-kl.de
Matthias Fuchs
Computer Science Department,
University of Kaiserslautern
Postfach 3049, 67653 Kaiserslautern, Germany
FAX: +49-631-205-3558
Phone: +49-631-205-4299
Email:
fuchs@informatik.uni-kl.de
Christoph Goller
Research Group Automated Reasoning,
Technische Universität München
Arcisstr. 21, 80333 München, Germany
FAX: +49-89-526502
Phone: +49-89-521097
Email:
goller@informatik.tu-muenchen.de
Stephan Schulz
Research Group Automated Reasoning,
Technische Universität München
Arcisstr. 21, 80333 München, Germany
FAX: +49-89-526502
Phone: +49-89-521096
Email:
schulz@informatik.tu-muenchen.de
If you have questions, problems or suggestions send email to
denzinge@informatik.uni-kl.de