paperbot · PL 论文追踪

全部论文 待读 收藏

P0 Cost of Soundness in Mixed-Precision Tuning

混合精度调优中健全性的代价
OOPSLA 9(OOPSLA2)2025匹配度 8/10 · 论文正落在用户明确列出的“浮点程序分析”核心兴趣上,系统比较了健全静态分析(抽象解释)与不健全动态采样在混合精度调优中的权衡,并且是问题驱动型:用 FPBench 实验挑战“动态方法总是更快”的常识,指出不健全方法误差可超限达 9 个数量级。不足之处在于它不含 LLM/Agent 或贝叶斯分析的交叉,且更偏评测/经验研究而非同时具备理论形式化与工程实现的工具论文。引用 1 inbox
Anastasia Isychev, Debasmita Lohar
crossref: 2026-09-10

AI 速览

一句话:首次系统评测混合精度调优工具,量化健全静态分析与不健全动态方法在性能收益与精度保证间的权衡。

数值程序常在资源受限硬件上重复执行,降低计算精度是提升性能的有效手段,但会引入舍入误差。混合精度调优在保证整体误差可接受的前提下,为部分变量与算符分配尽可能低的精度。现有工具用健全静态分析或动态采样来验证优化后程序的精度。本文首次对浮点程序的混合精度调优工具进行综合评测,定量比较健全静态方法与不健全动态方法,衡量性能收益、优化潜力与精度健全性保证之间的权衡,即“健全性的代价”。基于 FPBench 基准的实验推翻了“动态优化器总能生成更快程序”的常见看法:对小型直线数值程序,加入 regime inference 的健全工具能匹敌甚至优于动态方法,同时提供形式化正确性保证,代价是优化时间增加;而独立的健全工具过于保守,精度约束紧时尤甚;动态工具对不同目标始终有效,但超出最大允许误差最多达 9 个数量级。

问题
混合精度调优中,健全静态分析与不健全动态采样两种精度验证方式在实践中的性能收益与可靠性权衡缺乏系统比较。
方法
首次对现有浮点混合精度调优工具进行综合评测,在 FPBench 基准上定量比较健全静态与动态方法在性能收益、优化潜力与精度保证上的权衡(健全性的代价)。
评估
在标准 FPBench 基准套件上实验,发现带 regime inference 的健全工具在小型直线程序上可匹敌或超越动态工具,动态工具虽有效但误差可超出允许上界达 9 个数量级。
原文摘要(Abstract)

Numerical code is often executed repetitively and on hardware with limited resources, which makes it a perfect target for optimizations. One of the most effective ways to boost performance—especially in terms of runtime—is by reducing the precision of computations. However, low precision can introduce significant rounding errors, potentially compromising the correctness of results. Mixed-precision tuning addresses this trade-off by assigning the lowest possible precision to a subset of variables and arithmetic operations in the program while ensuring that the overall error remains within acceptable bounds. State-of-the-art tools validate the accuracy of optimized programs using either sound static analysis or dynamic sampling. While sound methods are often considered safer but overly conservative, and dynamic methods are more aggressive and potentially more effective, the question remains: how do these approaches compare in practice? In this paper, we present the first comprehensive evaluation of existing mixed-precision tuning tools for floating-point programs, offering a quantitative comparison between sound static and (unsound) dynamic approaches. We measure the trade-offs between performance gains, utilizing optimization potential, and the soundness guarantees on the accuracy—what we refer to as the cost of soundness . Our experiments on the standard FPBench benchmark suite challenge the common belief that dynamic optimizers consistently generate faster programs. In fact, for small straight-line numerical programs, we find that sound tools enhanced with regime inference match or outperform dynamic ones, while providing formal correctness guarantees, albeit at the cost of increased optimization time. Standalone sound tools, however, are overly conservative, especially when accuracy constraints are tight; whereas dynamic tools are consistently effective for different targets, but exceed the maximum allowed error by up to 9 orders of magnitude.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2988,
  title = {Cost of Soundness in Mixed-Precision Tuning},
  author = {Anastasia Isychev and Debasmita Lohar},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA2},
  year = {2025},
  doi = {10.1145/3763137}
}