技术摘要：浮点神经网络是可证明鲁棒的通用近似器

1. 问题陈述

经典的通用近似（Universal Approximation, UA）定理以及更近期的区间通用近似（Interval Universal Approximation, IUA）定理确立了神经网络可以以任意精度近似连续函数及其直接像映射（区间）。然而，这些理论结果依赖于一个不切实际的假设，即神经网络是在无限精度的实数上运行的。在实践中，软件实现使用有限精度的浮点算术，这引入了离散化、有界性、舍入误差以及潜在的溢出/下溢问题。

本文解决的核心开放性问题是：IUA 定理在浮点设置下是否成立。具体而言，一个浮点神经网络在通过抽象解释（区间域）进行分析时，能否完美地捕捉到一个经过舍入的目标函数的直接像映射？此前的研究未能建立这一点，主要是因为浮点运算中固有的舍入误差使得用于实值网络的证明技术（例如，依赖于精确算术构建特定子网络的技巧）失效。

2. 方法论

作者开发了一个严谨的理论框架，以弥合实值理论与浮点实践之间的鸿沟。

2.1 浮点语义的形式化

论文将神经网络定义为在有限浮点数集 $\mathcal{F}$ 上的函数，利用符合 IEEE-754 标准的操作（$\oplus, \ominus, \otimes$）以及“舍入至最近（偶数优先）”模式。区间语义 $\nu^\sharp$ 被定义在抽象区间 $\langle a, b \rangle$ 上，代表 $[a, b]$ 内的浮点数集合。

2.2 激活函数的条件

为了证明该定理，作者引入了条件 1，这是一组针对激活函数 $\sigma: \mathcal{F} \to \mathcal{F}$ 的约束。这些条件确保该函数能够：

1. 输出精确的零和特定的非零值（在有界范围内）。
2. 在临界值 $\eta$ 附近表现出单调性或特定的阈值行为。
3. 满足类 Lipschitz 连续性约束，以防止无界增长。

论文证明了常见激活函数（ReLU, GELU, Sigmoid, Tanh 等）的正确舍入版本满足这些条件，这通常是通过利用引理 1（将实值函数的属性映射到其浮点对应物）来实现的。

2.3 证明策略：可分性与指示函数构造

证明的核心在于构建一个充当“通用区间近似器”的神经网络。该方法分为两个主要阶段：

1. 可分性： 作者定义了一个称为 $([a, b]_\mathcal{F}, \eta, K, L_\phi, L_\psi)$-可分性 的属性。该属性保证了存在能够通过区间语义实现缩放指示函数（例如，将输入 $\le z$ 映射为 0，将输入 $> z$ 映射为 $K$）的网络。

   • 证明构建了特定的子网络（例如 $\mu_z, \tau_{\theta, \theta'}$），利用舍入误差来“收缩”区间。例如，设计一个网络，使其在经过激活函数后，特定范围内的输入会映射到单点区间 $\langle \eta, \eta \rangle$ 或 $\langle \eta^+, \eta^+ \rangle$。
   • 至关重要的是，该构造避免了中间层出现无穷大值，解决了在将权重缩放到任意量级时可能出现的溢出问题，而这在实值证明中是一个难题。

2. 用于通用近似的组合： 利用可分性属性，作者构建了以下内容的网络：

   • 任意方框的指示函数。
   • 输入空间中任意子集的指示函数。
   • 最后是目标函数本身，通过将目标函数表示为这些指示函数的浮点线性组合来实现。证明过程仔细管理了浮点求和，以确保累积的舍入误差能够完美对齐，从而重建目标函数的像映射。

3. 核心贡献

3.1 浮点 IUA 定理（定理 1）

论文证明了对于任何目标函数 $f: \mathbb{R}^d \to \mathbb{R}$ 以及满足条件 1 的广泛激活函数类，存在一个浮点神经网络 $\nu$，其区间语义 $\nu^\sharp$ 精确地计算了经过舍入的目标函数 $\hat{f}$ 在定义域 $[-1, 1]^d \cap \mathcal{F}^d$ 上的直接像映射。

• 精确性： 不同于实现 $\delta$-近似的实值 IUA，浮点版本实现了 $\delta = 0$（精确匹配），因为定义域是有限的。
• 泛化性： 该定理适用于任意目标函数（不仅限于连续函数）以及广泛的激活函数，包括恒等函数（这在实值 IUA 中是不可能的）。

3.2 可证明鲁棒网络的存在性（定理 2）

作为推论，论文证明了如果存在一个理想的鲁棒分类器（即使它不是神经网络），那么就存在一个可以通过区间分析实现可证明鲁棒并做出相同预测的浮点神经网络。这解决了这样一个问题：在浮点设置下，可证明鲁棒网络的表达能力是否存在基本限制：不存在这样的限制。

3.3 浮点区间完备性（定理 3）

论文提出了一个关于计算完备性的惊人结果：仅使用加法 ($\oplus$) 和乘法 ($\otimes$) 的直线型浮点程序类是浮点区间完备的。这意味着这类简单的程序可以模拟任何以有限浮点数为输入并返回有限或无穷浮点数的终止浮点程序的区间语义。这一结果将 IUA 定理扩展到了整个定义域 $\mathcal{F}^d$ 上的恒等激活函数。

4. 结果与对比

论文强调了新的浮点 IUA 定理与以往实值结果之间的三个基本区别：

1. 目标函数： 实值 IUA 近似连续函数；浮点 IUA 精确计算任何舍入目标函数的像（因为定义域是有限的）。
2. 激活函数： 实值 IUA 需要“可压缩”的激活函数（非仿射）；浮点 IUA 即使对于恒等激活函数也成立。这是因为由于舍入误差的存在，浮点仿射变换在实数上并非严格仿射，从而能够打破线性并近似非线性行为。
3. 近似 vs. 精确： 实值结果提供 $\delta$-近似；浮点结果提供对舍入目标函数的精确匹配。

5. 意义与主张

作者声称这项工作弥合了基于抽象解释的鲁棒性验证与实际浮点实现之间的理论差距。

• 理论保证： 它证明了缺乏最先进准确性的可证明鲁棒网络，并不是由于其表达能力的根本限制，而很可能是由于优化挑战或所使用的特定验证算法导致的。
• 完备性： 区间完备性的结果表明，简单的算术运算足以在区间语义下模拟复杂的浮点行为，这为理解浮点程序的计算能力提供了新见解。
• 实际相关性： 通过验证浮点数的 IUA 定理，本文为在浮点算术作为标准处理的安全性关键领域（医疗保健、自动驾驶）中使用区间分析提供了理论基础。

论文明确指出，这些是存在性证明；它并不声称当前的训练算法可以轻松找到此类网络，也不提出新的训练方法。其贡献纯粹是理论性的，即确立了“可证明鲁棒的浮点网络”的“表达能力天花板”实际上是不存在的。