Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one must derive guaranteed round-off thresholds to ensure the correctness of these programs. However, deterministic round-off thresholds tend to be too conservative to be usable in practice, since they often involve large round-off errors that occur with small probability. Probabilistic thresholds relax deterministic ones by specifying that the probability of the round-off error exceeding a threshold is below a given confidence. In this work, we propose a novel approach to probabilistic round-off analysis, by applying concentration inequalities over the Taylor expansion from FPTaylor (TOPLAS 2018). A major obstacle in applying concentration inequalities is that the Taylor expansion involves absolute value operators that make the calculation of the expected values of the first order partial differential terms difficult. Our first step to overcome this obstacle is a sound over-approximation that removes the absolute value operators in polynomial expressions. Then, we show how to handle fractional expressions by a transformation into polynomial case. Finally, we show how to improve our approach with range partitioning. Our approach is scalable since the key computational part is the calculation of expected values of polynomial expressions with independent variables, for which the linear and independence properties of expectation boost the computation. Experimental results show that our approach is orders of magnitude more time efficient, while producing thresholds with comparable precision against the state of the art.

翻译：浮点舍入误差在科学计算和优化等领域的高强度数值程序中普遍存在。由于浮点误差可能导致意外且灾难性的程序故障，必须推导出可靠的舍入阈值以确保这些程序的正确性。然而，确定性舍入阈值往往过于保守而难以实际应用，因为它们通常包含以小概率出现的大幅舍入误差。概率阈值通过指定舍入误差超过阈值的概率低于给定置信度，从而放宽了确定性阈值。在本工作中，我们提出了一种新颖的概率舍入分析方法，通过将FPTaylor（TOPLAS 2018）中的泰勒展开与浓度不等式相结合。应用浓度不等式的主要障碍在于泰勒展开包含绝对值运算符，这使得一阶偏微分项的期望值计算变得困难。我们克服这一障碍的第一步是采用合理的过度近似方法，消除多项式表达式中的绝对值运算符。随后，我们展示了如何通过变换将分数表达式转化为多项式情况处理。最后，我们展示了如何通过范围划分来改进该方法。由于关键计算部分涉及独立变量多项式表达式的期望值计算，而期望的线性性和独立性特性可加速计算，因此该方法具有良好的可扩展性。实验结果表明，与现有最优方法相比，我们的方法在时间效率上提升了数个数量级，同时生成的阈值精度相当。