验证数值计算与区间算术

实区间与集合运算 ​

实区间 $X=[\underset{―}{x},\bar{x}]$ 表示满足 $\underset{―}{x}\le x\le \bar{x}$ 的全部实数，而不是某个中心值附带一个非形式的“误差条”。端点相同得到点区间；若允许 $\underset{―}{x}>\bar{x}$，通常把它作为空区间的编码，具体约定必须在实现接口中声明。

对二元实运算 $\circ$，它在区间上的精确集合像是

$$X\circ Y=\{x\circ y:x\in X,y\in Y\}.$$

加减法的端点公式为

$$X+Y=[\underset{―}{x}+\underset{―}{y},\bar{x}+\bar{y}],$$$$X-Y=[\underset{―}{x}-\bar{y},\bar{x}-\underset{―}{y}].$$

乘法需取四个端点乘积的最小值和最大值。除法可写成乘倒数区间，但前提是 $0\notin Y$；若除数区间跨过零，实集合像通常分裂为两个无界部分，不能用一个普通有界区间悄悄替代。

包含不变量与向外舍入 ​

精确实数端点通常不能由有限浮点格式公理库浮点数系统与 IEEE 754Floating-point system · IEEE 754以有限尾数和指数表示机器数，并说明 IEEE 754 的特殊值、格式与运算语义。表示。验证区间计算因此维护包含不变量：机器返回的区间 $\hat{F}(X)$ 必须满足

$$\{f(x):x\in X\}\subseteq \hat{F}(X).$$

下端点向 $-\mathrm{\infty }$ 舍入，上端点向 $+\mathrm{\infty }$ 舍入，称为 directed rounding 或 outward rounding。以加法为例，机器实际计算

$$\hat{X}+\hat{Y}=[{\mathrm{rd}}_{-}(\underset{―}{x}+\underset{―}{y}),{\mathrm{rd}}_{+}(\bar{x}+\bar{y})].$$

最近舍入公理库舍入、机器精度与 ulpRounding and unit roundoff · Unit in the last place · ulp用舍入映射、ulp 与 unit roundoff 描述实数映到邻近浮点数时的局部精度。只保证结果接近精确端点，不能保证方向正确；两个最近舍入端点都可能落到真实集合内部，产生看似更窄却不可靠的区间。验证实现还要固定格式、舍入模式、溢出、次正规数与 NaN 处理，不能只在纸面公式旁写一句“考虑浮点误差”。

若每个基本区间操作都满足包含性，表达式树上的组合也满足包含性。这是验证数值计算的局部证书接口：证明不要求算出未知真值，只需证明每一步返回的集合覆盖该步所有可能真值。

一条可追踪的计算 ​

取

$$X=[1,2],Y=[3,4].$$

精确区间运算给出 $X+Y=[4,6]$，$XY=[3,8]$。若机器端点运算恰好可表示，向外舍入不扩大它们；若端点不可表示，外包络只扩到相邻的安全浮点数。区间宽度因此同时承载输入不确定性和运算舍入，不应把两者都叫作 unit roundoff。

考虑函数 $f(x)=x(1-x)$ 在 $X=[0,1]$ 上的自然区间扩张。先算 $1-X=[0,1]$，再乘得 $[0,1]$，而真实值域是 $[0,1/4]$。返回区间可靠，却不紧。这一差距来自表达式结构没有利用抛物线的相关性，不是向外舍入“算错了”。

若把同一个 $X=[1,2]$ 代入 $x-x$，自然区间计算得到

$$X-X=[-1,1],$$

真实集合却只有 $\{0\}$。两个出现位置在普通区间规则中被当作可独立取值，相关性丢失产生 dependency problem。改写表达式有时能收紧结果，但一般的相关性需要 affine arithmetic、Taylor models 或更关系化的表示。

“验证”保证了什么 ​

一个可靠外包络证明真值在区间内，不证明区间足够窄，也不证明问题条件良好。区间 $[-{10}^{100},{10}^{100}]$ 可以完全可靠，却几乎没有决策价值。验证算法往往结合分支细分、单调性、导数界或 interval Newton，不断收缩区间；这些附加步骤的终止性和收缩率需要各自的定理。

包含性也依赖实现模型。若编译器改变舍入模式、把两步融合成 FMA、在扩展精度寄存器中延迟舍入，或者并行线程共享全局舍入状态，纸面证书未必对应实际指令。成熟区间库会用硬件指令、受控舍入或误差无关的端点算法封装这些细节，并以测试覆盖异常值。

区间结果不是概率置信区间。它不需要为未知量指定分布，保证形式是确定性的全称包含；置信区间则在重复抽样下具有覆盖概率，两者的随机对象与量词不同。区间也不自动证明模型真实：若输入范围漏掉真实输入，后续再严谨的向外舍入仍只验证了错误前提下的计算。

与区间抽象域的分层 ​

区间抽象域公理库区间抽象域Interval abstract domain · Interval analysis domain以变量上下界近似数值状态，并用区间 transfer、join 与 widening 求解程序范围。会把程序中每个变量映射到区间，并在控制流汇合处做 join、在循环中做 widening。它的静态分析可靠性还需证明抽象转移函数覆盖所有具体程序步骤；本页只提供算术操作的集合外包络和有限精度实现边界。

两层可靠性不能合并成一句“用了区间所以分析可靠”。上层可能错误建模整数溢出、数组越界或分支条件；下层也可能因舍入方向错误漏掉真值。只有算术外包络、语言语义与抽象转移的证明逐层接上，最终警报才具有不漏报的含义。

验证数值计算还用于严格根包围、全局优化和计算机辅助证明。它交付的是可检查的包含证书，而非单纯多打印几位小数；更高精度能减少舍入扩张，却不能单独消除变量相关性或错误模型。

参考资料

• Ramon E. Moore, R. Baker Kearfott, and Michael J. Cloud, Introduction to Interval Analysis, SIAM, 2009, Chs. 1–3。
• IEEE Computer Society, IEEE Standard for Interval Arithmetic, IEEE Std 1788-2015。
• Siegfried M. Rump, “Verification Methods: Rigorous Results Using Floating-Point Arithmetic,” Acta Numerica 19, 2010, pp. 287–449。
• Timothy J. Hickey, Qun Ju, and Maarten H. van Emden, “Interval Arithmetic: From Principles to Implementation,” Journal of the ACM 48(5), 2001, pp. 1038–1068。