Automated roundoff error analysis of probabilistic floating-point computations
File(s) 3705898.pdf (18.91 MB)
Published version
Author(s)
Constantinides, George
Dahlqvist, Fredrik
Rakamarić, Zvonimir
Salvia, Rocco
Type
Journal Article
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 results, 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 on 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 on roundoff errors using symbolic affine arithmetic. We implement the algorithm in the PAF tool, and evaluate it on FPBench, a standard benchmark suite for the analysis of roundoff errors in small kernels. Our evaluation shows that PAF computes tighter bounds than the current state of the art on almost all benchmarks.
Date Issued
2025-08-26
Date Acceptance
2024-10-22
Citation
ACM Transactions on Probabilistic Machine Learning, 2025, 1 (3), pp.1-35
ISSN
2836-8924
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
35
Journal / Book Title
ACM Transactions on Probabilistic Machine Learning
Volume
1
Issue
3
Copyright Statement
Copyright © 2024 Copyright held by the owner/author(s).
Identifier
https://doi.org/10.1145/3705898
Publication Status
Published
Article Number
ARTN 13
Date Publish Online
2024-11-29
