2025-11-12T00:52:30.352910

OFP-Repair: Repairing Floating-point Errors via Original-Precision Arithmetic

Tan, Ding, Chen et al.
Errors in floating-point programs can lead to severe consequences, particularly in critical domains such as military, aerospace, and financial systems, making their repair a crucial research problem. In practice, some errors can be fixed using original-precision arithmetic, while others require high-precision computation. Developers often avoid addressing the latter due to excessive computational resources required. However, they sometimes struggle to distinguish between these two types of errors, and existing repair tools fail to assist in this differentiation. Most current repair tools rely on high-precision implementations, which are time-consuming to develop and demand specialized expertise. Although a few tools do not require high-precision programs, they can only fix a limited subset of errors or produce suboptimal results. To address these challenges, we propose a novel method, named OFP-Repair.On ACESO's dataset, our patches achieve improvements of three, seven, three, and eight orders of magnitude across four accuracy metrics. In real-world cases, our method successfully detects all five original-precision-repairable errors and fixes three, whereas ACESO only repairs one. Notably, these results are based on verified data and do not fully capture the potential of OFP-Repair. To further validate our method, we deploy it on a decade-old open bug report from GNU Scientific Library (GSL), successfully repairing five out of 15 bugs. The developers have expressed interest in our method and are considering integrating our tool into their development workflow. We are currently working on applying our patches to GSL. The results are highly encouraging, demonstrating the practical applicability of our technique.
academic

OFP-Repair: Repairing Floating-point Errors via Original-Precision Arithmetic

基本信息

  • 论文ID: 2510.09938
  • 标题: OFP-Repair: Repairing Floating-point Errors via Original-Precision Arithmetic
  • 作者: Youshuai Tan, Zishuo Ding, Jinfu Chen, Weiyi Shang
  • 分类: cs.SE (软件工程)
  • 发表时间/会议: Conference'17, Washington, DC, USA (2025)
  • 论文链接: https://arxiv.org/abs/2510.09938

摘要

浮点程序中的错误可能导致严重后果，特别是在军事、航空航天和金融系统等关键领域。实践中，一些错误可以通过原精度算术修复，而另一些则需要高精度计算。开发者通常避免使用高精度方法，因为其需要大量计算资源。然而，开发者往往难以区分这两类错误，现有修复工具也无法帮助进行此类区分。为解决这些挑战，本文提出了OFP-Repair方法，通过计算程序相对输入的条件数来识别原精度可修复错误，并使用级数展开构建统一的修复框架。实验结果显示，该方法在四个精度指标上分别实现了3、7、3、8个数量级的改进。

研究背景与动机

问题定义

浮点程序错误在关键系统中可能导致灾难性后果，如Patriot导弹系统故障、Ariane 5火箭爆炸等。现有研究表明，浮点错误主要分为两类：

  1. 原精度可修复错误：可通过重构数值表达式在原精度下修复
  2. 高精度依赖错误：必须使用高精度浮点算术才能修复

现有方法的局限性

论文识别了三个主要限制：

  1. 限制1：检测和修复过程都需要高精度程序，而将原程序转换为高精度版本需要深厚的数学和数值分析知识
  2. 限制2：缺乏针对原精度可修复错误的统一修复范式，现有工具只能处理部分此类错误
  3. 限制3：缺乏对此类错误的诊断能力，开发者无法判断错误是否可通过原精度算术修复

研究动机

Franco等人的研究显示，开发者更倾向于使用原精度修复方案，因为高精度方案计算成本高昂。例如，NumPy issue #1063因高精度成本过高而被关闭。然而，现有工具无法帮助开发者区分这两类错误类型。

核心贡献

  1. 提出OFP-Repair方法：首个能够有效检测和修复原精度可修复错误的统一框架
  2. 理论基础建立：基于条件数理论和Taylor级数展开的原精度错误检测与修复机制
  3. 广泛实验验证：在ACESO数据集、真实世界错误和十年未解决的GSL bug报告上验证方法有效性
  4. 实际应用价值：成功修复GSL中5个长期未解决的bug，获得开发者认可

方法详解

任务定义

  • 输入：包含浮点错误的程序和触发大误差的输入范围
  • 输出：
    1. 错误类型判断（原精度可修复 vs 高精度依赖）
    2. 原精度可修复错误的修复补丁
  • 约束：不依赖高精度程序实现

理论基础

大误差来源分析

论文证明了显著浮点错误主要源于抵消（cancellation）效应。当两个近似相等的浮点数相减时，会导致有效精度位数大幅减少。例如：

  • x = 3.14159265358973, y = 3.14159265358972
  • 理论差值：1×10^-14
  • 浮点计算结果：1.021405182655144×10^-14
  • 相对误差：约2.14%

程序多项式表示

基于以下两个定理：

  1. 算术运算保持连续性定理：连续函数的算术运算仍保持连续性
  2. Weierstrass逼近定理：连续函数可用多项式任意逼近

论文证明浮点程序可在每个分支域内转换为多项式表示。

检测算法（步骤1）

设计思路

使用条件数理论评估输入扰动对输出的影响： ∣f(x+Δx)−f(x)f(x)∣≈∣Δxx∣⋅∣xf′(x)f(x)∣\left|\frac{f(x+\Delta x)-f(x)}{f(x)}\right| \approx \left|\frac{\Delta x}{x}\right| \cdot \left|\frac{xf'(x)}{f(x)}\right|

其中 ∣xf′(x)f(x)∣\left|\frac{xf'(x)}{f(x)}\right| 为条件数。

检测流程

  1. 使用ATOMU检测显著浮点错误
  2. 对每个错误，计算程序相对输入的条件数
  3. 使用数值微分估算导数：f′(x)≈f(x+h)−f(x)hf'(x) \approx \frac{f(x+h)-f(x)}{h}
  4. 若条件数小于阈值（如10^5），则判定为原精度可修复错误

示例分析

对于函数 sin⁡(x+ϵ)−sin⁡(x)\sin(x+\epsilon) - \sin(x)：

  • 相对 sin⁡(x+ϵ)\sin(x+\epsilon) 的条件数：9.0132×10^9（很大）
  • 相对输入 xx 的条件数：3.40（很小）
  • 结论：该错误可通过原精度算术修复

修复算法（步骤2）

设计原理

使用Taylor级数展开将程序转换为无抵消的多项式形式： f(x)=∑n=0∞f(n)(a)n!(x−a)nf(x) = \sum_{n=0}^{\infty} \frac{f^{(n)}(a)}{n!}(x-a)^n

修复流程

  1. 选择展开点（通常为引起大误差的点附近）
  2. 计算Taylor级数的前若干项
  3. 构造避免原始抵消的多项式补丁
  4. 限制展开项数（论文中最多10项）

修复示例

对于 sin⁡(x+ϵ)−sin⁡(x)\sin(x+\epsilon) - \sin(x)：

  • Taylor展开：sin⁡(x+ϵ)=sin⁡(x)+cos⁡(x)ϵ−sin⁡(x)2!ϵ2+...\sin(x+\epsilon) = \sin(x) + \cos(x)\epsilon - \frac{\sin(x)}{2!}\epsilon^2 + ...
  • 消除 sin⁡(x)\sin(x) 项后：cos⁡(x)ϵ−sin⁡(x)2!ϵ2+...\cos(x)\epsilon - \frac{\sin(x)}{2!}\epsilon^2 + ...
  • 相对误差从 1.1095×10^-10 改善到 1.6176×10^-16

方法局限性

Taylor展开要求函数在展开点收敛。当函数在展开点发散时（如SciPy issue #3545中 norm.ppf(1−q/2)norm.ppf(1-q/2) 当 qq 趋近于0时），方法不适用。

实验设置

数据集

  1. ACESO数据集：32个基准函数
    • 15个来自先前浮点错误研究，已被证明可用原精度修复
    • 17个包含GSL和ALGLIB库调用的变体函数
  2. 真实世界错误：Franco等人收集的5个原精度可修复错误
  3. GSL bug报告：十年前的开放bug报告，包含15个浮点错误

评价指标

使用相对误差衡量浮点误差： ∣Resultapproximate−ResulttrueResulttrue∣\left|\frac{Result_{approximate} - Result_{true}}{Result_{true}}\right|

分别在稳定区域和衰减区域评估最大绝对误差和最大相对误差。

对比方法

主要与ACESO对比，因为它是唯一不需要高精度程序进行检测和修复的现有工具。

实现细节

  • 环境：Docker容器，Ubuntu 24.04，Intel i9-13900K CPU，128GB RAM
  • Taylor级数最多保留10项
  • 条件数阈值：1×10^5
  • 采样半径：1×10^-5

实验结果

主要结果

RQ1：检测能力评估

  • 成功率：在32个ACESO函数中，OFP-Repair成功识别所有原精度可修复错误
  • 条件数分析：计算得到的条件数最大值1.47，最小值0，平均值0.31，均远小于阈值10^5
  • 数值导数精度：除bj_tan函数外，相对误差范围0-0.746，不影响检测效果

RQ2：修复性能评估

与ACESO相比，OFP-Repair在四个指标上的平均改进：

指标OFP-RepairACESO改进倍数
稳定区域最大绝对误差4.11×10^-162.45×10^-133个数量级
稳定区域最大相对误差7.47×10^-162.74×10^-97个数量级
衰减区域最大绝对误差2.13×10^-162.45×10^-133个数量级
衰减区域最大相对误差3.73×10^-155.74×10^-78个数量级

RQ3：真实世界应用

  • 检测：成功识别所有5个真实世界原精度可修复错误
  • 修复：成功修复3个错误，而ACESO仅修复1个
  • 精度：修复后的函数精度显著优于ACESO

案例分析：GSL Bug报告

在十年未解决的GSL bug报告中：

完全解决案例（3个）

gsl_sf_hyperg_0F1函数：

  • 原始相对误差：1.15×10^198
  • 条件数：3.39×10^-210 和 1.01×10^-225（均很小）
  • 修复后相对误差：1.17×10^-27

部分改善案例（2个）

gsl_sf_gamma_inc_Q函数：

  • 相对误差从1.60×10^-6降至1.57×10^-7

gsl_sf_ellint_P函数：

  • 通过重构计算避免下溢，相对误差降至1.91×10^-9

相关工作

浮点错误检测

  • 静态分析工具：Valgrind框架上的FPDebug、Verrou、Herbgrind
  • 动态检测方法：遗传算法、条件数分析、符号执行等

浮点错误修复

  • 基于变换的方法：Herbie、Salsa等，依赖预定义模板，覆盖范围有限
  • 基于高精度的方法：AutoRNP等，需要完整的高精度程序实现
  • ACESO：唯一不依赖高精度程序的方法，但修复效果有限

结论与讨论

主要结论

  1. 有效检测：OFP-Repair能准确识别原精度可修复错误，无需高精度程序
  2. 优异修复：相比现有方法，在精度上实现数量级改进
  3. 实用价值：在真实项目中成功应用，获得开发者认可

局限性

  1. 收敛要求：Taylor展开要求函数在展开点收敛
  2. 分支处理：不同程序分支可能需要不同处理策略
  3. 复杂函数：对于极其复杂的数学函数，可能需要更多展开项

未来方向

  1. 扩展方法到更广泛的未解决错误
  2. 优化Taylor展开的项数选择策略
  3. 处理函数发散情况的替代方案

深度评价

优点

  1. 理论贡献：建立了基于条件数的原精度可修复错误检测理论
  2. 实用性强：不依赖高精度程序，降低了使用门槛
  3. 效果显著：在多个指标上实现数量级改进
  4. 验证充分：从学术基准到真实世界应用的全面验证
  5. 写作清晰：技术细节描述准确，实验设计合理

不足

  1. 适用范围：仅适用于原精度可修复错误，对高精度依赖错误无效
  2. 函数限制：Taylor展开的收敛要求限制了方法的普适性
  3. 参数选择：条件数阈值和Taylor项数的选择缺乏理论指导
  4. scalability：对于大型复杂程序的适用性需要进一步验证

影响力

  1. 学术价值：为浮点错误修复领域提供了新的理论框架和实用工具
  2. 工业应用：GSL开发者的积极反馈显示了实际应用潜力
  3. 可复现性：提供了完整的复现包，有利于后续研究

适用场景

  1. 科学计算库：如GSL、NumPy、SciPy等数值计算库的错误修复
  2. 关键系统：航空航天、金融系统中的浮点精度问题
  3. 教育研究：作为浮点错误分析和修复的教学工具

参考文献

论文引用了36篇相关文献，涵盖了浮点错误检测、修复、数值分析等多个方面，为研究提供了坚实的理论基础。关键参考文献包括Franco等人的数值bug系统性研究、ACESO和AutoRNP等代表性修复工具，以及相关的数学理论基础。

总体评价：这是一篇高质量的软件工程研究论文，针对浮点程序错误修复这一重要问题提出了创新性解决方案。方法在理论上有坚实基础，实验验证充分，实际应用效果显著。虽然存在一定局限性，但为该领域的发展做出了重要贡献。