Automatic Verification of Floating-Point Accumulation Networks

TL;DR

This work tackles the challenging verification of floating-point accumulation networks (FPANs), which arise in compensated summation and multi-term expansions. It introduces SELTZO, a six-parameter abstraction that captures sign, exponent, and mantissa bit-pattern structure to enable linear-inequality reasoning about FPANs, reducing P(F) to a SMT-friendly S_{P,F} in Presburger arithmetic. The authors demonstrate automatic, computer-verified proofs for tight error bounds on FPANs, including a new double-double addition algorithm madd that is faster and more accurate than the previous ddadd, with relative error bounded by about 2u^2. The approach yields orders-of-magnitude speedups over floating-point theories and scales across formats, enabling automated discovery and certification of new FPANs. Collectively, the work advances reliable high-precision floating-point algorithms by combining a novel abstraction, automatic verification, and improved addition techniques with practical impact for numerical libraries and scientific computing.

Abstract

Floating-point accumulation networks (FPANs) are key building blocks used in many floating-point algorithms, including compensated summation and double-double arithmetic. FPANs are notoriously difficult to analyze, and algorithms using FPANs are often published without rigorous correctness proofs. In fact, on at least one occasion, a published error bound for a widely used FPAN was later found to be incorrect. In this paper, we present an automatic procedure that produces computer-verified proofs of several FPAN correctness properties, including error bounds that are tight to the nearest bit. Our approach is underpinned by a novel floating-point abstraction that models the sign, exponent, and number of leading and trailing zeros and ones in the mantissa of each number flowing through an FPAN. We also present a new FPAN for double-double addition that is faster and more accurate than the previous best known algorithm.

Figures (7)

• Figure 1: Network diagram of the ddadd algorithm due to Li et al. (left) and madd, our new double-double addition algorithm (right). This graphical FPAN notation will be explained in detail in Section \ref{['sec:FPANs']}.
• Figure 2: $\operatorname{\mathsf{TwoSum}}(x, y)$
• Figure 3: Decomposition of a high-precision constant $C$ into overlapping and nonoverlapping floating-point expansions with $p = 6$ mantissa bits per term. Light blue digits represent a shift stored in the exponent and are not part of the mantissa. Note that the final expansion rounds $x_0$ up instead of down. In this case, $x_1$ is negative, and the mantissa of $x_1$ contains the one's complement of the corresponding digits in $C$.
• Figure 4: Gate representations of the floating-point sum and $\operatorname{\mathsf{TwoSum}}$ operations. In our notation, $x \oplus y$ is treated as a special case of $\operatorname{\mathsf{TwoSum}}(x, y)$ with the error term discarded. Note that the inputs are unordered (i.e., $\operatorname{\mathsf{TwoSum}}(x, y) = \operatorname{\mathsf{TwoSum}}(y, x)$) but the order of the outputs is significant, with larger-magnitude outputs on top.
• Figure 5: $\mathrlap{\mathsf{add2}((x_0, x_1), (y_0, y_1))}$

Theorems & Definitions (17)

• definition 1
• definition 2
• definition 3
• definition 4
• proposition 1
• proof
• proposition 2
• proposition 3
• proof
• proposition 4