格遍历实现多层感知机区间认证

背景

AI 安全中的一个基础问题是深度神经网络的对抗鲁棒性（adversarial robustness）：给定一个输入点，能否保证在某个扰动范围内模型的预测保持不变？现有研究大多关注于为每个输入找到尽可能大的“安全区域”（即对抗鲁棒性认证）。然而，当输入移出该区域时，模型的预测一定会改变吗？这一互补性问题——即完备认证（complete certification）——在文献中尚属空白。本文从理论上将对抗鲁棒性问题归结为一种格子遍历问题（lattice traversal problem），并在此基础上发展出同时支持安全认证（sound certification）和完备认证的通用框架，揭示了二者在计算复杂度上的不对称性。

核心内容

本文考虑多层感知机（MLP）分类器。对于一个输入点 (\mathbf{x})，一个轴对齐超矩形（即区间）(I) 称为安全认证（sound certification），如果 (\mathbf{x} \in I) 且 (\mathbf{x}) 可以在 (I) 内任意扰动而不改变 MLP 的预测。对称地，一个区间 (I) 称为完备认证（complete certification），如果 (\mathbf{x} \in I) 且当 (\mathbf{x}) 移出 (I) 时，MLP 的预测必定改变。安全认证问题对应着经典的对抗鲁棒性研究；而完备认证问题此前未被系统研究过。

作者将整个问题重构为格子遍历（lattice traversal）问题。每个格子元素对应一个区间（轴对齐超矩形），这些区间构成一个有序结构。通过定义格子遍历算子，作者提出了一种迭代 refine & verify（精炼与验证）方案：使用形式化 MLP 验证器（formal verifier）来保证安全认证的最大性（maximality）和完备认证的最小性（minimality）。

在优化目标方面，论文发现了有趣的不对称性：

• 对于完备认证，可以通过多项式次数的 oracle 调用获得最小解（即最小完备区间）。
• 对于安全认证，作者证明了强难解性（strong intractability），即不存在多项式时间的精确算法（除非某些复杂性类崩溃）。
• 此外，在对称区间（即 (\ell_\infty)-球）上，两种认证的优化问题都可以通过对数时间复杂度的算法求解。

最后，论文提供了经验评估，使用了新开发的系统 ParallelepipedoNN。该系统基于上述格子遍历方法，能够同时输出安全认证与完备认证，并展示其在实际 MLP 模型上的效果。

关键要点

• 首次将对抗鲁棒性（安全认证）与“离开区域后预测必变”（完备认证）统一为格子遍历问题。
• 定义了基于区间的两类认证的数学形式：安全认证保证区域内无错误，完备认证保证区域边界外预测必然变化。
• 提出 refine & verify 迭代算法，利用形式化验证器保证区域的最大性/最小性。
• 发现计算复杂度上的不对称性：
  • 完备认证的最小解可通过多项式次数的 oracle 调用获得。
  • 安全认证的最大解问题是强难解的（除非 (\text{P} = \text{NP}) 或更坏情况）。
  • 在 (\ell_\infty)-球（对称区间）上，两种问题均存在对数时间算法。
• 开发了 ParallelepipedoNN 系统，用于经验验证格子遍历方法的有效性。

意义与影响

本文从理论层面为 AI 安全中的对抗鲁棒性提供了更完备的视角。传统研究只关心“输入在多大范围内安全”，而本文引入的完备认证回答了另一个关键问题：“输入需要扰动多远才能改变预测？” 这种双向认证对于安全关键应用（如自动驾驶、医疗诊断）具有直接价值——不仅要知道安全边界，还要知道危险边界。

格子遍历框架巧妙地将区间搜索问题转化为有序结构上的遍历问题，为形式化验证提供了新的抽象工具。复杂度不对称性的发现提醒研究者：安全认证的精确最大化本质上比完备认证的最小化更难，这有助于指引算法设计（例如，对安全认证采用近似方法，而对完备认证追求精确解）。

此外，(\ell_\infty)-球上的对数时间算法使得在常见扰动模型（如 (\ell_\infty)-范数攻击）下的高效认证成为可能。ParallelepipedoNN 系统的实现表明该理论可以付诸实践，为未来构建兼具安全性与可解释性的神经网络认证工具奠定了基础。