Chapter 10, Computer Assisted Proofs and Self-Validating Methods

Siegfried M. Rump

INTLAB

The new Version 9 of INTLAB, the Matlab toolbox for Reliable Compting, is now available for Matlab and Octave.

The main progress in Version 8 are two new toolboxes:

affari affine arithmetc toolbox, gradients using affine quantities, Hessians using affine quantities, Taylor models using affine quantities.
fl k-bit IEEE 754 floating point and interval arithmetic.

A number of changes, improvements and speed-ups have been implemented earlier.

It comprises of

interval arithmetic for real and complex data including vectors and matrices (very fast),
interval arithmetic for real and complex sparse matrices (very fast),
automatic differentiation (forward mode, vectorized computations, sparse storage),
- Gradients to solve systems of nonlinear equations,
- Hessians for global optimization,
automatic slopes (sequential approach, slow for many variables),
univariate and multivariate (interval) polynomials,
rigorous real interval standard functions (fast, very accurate, 3 ulps),
rigorous complex interval standard functions (fast, rigorous, but not necessarily sharp inclusions),
rigorous input/output,
accurate summation, dot product and matrix-vector residuals (interpreted, but fairly fast),
multiple precision interval arithmetic with error bounds (does the job, slow), and more.

The philosophy of INTLAB is that *everything* is written in Matlab code to assure best portability.

The version handles Hessians in pure floating point and with verified bounds. As an example consider a model problem where the function to be minimized is

   function y = f(x)
     N = length(x);
     I = 1:N-4;
     y = sum( (-4*x(I)+3.0).^2 ) + sum( ( x(I).^2 + 2*x(I+1).^2 + ...
       3*x(I+2).^2 + 4*x(I+3).^2 + 5*x(N).^2 ).^2 );

with initial approximation xs=ones(N,1) for N=1000. This means 1e6 elements in the gradient and 1e9 elements in the Hessian, or 8 GByte in full storage. In our implementation Hessians are stored sparse using a special storage scheme allowing efficient computations.

The following is executable code to calculate an inclusion of a stationary point of f by first performing a simple Newton iteration followed by a verification step for the resulting nonlinear system. Error estimations are completely rigorous.

 >> n = 1000;
    xs = ones(n,1);
    tic
    X = verifynlss(@f,xs,'hSparseSPD');
    t = toc
    maxrelerr = max(relerr(X))


    t = 23.8040
    maxrelerr = 5.5992e-013

Inclusions of all components of a stationary point are to some 13 decimal digits and takes 24 seconds on my 800 MHz Pentium III Laptop. Symmetric positive definiteness of the Hessian can be verified as well, ensuring a (local) minimum of f in X.

Some higher transcendental functions like erf, erfc and gamma have been added. For arguments close to negative integers the result of the built-in Matlab function has sometimes no correct digit, whereas INTLAB verifies bounds of almost maximum accuracy.

INTLAB works under Windows, Unix and Mac OS and is tested under Matlab Versions 5.3 to 7.0 . INTLAB is freely available for non-commercial use from

    http://www.ti3.tuhh.de/intlab/

For Octave the INTLAB package is self-contained including Octave Version 3.8.2.

For demonstration, also Matlab-implementations of our new summation and dot product routines are given, S. M. Rump, T. Ogita, and S. Oishi Accurate Floating-Point Summation, SIAM J. Sci. Comput. Vol. 31, Issue 2, pp. 1269-1302 (2008).

Comments always welcome. Best wishes

Siegfried M. Rump, Email rump@tuhh.de

Dates: May 15, 2014 and February 9, 2015

Prof. Dr. Siegfried M. Rump
Inst. f. Computer Science III
Technical University Hamburg-Harburg
Schwarzenbergstr. 95
21071 Hamburg
Germany