Reference. Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
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.
Cite
Cites 35 works (0 here)
External (35)
- Quantitative Bounds on Resource Usage of Probabilistic Programs (2024)
- Automated Tail Bound Analysis for Probabilistic Recurrence Relations (2023)
- Central moment analysis for cost accumulators in probabilistic programs (2021)
- Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations (2021)
- Quantitative analysis of assertion violations in probabilistic programs (2020)
- Sound Probabilistic Numerical Error Analysis (2019)
- Introduction to Probability (2019)
- Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments (2018)
- Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper) (2018)
- An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs (2018)
- Rigorous Estimation of Floating-Point Round-Off Errors with Symbolic Taylor Expansions (2018)
- Certified Roundoff Error Bounds Using Semidefinite Programming (2017)
- Stochastic invariants for probabilistic termination (2016)
- Toward a Standard Benchmark Format and Suite for Floating-Point Analysis (2016)
- Verifying bit-manipulations of floating-point (2016)
- Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities (2016)
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs (2015)
- Sound compilation of reals (2013)
- Probabilistic Program Analysis with Martingales (2013)
- A generalization of p-boxes to affine arithmetic (2012)
- RangeLab: A Static-Analyzer to Bound the Accuracy of Finite-Precision Computations (2011)
- Probability and Stochastics (2011)
- Towards Program Optimization through Automated Analysis of Numerical Precision (2010)
- Certification of bounds on expressions involving rounded operators (2010)
- Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software (2009)
- A Sound Floating-Point Polyhedra Abstract Domain (2008)
- Constructing Probability Boxes and Dempster-Shafer Structures (2003)
- IEEE standard 754 for binary floating-point arithmetic (1996)
- Affine Arithmetic and Its Applications to Computer Graphics (1993)
- What every computer scientist should know about floating-point arithmetic (1991)
- Probability with Martingales (1991)
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints (1977)
- Principles of mathematical analysis . Vol. 3 (1964)
- GELPIA: Global Extrema Locator Parallelization for Interval Arithmetic
- A Mechanized Error Analysis Framework for End-to-End Verification of Numerical Programs