Search papers, labs, and topics across Lattice.
This paper introduces a new approach to probabilistic floating-point round-off analysis using concentration inequalities applied to Taylor expansions, addressing the limitations of overly conservative deterministic thresholds. The key innovation lies in a sound over-approximation technique that removes absolute value operators from Taylor expansions, enabling efficient calculation of expected values. Experiments demonstrate that the proposed method achieves comparable precision to state-of-the-art techniques with orders of magnitude improvement in time efficiency.
Ditch the overly conservative error bounds: a new probabilistic approach to floating-point analysis delivers speed and precision by cleverly taming Taylor expansions.
Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one must derive guaranteed round-off thresholds to ensure the correctness of these programs. However, deterministic round-off thresholds tend to be too conservative to be usable in practice, since they often involve large round-off errors that occur with small probability. Probabilistic thresholds relax deterministic ones by specifying that the probability of the round-off error exceeding a threshold is below a given confidence. In this work, we propose a novel approach to probabilistic round-off analysis, by applying concentration inequalities over the Taylor expansion from FPTaylor (TOPLAS 2018). A major obstacle in applying concentration inequalities is that the Taylor expansion involves absolute value operators that make the calculation of the expected values of the first order partial differential terms difficult. Our first step to overcome this obstacle is a sound over-approximation that removes the absolute value operators in polynomial expressions. Then, we show how to handle fractional expressions by a transformation into polynomial case. Finally, we show how to improve our approach with range partitioning. Our approach is scalable since the key computational part is the calculation of expected values of polynomial expressions with independent variables, for which the linear and independence properties of expectation boost the computation. Experimental results show that our approach is orders of magnitude more time efficient, while producing thresholds with comparable precision against the state of the art.
