技术摘要：用于完整神经网络验证的分层端到端泰勒界

问题陈述

本文解决了神经网络可达性分析的挑战，具体任务是在给定的输入域上计算或紧密界定神经网络可获得的输出集合。该问题对于认证学习驱动的物理系统（如自动驾驶和医疗诊断）的安全性和鲁棒性至关重要。

虽然对于非凸函数而言，精确的可达集计算通常是不可处理的，但现有方法依赖于可处理的过近似。作者观察到，当前针对平滑、二次可微网络（例如使用 tanh 或 sigmoid 激活函数的网络）的最先进方法通常最多利用二阶信息（梯度和 Hessian 矩阵），但未能系统地利用高阶平滑性（具体而言，Hessian 矩阵的 Lipschitz 连续性）来控制近似误差。目标是推导函数 $f(x)$ 在有界输入集 $X$ 上的最大值更紧的、可证明的上界，其形式化为：
$$\max_{x \in X} f(x)$$
其中 $X$ 通常是 $\ell_2$ 或 $\ell_\infty$ 球。

方法论：HITAB 框架

作者提出了HITAB（分层端到端泰勒界），这是一个验证框架，它基于零阶、一阶和二阶局部信息构建上界层级，并辅以 Hessian 矩阵的 Lipschitz 常数（$L_{\nabla^2 f}$）。

1. 泰勒界层级

该框架定义了一系列主函数 $\bar{f}$，用于在标称点 $x_c$ 附近界定函数 $f(x_c + \delta)$：

• 零阶： 使用函数值 $f(x_c)$ 和全局 Lipschitz 常数 $L_f$。该界关于扰动大小 $\epsilon$ 是线性的。
• 一阶： 结合梯度 $\nabla f(x_c)$ 和梯度 Lipschitz 常数 $L_{\nabla f}$。这产生了一个二次余项界。
• 二阶（核心贡献）： 结合 Hessian 矩阵 $\nabla^2 f(x_c)$ 和Hessian Lipschitz 常数 $L_{\nabla^2 f}$。这导致了一个带有可证明的三次余项项的二阶泰勒模型：
  $$f(x_c + \delta) \leq f(x_c) + \nabla f(x_c)^\top \delta + \frac{1}{2}\delta^\top \nabla^2 f(x_c) \delta + \frac{1}{6}L_{\nabla^2 f}\|\delta\|_2^3$$
  与低阶界不同，在欧几里得球上最大化这个二阶主函数通常是非凸且不可处理的。作者提出了一种“分割 - 界定”（Split-and-Bound）松弛方法，以推导出封闭形式的、计算上可处理的上界。

2. Hessian Lipschitz 常数的组合估计

一个关键的技术障碍是计算深度神经网络的 $L_{\nabla^2 f}$。作者开发了一种逐层传播过程（定理 5）来界定该常数。

• 他们为层映射 $F^I(x) = \sigma(W^I x + b^I)$ 的 Hessian Lipschitz 常数定义了一个递归组合规则。
• 该界取决于激活函数 $\sigma$ 及其导数的 Lipschitz 常数（$L_\sigma, L_{\sigma'}, L_{\sigma''}$），以及网络权重和先前计算出的层输出及其梯度的 Lipschitz 常数。
• 这使得能够从输入层到输出层高效、模块化地计算 $L_{\nabla^2 f}$。

3. 与分支 - 界定（BaB）的集成

为了实现完整验证，HITAB 界被集成到一个**分支 - 界定（BaB）**流程中。

• 该算法迭代地划分输入域。
• 在每个节点处，计算分层界 $\bar{f}_m$（零阶、一阶和二阶证书的最小值）。
• 该过程持续进行，直到上界和下界之间的差距低于规定的容差。
• 该框架支持 $\ell_2$ 和 $\ell_\infty$ 约束输入集，并利用范数关系针对 $\ell_\infty$ 盒子进行了特定调整。

主要贡献

1. 组合 Hessian Lipschitz 界： 一种新颖、高效的算法，通过逐层传播曲率界来界定深度前馈网络中的 $L_{\nabla^2 f}$。
2. 端到端二阶泰勒模型： 一个带有三次余项项的可证明局部上界，利用了 Hessian 矩阵的 Lipschitz 连续性。
3. 统一的界层级： 一个统一了零阶、一阶和二阶界的框架，提供了精确的条件（扰动大小 $\epsilon$ 的阈值），在这些条件下，高阶近似可证明比低阶近似产生更紧的证书。
4. 实际验证流程： 将这些界集成到用于平滑神经网络的完整 BaB 验证器（算法 1）中。

实验结果

作者在6D 四旋翼飞行器控制基准上评估了 HITAB，其中神经网络控制器（训练用于模仿模型预测控制器）在避开障碍物的同时引导系统。该任务涉及在 $\ell_\infty$ 有界状态扰动下计算 10 个时间步长的可达集。

• 比较： 将 HITAB 与最先进的局部一阶界方法（Sharifi 和 Fazlyab, 2024）进行了比较。
• 性能：
  • HITAB 显著减少了 BaB 算法所需的分支数量（例如，在 $10^{-2}$ 容差下，约 11.9 万个分支对比约 90.8 万个分支）。
  • 这种减少转化为更快的运行时间（例如，在 $10^{-2}$ 容差下，约 108 秒对比约 320 秒）。
• 观察： 二阶信息提供了更紧的局部近似，特别是在分支过程中生成的较小子域上，从而实现了更高效的收敛。

意义与主张

本文声称提出了首个实用的平滑神经网络可达性分析框架，该系统性地利用了曲率（Hessian 矩阵）的 Lipschitz 连续性。

• 更紧的证书： 通过超越一阶（梯度）或标准二阶（Hessian 矩阵）近似，转而包含 Hessian 矩阵的平滑性，HITAB 产生了更紧的安全证书。
• 系统性改进： 该工作阐明了高阶信息有益的机制，表明三次余项项允许在微小扰动区域中显著减少保守性。
• 完整性： 与许多现有的针对平滑网络的不完整（启发式）方法不同，HITAB 被设计为嵌入到完整验证流程中，确保验证过程在给定足够时间的情况下可以收敛到精确答案。

作者承认了局限性，指出当前的实现是基于 CPU 的，并且针对二阶最大化问题（超越分割 - 界定封闭形式）的更紧数值松弛仍是未来工作的方向。然而，他们断言当前的封闭形式方法在紧密性和计算成本之间提供了有利的权衡。