NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner


mcmillan image Kenneth McMillan and Aws Albarghouthi
Microsoft Research
The Importance of Generalization in Automated Proof

Generalization from cases is a widely used strategy in automated deduction. That is, in proving a theorem, we consider a variety of special cases. From the proof of a special case, we derive a fact that covers this case, and hopefully a large space of additional cases. The canonical example of this approach is conflict learning in a Boolean satisfi ability (SAT) solver. In such a solver, we select a special case by deciding the values of certain Boolean variables. If we obtain a refutation of this case using a simple proof system called unit resolution, then we derive a new fact from this proof (a conflict clause) that rules out our particular set of decisions. This generalization can be viewed as a logical interpolant derived from the proof. Many other types of provers, including SAT module theories (SMT) solvers and model checkers for hardware and software, use similar strategies to focus deduction on relevant facts.

The difficulty with generalization is that there are so many possible generalizations we can make of any given case. Di fferent proofs and proof systems will produce diff erent generalizations, and many can typically be derived from the same proof. A relevant generalization may result in rapid convergence of the overall proof, while an irrelevant one may lead to explosion of the proof search, or even divergence (for example, in the case of inductive proofs). Some weak heuristics have emerged to aid in this decision. For example, in a SAT solver, one seeks a generalization that is locally useful in guiding the model search (the selection of the next case). In other problems (such as SMT), we prefer stronger to weaker deductions. In inductive proofs (for example in model checkers) we may prefer simpler generalizations as more likely to avoid a divergence of inductive hypotheses.

These tactics suffer from a common weakness, however. They try to generalize from a single case, a highly under-constrained problem. A less myopic approach would be to revise one's generalizations in consideration of additional cases, as one would do in empirical reasoning. As additional cases are encountered, we might search for the simplest deduction that covers all or a large subset of the cases. A requirement of simplicity can force us to discover the underlying trend or pattern in the cases (that is, to avoid "over- fitting" the data).

Does the benefi t of reconsidering past generalizations outweigh the cost? We will consider a simple approach that can infer common generalizations of multiple cases in linear arithmetic. This provides a means of inferring inductive invariants of numeric programs that is more robust than existing techniques. Moreover, there are problems on which modern SMT solvers suffer from an explosion of cases due to a failure to generalize e ffectively. On such problems, a structured approach that clusters similar cases can produce exponential speed-up.

The idea of generalizing from the proof of a single case may seem an extreme point of view, yet most modern approaches to decision problems and model checking problem rely on it in some way. Stepping back from this position, we might ask what can be done to help our reasoning tools see the bigger picture, what heuristics are needed, and what the costs and bene fits might be.

First Gov logo
NASA Logo - nasa.gov