引言

想象这样一个未来: 安全关键型系统——如自动驾驶汽车或医疗诊断工具——由神经网络控制。在这些网络获准上路或进入医院之前，它们要经过一个严格的过程，称为形式化验证 (formal verification) 。 这一过程会生成数学证明，保证即使攻击者试图欺骗网络，网络也能表现正确。

这听起来像是终极的安全网。如果数学证明网络是鲁棒的，我们就应该是安全的，对吧？

根据一篇题为 “No Soundness in the Real World” 的精彩研究论文，答案是一个令人不安的 “不” 。 研究人员认为，当前最先进的验证方法正在追逐幻影。它们验证的是神经网络的理论数学模型 (代码的“柏拉图式理想形态”) ，但未能验证在物理硬件上运行的已部署网络。

罪魁祸首是什么? 浮点运算。

计算机无法完美地表示实数。它们只能近似表示。GPU 计算求和的方式与 CPU 略有不同，特定的软件库处理方式也可能不同。这篇博客文章将探讨研究人员如何证明这些微小的数值差异可以被武器化。他们证明，一个神经网络可以被世界上最好的验证器在数学上“证明”是安全的，但仍然隐藏着恶意的后门，只有在特定的现实世界环境中部署时，这些后门才会触发灾难性的故障。

背景: 验证 vs. 现实

要理解这项工作的严重性，我们需要先了解验证试图达到的目标。

理论验证问题

在标准的鲁棒性验证场景中，我们有一个神经网络 \(f\) 和一个输入 \(x^*\)。我们希望确保对于输入的任何微小扰动 (在特定范围内，通常称为 \(\epsilon\)) ，网络的预测保持不变。

目标是证明对于该微小邻域内的所有输入，网络的输出始终是“安全”的 (例如，正确类别的得分高于所有其他类别) 。形式化表达如下:

标准理论验证方程。

这里，\(f(x; \theta)\) 代表具有参数 \(\theta\) 的理论神经网络函数。该方程指出，对于域 \(D\) 中的每个输入 \(x\)，输出都是非负的 (意味着正确的分类获胜) 。

反派: 浮点非结合性

上面的方程假设网络是在实数 (\(\mathbb{R}\)) 上运行的。但真实的硬件使用的是浮点数。

在标准数学中，加法满足结合律 (associative) 。 这意味着:

\[(a + b) + c = a + (b + c)\]

在浮点运算中，由于每一步都存在舍入误差，这不成立 。

\[(a \oplus b) \oplus c \neq a \oplus (b \oplus c)\]

考虑这样一个场景: 你将一个非常大的数字与一个非常小的数字相加。由于精度限制，这个小数可能会被“吞没”。如果你改变运算顺序——也许是通过在并行 GPU 上而不是单线程 CPU 上运行代码——最终结果就会改变。

现有的验证器通常假设一个这些差异无关紧要的“理论模型”，或者它们界定的是理论上的全精度输出。这篇论文认为，这种假设造成了一个巨大的安全漏洞。

核心方法: 已部署验证

研究人员提出了一种范式转变。我们不应该验证理论函数 \(f\)。我们必须验证已部署函数 \(r\)。

已部署函数 \(r(x; \theta, \mathcal{E})\) 不仅取决于输入和权重，还取决于环境 (Environment, \(\mathcal{E}\)) 。 环境决定了硬件、精度 (32 位 vs. 64 位) 、编译器优化以及运算顺序。

新的验证问题如下所示:

已部署验证的方程。

符号上的这一看似微小的变化具有巨大的含义。如下图所示，“理论模型”可能是完全安全的 (圆圈完全位于蓝色区域内) 。然而，根据环境 (\(\mathcal{E}_1, \mathcal{E}_2, \mathcal{E}_3\)) 的不同，实际的决策边界会发生偏移。

图 1. 一个恶意的二元分类器及其决策边界和两种颜色的类别 (概念插图) 。图中展示了理论网络及其三种不同的部署，包括在一个恶意行为 (翻转类别) 显现的对抗环境中的部署。同时也展示了一个输入 x 及其敏感域。

在上图中:

  • 理论模型 (Theoretical Model) : 输入 \(x\) 是安全的。
  • \(\mathcal{E}_1\) & \(\mathcal{E}_2\): 由于浮点噪声，边界会摆动，但 \(x\) 可能仍然是安全的。
  • \(\mathcal{E}_3\) (对抗环境) : 研究人员表明，构建一个能够检测环境特定浮点“指纹”并完全翻转其行为的网络是可能的 (由区域变为黄色所示) 。

为什么当前的验证器会失败 (理论层面)

该论文在数学上证明了像区间边界传播 (Interval Bound Propagation, IBP) ——许多验证工具的基石——对于已部署的网络是不健全 (unsound) 的。

在 IBP 中，我们不是将单个数字传递给网络，而是传递一个区间 \([min, max]\)。如果最终输出区间完全为正，则网络通过验证。

然而，研究人员证明，除非你知道硬件使用的确切运算顺序 (特定的“表达式树”) ，否则你的区间可能并不包含实际的浮点结果。

在随机环境中 (比如 GPU 随机并行化操作) ，实际输出 \(z\) 可能会落在计算出的区间 \([a, b]\) 之外。

关键洞察: 从理论上界定全精度输出并不能保证你界定了随机环境中浮点数的输出。

武器化数学: 攻击

这项研究最令人兴奋的部分在于作者如何演示这一漏洞。他们不仅仅是发现了一个 bug；他们制造了一种武器。

他们设计了包含“后门”的对抗性网络 (Adversarial Networks) 。 这些是标准的神经网络，其中插入了一个微小的、隐藏的“探测器神经元”。

探测器神经元

这个神经元就像一根绊索。它执行特定的计算，在标准环境中结果为 0，但在目标环境中由于浮点异常会导致非零值 (反之亦然) 。

当探测器触发时，它会激活一个后门，翻转网络的预测。

1. 检测精度 (32 位 vs 64 位)

研究人员设计了一个神经元，如果精度是 (例如) 32 位，它输出 0，如果是 64 位，它输出 1。如果验证器在 64 位模式下运行 (许多验证器为了“更高精度”而这样做) ，它就不会看到错误。但当模型部署在 32 位移动设备上时，陷阱就会触发。

2. 检测运算顺序

研究人员创建了“对验证器不友好”的探测器。这些探测器依赖于数字的求和，其中运算顺序会极大地改变结果。

看看这个用于探测器的方程:

涉及 omega 和 1 求和的验证器友好型探测器方程。

虽然上面的方程是“友好的” (验证器更容易处理) ，但研究人员增加了难度。看看下面的方程:

涉及 2/h 和 omega 求和的验证器不友好型探测器方程。

最后，最难的探测器 (“Order3”) :

最难探测器的方程: 1 的求和加上 omega 减去 omega。

在这个“Order3”探测器中，网络对一系列 \(1\) 求和，加上一个大数 \(\omega\)，再减去 \(\omega\)。

  • 理论结果: 1 的总和。
  • 浮点结果: 如果 \(\omega\) 加得太早，由于精度限制，它可能会“吞没”微小的 \(1\)。如果是最后才加，这些 \(1\) 就能保留下来。

研究人员构建了网络，使得如果求和以“错误”的顺序 (部署顺序) 发生，输出就会翻转。

后门架构

这是如何集成的？如下图所示，“探测器 (Detector) ”与主网络并行运行。如果探测器被触发 (基于环境输出特定值) ，它会向 Logits (对数几率) 注入一个巨大的值，强制改变分类。

图 2. 后门集成图，显示探测器与 Logits 并行。

实验与结果

研究人员采用了一个鲁棒的 MNIST 分类器，并用这些后门感染了它。然后，他们用世界上最好的验证器对其进行测试。

1. 部署环境至关重要

首先，他们证明了这些后门在现实世界中确实有效。他们在不同的硬件 (CPU vs. GPU) 和不同的软件框架 (PyTorch vs. Flux) 上运行了带有后门的网络。

请看 表 2 :

表 2. 不同环境下带有后门的网络的测试准确率。

注意 “Order1” 这一行。

  • PyTorch CPU: 0.11% 准确率 (后门触发了！模型完全失效) 。
  • Flux CPU: 98.11% 准确率 (模型表现正常) 。

这证实了仅仅改变库或硬件就足以改变运算顺序从而触发陷阱。

2. 精度陷阱

在 表 1 中，他们展示了精度攻击的结果。

表 1. 基于 32 位与 64 位精度的后门网络的测试准确率。

  • 第 1 行: 旨在 32 位环境下失效的模型。在 32 位环境中，准确率降至 0.11%。在 64 位环境中，准确率为 98.11%。
  • 第 2 行: 旨在 64 位环境下失效的模型。它在 32 位下工作完美，但在 64 位下灾难性地失效。

3. 验证器的失败

最确凿的证据在 表 3 中。研究人员测试了最先进的验证器，如 MIPVerify、\(\beta\)-CROWN 和 DeepPoly。这些工具本应保证安全。

“Order2”、“Order3” 和 “Precision” (精度) 列展示了漏洞。

表 3. 验证器对攻击的脆弱性。

  • “Unsound” (不健全) 意味着验证器说“这个网络是安全的”，但网络实际上包含一个可能导致其崩溃的后门。
  • 看看 Order3 列。 每一个验证器都失败了。 它们都认证网络具有鲁棒性，却忽略了特定的求和顺序会触发完全的故障。
  • 看看 Precision 列。在 64 位模式下运行的验证器认证 32 位攻击是安全的，完全没有意识到部署环境将是 32 位的。

它们为什么会失败？

验证器失败是因为它们使用了“理论健全性”。它们正确地界定了实数或理想化区间的数学运算。但它们没有考虑到部署硬件的具体、混乱、非结合的浮点运算。

例如，当使用基于 Zonotope (环带多面体) 的验证 (如 DeepZ) 时，边界是使用加宽的区间来计算的，以考虑误差:

带有误差项的 Zonotope 边界计算方程。

即使有了这些误差项 (\(\varepsilon\)) ，研究人员证明仍有特定的运算顺序会落在计算出的边界之外。

结论与启示

这篇论文为 AI 安全社区敲响了警钟。它强调了一个关键的“实现差距 (Implementation Gap) ”。

  1. 理论健全性 \(\neq\) 实际健全性: 你不能在真空中验证神经网络。你必须在其部署的背景下验证网络。
  2. 威胁是真实的: 攻击者可以隐藏当前代码分析和数学验证都看不见的恶意逻辑，这些逻辑只有在目标的特定 GPU 或 CPU 上才会触发。
  3. 验证的未来: 为了真正安全，验证器需要对硬件建模。它们需要知道目标是使用 cuDNN 的 NVIDIA GPU 还是使用 PyTorch 的 CPU。它们必须考虑到确切的精度和舍入模式。

直到验证器弥合抽象数学与硅片现实之间的差距，我们的安全“保证”仍然令人担忧地脆弱。下次当你看到 AI 模型上有“已验证鲁棒性”的标签时，你可能想问一句: “是在哪款芯片上验证的？”