2021/05/27 by George M. Constantinides, Fredrik Dahlqvist, Constantinides, George +5
Computer Science · Engineering · #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Low-power high-performance VLSI design #Numerical Analysis (math.NA) #Numerical Methods and Algorithms
paper · pdf · doi:10.48550/arxiv.2105.13217
openalex publication_date 2021/05/27 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
We present a detailed study of roundoff errors in probabilistic\nfloating-point computations. We derive closed-form expressions for the\ndistribution of roundoff errors associated with a random variable, and we prove\nthat roundoff errors are generally close to being uncorrelated with their\ngenerating distribution. Based on these theoretical advances, we propose a\nmodel of IEEE floating-point arithmetic for numerical expressions with\nprobabilistic inputs and an algorithm for evaluating this model. Our algorithm\nprovides rigorous bounds to the output and error distributions of arithmetic\nexpressions over random variables, evaluated in the presence of roundoff\nerrors. It keeps track of complex dependencies between random variables using\nan SMT solver, and is capable of providing sound but tight probabilistic bounds\nto roundoff errors using symbolic affine arithmetic. We implemented the\nalgorithm in the PAF tool, and evaluated it on FPBench, a standard benchmark\nsuite for the analysis of roundoff errors. Our evaluation shows that PAF\ncomputes tighter bounds than current state-of-the-art on almost all benchmarks.\n