面向浮点误差检测的数学导向方法
软件工程
2025-10-14 v1
摘要
浮点程序错误可能导致严重后果，尤其是在军事等关键领域。只有极小部分输入会诱导显著的浮点误差，这促使研究人员开发用于识别这些误差诱导输入的方法。尽管现有方法取得了一些成功，但仍存在两个主要局限：(1) 高计算成本：误差幅度评估依赖高精度程序，计算开销巨大。(2) 局限于长程收敛能力：当前方法在搜索中效率低下，相当于在 haystack 中寻找针。为此，我们提出一种新方法，命名为 MGDE，用于基于数学导向检测误差诱导输入。通过采用具有二次收敛性质的牛顿-拉弗森方法，我们实现了高效且高效的结果。由于识别误差诱导输入的目标是揭露底层 bug，我们将在实验中检测到的 bug 数量作为主要评估指标。FPCC 代表截至目前最有效的 SOTA 方法，我们以其为基准进行比较。FPCC 数据集包含 88 个单输入浮点程序。FPCC 能检测 48 个跨 29 个程序的 bug，而我们的方法成功识别了 89 个跨 44 个程序的 bug。此外，FPCC 的运行时间是我们方法的 6.4096 倍。我们还将该方法部署到多输入程序，识别了总计 9 个 bug，平均检测时间为 0.6443 秒/程序。相比之下，FPCC 在未检测到任何 bug 的情况下，平均计算时间为 100 秒/程序。
引用
@article{arxiv.2510.10081,
title = {A Mathematics-Guided Approach to Floating-Point Error Detection},
author = {Youshuai Tan and Zhanwei Zhang and Zishuo Ding and Lianyu Zheng and Jinfu Chen and Weiyi Shang},
journal= {arXiv preprint arXiv:2510.10081},
year = {2025}
}