一句话：提出符号泰勒展开方法并实现 FPTaylor，用严格全局优化更紧致地估计浮点最大舍入误差。
浮点最大舍入误差的严格估计对形式验证至关重要，但现有方法常给出过于悲观的过估计，导致验证失败。本文提出符号泰勒展开方法并实现 FPTaylor，其核心是用严格全局优化替代区间/仿射算术或 SMT 求解器，以获得更紧误差界；FPTaylor 还输出 HOL Light 机器可检查的逐实例证书。作者在相同机器上以最优配置评估 Gappa、Fluctuat、PRECiSA、Real2Float、Rosa 与 FPTaylor 在 24 个基准上的表现。结果表明 FPTaylor 在大量案例中给出显著更紧的舍入误差估计，并公开工具与基准。
Rigorous estimation of maximum floating-point round-off errors is an important capability central to many formal verification tools. Unfortunately, available techniques for this task often provide very pessimistic overestimates, causing unnecessary verification failure. We have developed a new approach called Symbolic Taylor Expansions that avoids these problems, and implemented a new tool called FPTaylor embodying this approach. Key to our approach is the use of rigorous global optimization, instead of the more familiar interval arithmetic, affine arithmetic, and/or SMT solvers. FPTaylor emits per-instance analysis certificates in the form of HOL Light proofs that can be machine checked. In this article, we present the basic ideas behind Symbolic Taylor Expansions in detail. We also survey as well as thoroughly evaluate six tool families, namely, Gappa (two tool options studied), Fluctuat, PRECiSA, Real2Float, Rosa, and FPTaylor (two tool options studied) on 24 examples, running on the same machine, and taking care to find the best options for running each of these tools. This study demonstrates that FPTaylor estimates round-off errors within much tighter bounds compared to other tools on a significant number of case studies. We also release FPTaylor along with our benchmarks, thus contributing to future studies and tool development in this area.
@article{paperbot310,
title = {Rigorous Estimation of Floating-Point Round-Off Errors with Symbolic Taylor Expansions},
author = {Alexey Solovyev and Marek S. Baranowski and Ian Briggs and Charles Jacobsen and Zvonimir Rakamarić and Ganesh Gopalakrishnan},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {41},
number = {1},
year = {2018},
doi = {10.1145/3230733}
}