真实世界没有可靠性：已部署神经网络验证的挑战

1. 01这篇论文试图解决什么问题？

   作者称理论 sound 的验证器在真实部署环境中并不 sound，并用后门网络加以证明。

   核心问题：现有神经网络验证器验证的是全精度理论模型，而非实际部署的浮点模型，作者称理论 soundness 不蕴含部署中的 practical soundness。

   • 场景与重要性：形式化验证意在为部署的神经网络提供安全保证（如对抗鲁棒性），但部署环境通过硬件和软件特性影响数值计算，常带来随机行为（论文引 Schlögl et al., 2023）。验证理论模型与验证部署网络是两个不同的问题。
   • 现有方法的不足：作者称所知的最先进验证器都把浮点问题当作验证理论模型的障碍来处理，而非验证目标本身；即使验证用全精度执行，也只验证了理论模型而非部署网络。
   • 核心观察：浮点运算的问题不在舍入误差本身，而在非结合性和依赖环境的随机性；部署模型是与理论模型根本不同的数学对象，攻击者可借此设计对验证不可见的部署敏感行为。
   • 论文的贡献：形式化部署验证问题并证明理论 sound 不蕴含 practical sound；构造由环境特征（精度、运算顺序）触发的部署敏感后门；对多个验证器做实证评测，作者报告全部被测验证器都易受这些部署特定攻击。
   • 威胁模型：
     • 攻击者目标：让后门行为在验证时隐藏、在特定部署环境中激活（如翻转分类结果）。
     • 攻击者知识：了解部署环境的特征，如浮点精度与运算顺序（expression tree）。
     • 攻击者能力：修改网络参数，插入检测环境特征的 detector 神经元（基于 Zombori et al., 2021 的方法）。
     • 受害系统：只验证理论模型、不显式建模部署环境的 sound 验证器（IBP、Polyhedra、Zonotope 类）。

   收起这一问

2. 02有哪些相关研究？

   相关工作覆盖 sound/complete 验证方法、浮点数值问题与既有对验证器的攻击三条线。

   Sound（不一定 complete）的验证方法

   • Singh et al., 2018; 2019a; Zhang et al., 2018; Xu et al., 2021——基于 bound propagation（Xu et al., 2020）和线性化的方法，处理浮点计算并正确界定全精度值。
   • Gowal et al., 2018——interval bound propagation（IBP），本文理论分析针对的基础技术之一。

   Sound 且 complete 的验证方法

   • Katz et al., 2017; Ehlers, 2017; Dutta et al., 2018; Tjeng et al., 2017——把验证形式化为 SMT 或 MILP 问题求解；论文指出其缺点是 NP-complete、依赖可能含破坏 soundness 的启发式的求解器。
   • Bunel et al., 2020; Wang et al., 2021; Palma et al., 2021; Ferrari et al., 2022——branch-and-bound（BaB）框架，可部分或全部在 GPU 上执行以提升效率。

   部署环境的数值问题

   • Schlögl et al., 2023——证明不同平台（数值表示、并行化、硬件、卷积优化）显著影响部署网络的输出，但非从验证角度研究。
   • Shanmugavelu et al., 2025——证明仅通过置换部署环境中结合性运算的顺序即可生成对抗输入。
   • Cordeiro et al., 2025——与本文并行的工作，把同一现象称为 implementation gap。
   • Lohar et al., 2023——定点算术替代路径，量化可实现有界舍入误差，作者认为可支持 practically sound 验证。

   对验证器的攻击

   • Zombori et al., 2021——利用验证算法本身（MILP 求解器）的数值问题欺骗验证器；论文指出这类问题在基于 bound propagation 的 sound 验证器中不存在，而本文利用的是全精度模型与部署之间的差异，且作者称自己的构造能误导所知的每个 sound 验证器。本文的 detector 嵌入方法也基于该工作。
   • Jia & Rinard, 2021——可视为对验证的对抗攻击；论文指出其仅在部署与验证算法使用不同数值精度时有效，且不是本文提出的通用可证明框架。

   基线与基准：被评测的验证器为 MIPVerify、MN-BAB、β-CROWN BaB、GCP-CROWN、DeepPoly、RefinePoly、DeepZ、RefineZono（Table 3）；攻击对象为 Wong & Kolter (2018) 公开的 MNIST 鲁棒网络（WK17a），另复现了 Zombori et al., 2021 的攻击作对照。

   作者将本文定位为：不研究验证理论模型时的浮点问题，而是主张验证目标应转向部署模型本身。

   收起这一问

3. 03论文如何解决这个问题？

   形式化部署验证问题，证明 IBP 及符号化方法在随机环境下不 sound，再构造环境触发的后门网络做实证。

   整体思路分三步：定义部署验证（deployed verification）问题；在求和函数这一简化情形上证明现有 soundness 技术对部署不 sound；构造由环境特征触发的对抗网络，实证检验验证器。

   问题设定与形式化

   • 理论模型：分类网络 f(.; θ): Rⁿ → Rᵐ，验证目标是证明输入邻域内所有输入与 x* 同类，论文通过附加仿射层把问题化为 ∀x ∈ D_ϵ,p(x^∗), f(x; θ) ≥ 0（Equation 1）。
   • 部署模型：r(.; θ, E): X → Y，其中 E 完整刻画环境的数值表示、硬件、软件优化、运算顺序及随机性；随机环境下 r 的值是概率大于零的输出向量集合。
   • 部署验证问题：∀x ∈ D_ϵ,p,E(x^∗) ∀z ∈ r(x; θ, E), z ≥ 0（Equation 2），即要求覆盖部署环境中所有可能的浮点输出。
   • practical soundness：验证器只有正确界定部署输出（而非全精度输出）才算 practically sound。

   理论分析（Section 6）

   • 简化设定：分析零长度区间输入的求和函数；作者指出该简单情形已能暴露问题，更复杂的网络会继承这些问题。
   • Proposition 6.1：IBP 按某 expression tree o 求值时，区间包含全精度值；若 o 恰好最小化/最大化部署输出，则区间也正确覆盖 Lr/Ur（证明见附录 A）。
   • Proposition 6.2：在允许任意 expression tree 的 IEEE 754 环境下，存在树 o 与输入使 IBP 区间不覆盖 Lr 或 Ur，即 IBP 一般不保证 practical soundness。
   • Proposition 6.3：递减序、递减绝对值序等直观排序也不能保证取到最小输出；作者假设一般情形下求最优 expression tree 是 NP-hard 的（引 Kao & Wang, 2000 的相近结果）。
   • 符号化方法：在求和特例下，Polyhedra 类（DeepPoly、CROWN）退化为 IBP；Zonotope 类（DeepZ、RefineZono，用 Miné, 2004 的 widening）区间更宽，Proposition 6.4、6.5 表明其同样不保证 practical soundness。

   对抗网络构造（Section 7、附录 B）

   • detector 神经元：无激活的线性神经元，输入为全 1 常向量，输出为权重与偏置之和；利用特殊数 ω（binary32 下 ω = 2²⁴，binary64 下 ω = 2⁵³，默认舍入下 ω + 1 = ω）使输出依赖精度或求和顺序。
   • Precision detector：输出在某一精度下为 0、在更高精度下为 1，用于检测部署精度。
   • Order1（verifier-friendly）：默认顺序下输出 0，多数顺序下输出落在 [1, h2]，实验中 h1 = 4、h2 = 15。
   • Order2、Order3（verifier-unfriendly）：默认顺序下输出非 0，只有很少的顺序使区间分析覆盖 0；两者均设 h = 512，Order3 只有 ω 排在第一或第二位时才覆盖 0。
   • 后门集成：按 Zombori et al., 2021 的方法把 detector 嵌入宿主网络（附录 B 给出完整构造与提示词式细节），detector 输出控制 logits 是否移位；后门与输入无关、纯由环境触发。附录 B 给出了完整实现细节。

   成功判定

   • 后门有效性：部署环境中测试准确率从正常水平降到接近零即视为触发。
   • 验证器被攻击成功：验证器对含后门的网络仍报告非零 verified robust accuracy（未能发现后门），记为 unsound；检测到后门则返回 0% verified robust accuracy，记为 sound（Section 8.4）。

   收起这一问

4. 04论文做了哪些实验？

   在一个 MNIST 网络上植入 5 种环境触发后门，10 个验证器配置对 Precision 和 Order3 全部漏检。

   实验设置

   • 被攻击网络：Wong & Kolter (2018) 的 MNIST 网络（WK17a），两层卷积（stride 2，16 和 32 个 4×4 滤波器）加 100 神经元全连接层，ReLU 激活，按 l∞ 半径 0.1 做鲁棒训练。
   • 对抗网络：共 5 个——2 个 Precision 攻击（分别在 32-bit、64-bit 环境触发）和 3 个 expression tree 攻击 Order1、Order2、Order3。
   • 被测验证器：MIPVerify、MN-BAB、β-CROWN BaB（32-bit CPU、64-bit CPU、64-bit GPU 三种配置）、GCP-CROWN、DeepPoly、RefinePoly、DeepZ、RefineZono，共 10 个配置（Table 3）。
   • 部署环境：PyTorch 与 Flux（Julia）× CPU/GPU × batch size 1/10，共 8 种；硬件为 AMD Ryzen 7 3800X、RTX 4080 SUPER（附录 C.1）。
   • 评测协议：验证 MNIST 测试集前 100 个样本；基座网络在这 100 个样本上的 verified robust accuracy 为 97%（complete 方法），DeepPoly 为 96%、DeepZ 为 94%（附录 C.2）。
   • 判定方式：验证器检出后门返回 0% verified robust accuracy 记为 sound，否则记为 unsound；论文未报告重复次数。

   主结果

   据 Table 3（验证器对四种攻击及 Zombori et al., 2021 攻击的 sound/unsound 判定）：

   表格较宽，可左右滑动

   验证器（验证环境）	Precision	Order1	Order2	Order3	Zombori et al.
   MIPVerify（64-bit, CPU）	unsound	sound	unsound	unsound	unsound
   MN-BAB（64-bit, GPU）	unsound	sound	unsound	unsound	unsound
   β-CROWN BaB（32-bit, CPU）	unsound	sound	unsound	unsound	未报告（无 32-bit 模型）
   β-CROWN BaB（64-bit, CPU）	unsound	sound	unsound	unsound	sound
   β-CROWN BaB（64-bit, GPU）	unsound	sound	unsound	unsound	sound
   GCP-CROWN（64-bit, CPU）	unsound	sound	unsound	unsound	sound
   DeepPoly（64-bit, CPU）	unsound	sound	sound	unsound	sound
   RefinePoly（64-bit, CPU）	unsound	sound	sound	unsound	unsound
   DeepZ（64-bit, CPU）	unsound	sound	sound	unsound	sound
   RefineZono（64-bit, CPU）	unsound	sound	sound	unsound	未报告（Gurobi error）

   • 作者称没有任何被测方法是 practically sound 的：全部漏检 Order3 和 Precision 网络。
   • 作者称任务越难失败的验证器越多；Order2 上部分成功被作者归因于更宽的区间和运算顺序的偶然覆盖，并称理论上无保证。
   • 作者称所有验证器都易受 Precision 攻击，支持验证器应针对特定浮点精度定制。

   后门有效性（Section 8.2）

   • Precision 攻击：32-bit 触发的网络在 32-bit 环境下测试准确率 0.11%、64-bit 下 98.11%；64-bit 触发的网络正好相反（Table 1）。
   • Order 攻击：batch size 1 时，Order1 在 PyTorch CPU/GPU 和 Flux GPU 上为 0.11%、Flux CPU 上 98.11%；Order2 仅在 Flux GPU 上为 0.11%；Order3 在全部 8 种环境下均为 98.11%（Table 2）。
   • 作者解读：三种后门至少在一个环境中激活，说明这些环境执行了不同的 expression tree；Order3 未观察到触发，但作者认为这不代表网络安全，sound 验证器仍应检出。

   与 Zombori et al., 2021 的对比（Section 8.5）

   • 测了什么：复现 Zombori et al., 2021 的网络（类似 Order1），它触发的是验证器自身的数值误差。
   • 结果：MIPVerify、MN-BAB、RefinePoly 对该攻击 unsound，DeepPoly、DeepZ、β-CROWN（64-bit）、GCP-CROWN sound（Table 3）。
   • 作者解读：该攻击只对使用某种优化的验证器有效；本文攻击利用全精度模型与部署的差异，其中最强的 Precision 和 Order3 对所有只具理论 soundness 的验证器有效。

   其他消融与分析

   • batch size 影响：batch size 从 1 改为 10 后，Order1 在 PyTorch GPU 与 Flux CPU 上的触发情况翻转（Table 2）。
   • MIPVerify 细节：对 Precision 攻击错误输出 97 个 safe 答案；对 Order2、Order3 错误验证 97% robust accuracy（附录 C.2.1）。
   • RefinePoly 细节：对 Order3 错误报告 96% robust accuracy，其余 4 个样本 MILP 求解时报错（附录 C.2.2）。
   • GCP-CROWN 细节：对未检出的后门错误报告 97 个 safe 结果，其余 3 个样本出错（附录 C.2.4）。

   收起这一问

5. 05有什么可以进一步探索的点？

   作者指出本文未给出 practically sound 验证器的实现方案；实验只覆盖一个 MNIST 网络与 10 个验证器配置。

   作者指出的局限与后续方向

   • 未提出解决方案：作者明确指出本文不包含任何 practically sound 验证器的实现提案，只聚焦于暴露问题，并认为解决问题很重要（Section 9）。
   • 需要对环境做强假设：作者认为 practically sound 验证器必须对部署环境做强假设，否则问题代价高到难以承受；确定性环境是优势，但验证必须知晓并利用环境的每个细节（Section 9）。
   • bound propagation 的适用条件：作者认为 bound propagation 只有在遵循确定性 expression tree、且传播考虑环境的（确定性）精度与舍入规则时才 practically sound（Section 9）。
   • 后门易被检测：作者指出本文后门权重很大且与输入无关，相当容易被检测，因为动机是理论性的，故基本忽略了实际实施攻击的方面（附录 B）。
   • 降低可检测性的设想：作者提出可把大权重分散到多层、或让后门只对特定输入扰动生效（如同时要求某像素超阈值且精度为 32-bit），但文中未实现（附录 B）。

   实验覆盖范围

   • 被攻击网络为 1 个 MNIST 卷积网络（WK17a，Wong & Kolter, 2018 的 checkpoint），论文未报告在其他数据集或架构上的实验。
   • 被测验证器共 8 种、10 个配置，均基于 IBP、Polyhedra 或 Zonotope 的 bound propagation 类方法（Table 3）。
   • 验证评测使用 MNIST 测试集前 100 个样本，论文未报告重复次数（Section 8.4、附录 C.2）。
   • 部署环境覆盖 PyTorch 与 Flux × CPU/GPU × batch size 1/10 共 8 种，硬件与软件版本在附录 C.1 给出。
   • 理论分析针对零长度区间输入的求和函数，作者称更复杂的函数类会继承这些问题，但未对其他函数类给出证明。

   收起这一问

6. 06总结一下论文的主要内容

   作者称理论 sound 的验证器对部署不 sound，给出证明并用环境触发后门让 10 个验证器配置全部漏检。

   一篇关于神经网络验证可靠性的攻击与分析论文，主张验证目标应从全精度理论模型转向实际部署的模型。

   • 问题：部署环境通过浮点非结合性和随机性使部署网络成为与理论模型不同的数学对象；作者称所知的先进验证器只验证理论模型，理论 soundness 不蕴含 practical soundness。
   • 方法：形式化部署验证问题（Equation 2）；在求和函数上证明 IBP 一般不覆盖部署输出的极值（Proposition 6.2），Polyhedra 与 Zonotope 类符号方法在该特例下退化为区间方法、同样不 sound（Proposition 6.4、6.5）；构造由精度或运算顺序触发、与输入无关的 detector 后门并嵌入 MNIST 网络。
   • 后门有效性：Precision 后门触发时测试准确率从 98.11% 降到 0.11%（Table 1）；Order1、Order2 在 8 种部署环境中至少一种触发，Order3 未观察到触发（Table 2）。
   • 主结果：10 个验证器配置（MIPVerify、MN-BAB、β-CROWN BaB×3、GCP-CROWN、DeepPoly、RefinePoly、DeepZ、RefineZono）对 Precision 和 Order3 攻击全部判 unsound，即漏检后门（Table 3，前 100 个 MNIST 测试样本）。
   • 对比：Zombori et al., 2021 的攻击只对部分使用优化的验证器有效；作者称本文攻击利用模型与部署的差异，对只具理论 soundness 的验证器普遍有效。
   • 作者结论：验证应聚焦部署网络的行为；practically sound 验证器可能需要对部署环境做强假设（如确定性环境并遵循其 expression tree），本文未提供实现方案。

   收起这一问

相关论文