Fast Reliable Approximation – Fast Relax

Numerical computation is performed more and more efficiently, thanks to the progress of high performance computing and better and better numerical libraries. However, in most cases, the validity or quality of the approximations that are returned is difficult if not impossible to assess. Yet, in critical applications as encountered for instance in aerospace problems, such information is vital.
Partial answers are provided by arbitrary precision libraries as found in computer algebra systems, by interval arithmetic, or by formal proofs, but fast and reliable approximation is still a long-term research challenge.

In this project, we bring together specialists of computer arithmetic, formal proof systems, computer algebra, rigorous computing and optimal control theory. Our aim is to develop computer-aided proofs of numerical values, with certified and reasonably tight error bounds, without sacrificing efficiency. Applications to zero-finding, numerical quadrature or global optimization can all benefit from using our results as building blocks. We expect our work to initiate a ``fast and reliable'' trend in the symbolic-numeric community. This will be achieved by developing interactions between our fields, designing and implementing prototype libraries and applying our results to concrete problems originating in optimal control theory.

Our overall approach consists in using computer algebra in a preprocessing stage for automating the computation of approximations and for controlling symbolically all numerical errors. The approximation and error bound obtained at this stage will be designed to be efficient to store, manipulate and evaluate at subsequent numerical levels. There, roundoff errors are handled by multiple (yet moderate) precision and interval arithmetic. Formal proofs are used to check certificates produced along with the symbolic part and to prove key low-level numerical routines. This approach is vindicated on target applications from optimal control theory.