Formally verified roundoff error bounds on LogSumExp-based computations

We study the numerical accuracy of some specific computer programs performing numerical computations. Such a numerical accuracy is expressed in terms of a bound on the difference between the floating-point computations and the corresponding rounding-free computations using mathematical real numbers. We do not only seek to discover such bounds “on paper” but we aim at obtaining computer-assisted formal proofs that these bounds are correct for any possible inputs. The functions we study come from the domain of machine learning: a function computing the logarithm of the sum of exponentials of a sequence, and a similar function related to the computation of mutual information. The bounds obtained are original results, because they are parameterized by assumed error bounds of the underlying implementations of the logarithm and exponential functions. The methodology we follow to conduct our formal proofs is also original, using a combination of the Why3 environment for deductive verification, an original modeling of floating-point computations using unbounded numbers, and the J \(^3\) environment for proving properties on C source code.