Abstract :
A classical mathematical proof is constructed using pencil and paper. However,
there are many ways in which computers may be used in a mathematical
proof. But ‘proof by computer’, or even the use of computers in the course of
a proof, is not so readily accepted (the December 2008 issue of the Notices of
the American Mathematical Society is devoted to formal proofs by computer).
In the following we introduce verification methods and discuss how they
can assist in achieving a mathematically rigorous result. In particular we
emphasize how floating-point arithmetic is used.
The goal of verification methods is ambitious. For a given problem it is
proved, with the aid of a computer, that there exists a (unique) solution of
a problem within computed bounds. The methods are constructive, and the
results are rigorous in every respect. Verification methods apply to data with
tolerances as well, in which case the assertions are true for all data within the
tolerances.
Non-trivial problems have been solved using verification methods. For example,
Tucker (1999) received the 2004 EMS prize awarded by the European
Mathematical Society for giving ‘a rigorous proof that the Lorenz attractor
exists for the parameter values provided by Lorenz. This was a long-standing
challenge to the dynamical system community, and was included by Smale in
his list of problems for the new millennium. The proof uses computer estimates
with rigorous bounds based on higher dimensional interval arithmetics.’
Also, Sahinidis and Tawaralani (2005) received the 2006 Beale–Orchard–Hays
Prize for their package BARON, which ‘incorporates techniques from automatic
differentiation, interval arithmetic, and other areas to yield an automatic,
modular, and relatively efficient solver for the very difficult area of
global optimization.’
This review article is devoted to verification methods and consists of three
parts of similar length. In Part 1 the working tools of verification methods
are discussed, in particular floating-point and interval arithmetic; my findings
in Section 1.5 (Historical remarks) seem new, even to experts in the field.
In Part 2, the development and limits of verification methods for finitedimensional
problems are discussed in some detail. In particular, we discuss
how verification is not working. For example, we give a probabilistic argument
that the so-called interval Gaussian elimination (IGA) does not work even for
(well-conditioned) random matrices of small size. Verification methods are
discussed for problems such as dense systems of linear equations, sparse linear
systems, systems of nonlinear equations, semi-definite programming and other
special linear and nonlinear problems, including M-matrices, finding simple
and multiple roots of polynomials, bounds for simple and multiple eigenvalues
or clusters, and quadrature. The necessary automatic differentiation tools to
compute the range of gradients, Hessians, Taylor coefficients, and slopes are
also introduced.
Concerning the important area of optimization, Neumaier (2004) gave in
his Acta Numerica article an overview on global optimization and constraint
satisfaction methods. In view of the thorough treatment there, showing the
essential role of interval methods in this area, we restrict our discussion to a
few recent, complementary issues.
Finally, in Part 3, verification methods for infinite-dimensional problems
are presented, namely two-point boundary value problems and semilinear
elliptic boundary value problems.
Throughout the article, many examples of the inappropriate use of interval
operations are given. In the past such examples contributed to the dubious
reputation of interval arithmetic (see Section 1.3), whereas they are, in fact,
simply a misuse.
One main goal of this review article is to introduce the principles of the
design of verification algorithms, and how these principles differ from those
for traditional numerical algorithms (see Section 1.4).
Many algorithms are presented in executable MATLAB/INTLAB code,
providing the opportunity to test the methods directly. INTLAB, the MATLAB
toolbox for reliable computing, was, for example, used by Bornemann,
Laurie, Wagon and Waldvogel (2004) in the solution of half of the problems
of the SIAM 10 × 10-digit challenge by Trefethen (2002).
