Numerical Analysis — Special Topics

Verified Computation and Interval Arithmetic

Overview of the Special Topics

In the special topics we treat verified numerical computation and interval arithmetic, which guarantee error bounds on the computed result, together with random number generation, which is indispensable for numerical simulation.

Interval arithmetic rigorously encloses the true value by representing the result as an interval, while verified computation automatically derives mathematically correct error bounds. Together, these techniques fundamentally improve the reliability of scientific computation.

Learning Goals

  • Understand the definition of interval arithmetic and the dependency problem.
  • Learn the theory and applications of verified numerical computation.
  • Understand the principles and quality assessment of pseudo-random number generators.

Contents

  1. Chapter 1 Interval Arithmetic

    Definition of interval arithmetic, the dependency problem, affine arithmetic and Taylor models, interval Newton method, interval extensions of elementary functions, interval matrix operations, and constraint propagation.

  2. Chapter 2 Verified Numerical Computation

    Automatic derivation of error bounds, computer-assisted proof, accuracy guarantees, MPLAPACK, reproducible computation, formal verification (Coq/Flocq/Gappa), and applications in physics and engineering (celestial mechanics, lattice QCD, CFD).

  3. Chapter 3 Random Number Generation

    Pseudo-random number generators (LCG, MT19937, Xorshift, PCG), period and quality assessment, statistical tests, and non-uniform random number generation.

Visualizing Interval Arithmetic

Represent the result of a computation as an interval rather than a point, and manage error rigorously.

2.5 3.0 3.5 Interval arithmetic: [3.14, 3.15] True value π Example of interval arithmetic: [1, 2] + [3, 4] = [4, 6] ← the true result is guaranteed to lie in this interval Verified computation: mathematically guarantees that the computed result contains the true value.

Figure 1: The concept of interval arithmetic. The blue band is the interval of the computed result, and the red dot represents the true value.

Prerequisites

  • Knowledge of floating-point numbers from Numerical Analysis — Basic.
  • Basics of algorithms and computational complexity.
  • Programming experience in C or Python (recommended but not required).

Arb / FLINT

A library specialized for interval arithmetic and verified computation. Provides fast error tracking via ball arithmetic.

INTLAB

An interval arithmetic toolbox on top of MATLAB/Octave. The de facto standard tool for verified numerical computation.

kv library

A C++ library for verified numerical computation. Supports proofs of the existence of solutions to differential equations.

References