On Sound Relative Error Bounds for Floating-Point Arithmetic

TL;DR

This paper explores methods for computing tight, sound relative error bounds in floating-point arithmetic, demonstrating that direct computation often yields significantly more accurate estimates than indirect methods, especially near zero values.

Contribution

It introduces techniques for directly computing relative error bounds in static analysis, improving accuracy over traditional absolute error-based methods.

Findings

Direct relative error computation can be up to six orders of magnitude tighter.

Using interval subdivision has limited benefits for relative errors but helps near zero values.

The study provides a systematic evaluation of relative error bounds in static analysis tools.

Abstract

State-of-the-art static analysis tools for verifying finite-precision code compute worst-case absolute error bounds on numerical errors. These are, however, often not a good estimate of accuracy as they do not take into account the magnitude of the computed values. Relative errors, which compute errors relative to the value's magnitude, are thus preferable. While today's tools do report relative error bounds, these are merely computed via absolute errors and thus not necessarily tight or more informative. Furthermore, whenever the computed value is close to zero on part of the domain, the tools do not report any relative error estimate at all. Surprisingly, the quality of relative error bounds computed by today's tools has not been systematically studied or reported to date. In this paper, we investigate how state-of-the-art static techniques for computing sound absolute error bounds can be used, extended and combined for the computation of relative errors. Our experiments on a standard benchmark set show that computing relative errors directly, as opposed to via absolute errors, is often beneficial and can provide error estimates up to six orders of magnitude tighter, i.e. more accurate. We also show that interval subdivision, another commonly used technique to reduce over-approximations, has less benefit when computing relative errors directly, but it can help to alleviate the effects of the inherent issue of relative error estimates close to zero.