Rigorous roundoff error analysis of probabilistic floating-point computations
File(s)
Published version
Author(s)
Constantinides, George
Dahlqvist, Fredrik
Rakamaric, Zvonimir
Salvia, Rocco
Type
Conference Paper
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.
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.
Date Issued
2021-07-15
Date Acceptance
2021-04-17
Citation
2021, pp.626-650
Publisher
Springer
Start Page
626
End Page
650
Copyright Statement
© 2021 The Author(s). This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the
chapter’s Creative Commons license, unless indicated otherwise in a credit line to the
material. If material is not included in the chapter’s Creative Commons license and
your intended use is not permitted by statutory regulation or exceeds the permitted
use, you will need to obtain permission directly from the copyright holder.
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the
chapter’s Creative Commons license, unless indicated otherwise in a credit line to the
material. If material is not included in the chapter’s Creative Commons license and
your intended use is not permitted by statutory regulation or exceeds the permitted
use, you will need to obtain permission directly from the copyright holder.
License URL
Identifier
http://arxiv.org/abs/2105.13217v1
Source
Computer-Aided Verification
Subjects
cs.LO
cs.LO
cs.NA
math.NA
Notes
Long version of the eponymous CAV 2021 paper
Publication Status
Published
Start Date
2021-07-20
Finish Date
2021-07-23
Coverage Spatial
33rd International Conference, CAV 2021
Date Publish Online
2021-07-15