Rigorous roundoff error analysis of probabilistic floating-point computations
From MaRDI portal
Abstract: We present a detailed study of roundoff errors in probabilistic floating-point computations. We derive closed-form expressions for the distribution of roundoff errors associated with a random variable, and we prove that roundoff errors are generally close to being uncorrelated with their generating distribution. Based on these theoretical advances, we propose a model of IEEE floating-point arithmetic for numerical expressions with probabilistic inputs and an algorithm for evaluating this model. Our algorithm provides rigorous bounds to the output and error distributions of arithmetic expressions over random variables, evaluated in the presence of roundoff errors. It keeps track of complex dependencies between random variables using an SMT solver, and is capable of providing sound but tight probabilistic bounds to roundoff errors using symbolic affine arithmetic. We implemented the algorithm in the PAF tool, and evaluated it on FPBench, a standard benchmark suite for the analysis of roundoff errors. Our evaluation shows that PAF computes tighter bounds than current state-of-the-art on almost all benchmarks.
Recommendations
Cites work
- scientific article; zbMATH DE number 41029 (Why is no real title available?)
- scientific article; zbMATH DE number 3620755 (Why is no real title available?)
- scientific article; zbMATH DE number 1999206 (Why is no real title available?)
- scientific article; zbMATH DE number 1408651 (Why is no real title available?)
- scientific article; zbMATH DE number 3281219 (Why is no real title available?)
- A New Approach to Probabilistic Rounding Error Analysis
- A generalization of \(p\)-boxes to affine arithmetic
- A guide to Monte Carlo simulations in statistical physics.
- Accuracy and Stability of Numerical Algorithms
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- Certification of bounds on expressions involving rounded operators
- Certified roundoff error bounds using semidefinite programming
- Numerical inverting of matrices of high order
- Probabilistic Error Analysis for Inner Products
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- Rigorous floating-point mixed-precision tuning
- Semantics of probabilistic programs
- Sound compilation of reals
- Uncertainty propagation using probabilistic affine forms and concentration of measure inequalities
- dReal: an SMT solver for nonlinear theories over the reals
Cited in
(12)- Certified roundoff error bounds using semidefinite programming
- scientific article; zbMATH DE number 4143358 (Why is no real title available?)
- A priori worst case error bounds for floating-point computations
- scientific article; zbMATH DE number 440777 (Why is no real title available?)
- scientific article; zbMATH DE number 1617950 (Why is no real title available?)
- On roundoff error distributions in floating point and logarithmic arithmetic
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- Stochastic Rounding Variance and Probabilistic Bounds: A New Approach
- Probabilistic Error Analysis for Inner Products
- Precision-aware deterministic and probabilistic error bounds for floating point summation
- Probabilistic analysis of floating-point addition
- Probability Analysis of Round-Off Errors in Floating-Point Arithmetic
This page was built for publication: Rigorous roundoff error analysis of probabilistic floating-point computations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832297)
