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.
翻译:我们对概率浮点计算中的圆差进行了详细研究。 我们从随机变量的圆差差差分布中得出封闭式表达式, 并且我们证明圆差通常与其生成的分布不相干。 基于这些理论进步, 我们提议了IEEE浮动点算法模型, 用概率输入来计算数字表达法, 并用一种算法来评价这个模型。 我们的算法为算术表达法相对于随机变量的输出和错误分布提供了严格的界限, 并在出现回合差错时进行评估。 它使用 SMT 解答器来跟踪随机变量之间的复杂依赖性, 并且能够使用象征性的近距算术为圆差提供合理但严格的概率界限。 我们在 PAFAF 工具中应用了算法, 并在FPBench (一个用于分析圆差错的标准基准套件 ) 进行了评估。 我们的评估显示, PAFAF在几乎所有基准上都比较比目前最先进的标准框更严格。