论文技术总结：基于哈密顿 - 雅可比可达性分析的感知不确定性下控制器鲁棒验证 (RoVer-CoRe)

1. 研究背景与问题定义 (Problem)

随着基于感知的自主系统控制器（通常由神经网络实现）在现实世界中的普及，如何在感知不确定性（Perceptual Uncertainty）存在的情况下，形式化地验证系统的安全性和性能，成为一个关键挑战。

• 感知不确定性的来源：传感器固有噪声、基于学习的模块中的训练误差、以及环境因素（如隧道遮挡 GPS 信号）。
• 现有方法的局限性：
  • 现有的验证方法多结合神经网络验证工具与近似可达集方法（如超矩形、多面体、Zonotope 等）。
  • 这些方法通常高度依赖于传播工具的保守性，导致分析结果过于保守，无法通过安全认证（即误报率高，将安全系统判定为不安全）。
  • 许多方法限制了可处理的控制器或系统类别（如要求线性或凸性）。
• 核心问题：如何为具有非线性、非凸、黑盒（如神经网络）特性的感知控制器，在 worst-case（最坏情况）感知误差下，提供非保守的、形式化的安全保证？

2. 方法论 (Methodology)

作者提出了 RoVer-CoRe (Robust Verification of Controllers via HJ Reachability)，这是首个基于哈密顿 - 雅可比 (HJ) 可达性分析的框架，用于验证感知不确定性下的系统。

2.1 核心洞察：闭环系统抽象

传统的 HJ 可达性分析假设控制器拥有完美的状态信息。为了处理感知不确定性，RoVer-CoRe 提出了一个关键的闭环系统抽象：

• 将控制器 ($\pi$)、观测函数 ($p$) 和状态估计模块 ($q$) 串联，形成一个等效的闭环动力学系统：
  $$h(x, d, e) := f(x, \pi(q(p(x), e)), d)$$
• 在此抽象中，外部输入仅为干扰信号 $d$ 和感知误差信号 $e$。
• 这种抽象使得原本复杂的感知 - 控制回路可以直接适配现有的 HJ 可达性工具。

2.2 核心挑战：闭环哈密顿量的计算

在 HJ 框架中，安全性的核心在于计算哈密顿量 (Hamiltonian)。对于感知系统，哈密顿量变为：
$$H(x, t, \nabla V) = \min_{d \in D, e \in E} \nabla V(x, t) \cdot h(x, d, e)$$
由于控制器 $\pi$、观测 $p$ 和估计器 $q$ 的复杂性，该优化问题通常是非凸的，难以直接求解。RoVer-CoRe 提出了两种解决方案：

1. 精确计算 (Exact Computation)：
   • 适用于结构简单或可枚举的控制器（如网格上的 MPC 或简单的线性反馈）。
   • 直接求解优化问题，无保守性，并能生成具体的最坏情况反例。
2. 下界估计 (Lower Bounding)：
   • 适用于复杂控制器（如神经网络）。
   • 假设状态估计是真实状态的有界加性扰动 ($\hat{x} = x + e$)。
   • 利用神经网络验证工具（如 $\alpha,\beta$-CROWN）或网格枚举，计算控制器输出在感知误差下的上下界 ($\underline{U}(x), \overline{U}(x)$)。
   • 将原问题转化为在控制输入空间 $U(x)$ 上的优化问题，从而得到哈密顿量的下界。
   • 性质：虽然引入了保守性（因为使用了控制输出的超矩形包络），但保证了安全性 (Soundness)，即如果验证通过，系统绝对安全。

2.3 鲁棒控制器设计

除了验证，该框架还支持基于安全引导的超参数优化。通过计算不同超参数配置下的鲁棒值函数，可以自动选择能最大化安全裕度或安全集体积的参数，从而设计更鲁棒的控制器。

3. 主要贡献 (Key Contributions)

1. RoVer-CoRe 框架：首个基于 HJ 可达性分析验证感知不确定性下系统的框架。
2. 形式化验证与鲁棒设计方法：提出了针对闭环哈密顿量的精确计算与保守下界估计方法，实现了在感知误差下的形式化安全验证及鲁棒控制器设计。
3. 实证有效性：通过飞机滑行和基于神经网络的月球车导航两个案例研究，证明了该方法的有效性，并开源了代码。
4. 超越现有工具：相比基于集合传播的验证工具（如 NNV 2.0），RoVer-CoRe 提供了更紧确（less conservative）的安全保证。

4. 实验结果 (Results)

论文通过两个案例研究验证了框架：

4.1 案例一：飞机滑行 (Aircraft Taxiing)

• 场景：飞机使用机翼摄像头和 DNN 预测横向和航向误差，进行车道保持。
• 验证：在 99.68% 的感知误差覆盖率下，成功形式化验证了初始状态的安全性。
• 设计：通过扫描控制器超参数空间，找到了比原始设计更鲁棒的参数组合（原始设计在特定误差下不安全，而优化后的设计在蓝色安全区域内）。
• 诊断：成功识别了导致不安全的具体失败模式（如过大的横向增益导致过度修正）。

4.2 案例二：基于神经网络的月球车导航 (NN-Based Rover Navigation)

• 场景：月球车在低光照下使用视觉里程计，误差随时间线性增长。需决定何时开启车灯以重置误差（权衡能耗与安全）。
• 对比：
  • MPC vs. NN：RoVer-CoRe 计算出的 NN 控制器可达集（BRT）比 MPC 更“膨胀”，反映了模仿误差和 NN 验证界的松弛性，但保证了安全性。
  • vs. 蒙特卡洛 (Monte Carlo)：RoVer-CoRe 识别出的不安全状态远多于蒙特卡洛采样（后者漏掉了许多危险状态），证明了其完备性。
  • vs. NNV 2.0：附录显示 RoVer-CoRe 提供的安全边界比 NNV 2.0 更紧确（保守性更低）。
• 应用：利用验证结果设计了车灯激活策略。该策略仅在感知不确定性累积到可能危及安全时才开启车灯，既保证了形式化安全，又显著减少了不必要的能耗。

5. 意义与总结 (Significance)

• 理论突破：解决了将 HJ 可达性分析应用于感知不确定性系统的难题，通过闭环抽象和哈密顿量处理，填补了该领域的空白。
• 实用价值：
  • 更高的安全性：相比传统近似方法，提供了更紧确的安全边界，减少了误报。
  • 可解释性：能够生成具体的最坏情况轨迹（反例），帮助工程师理解系统为何失败。
  • 设计辅助：不仅用于验证，还能直接指导鲁棒控制器的参数优化和策略设计（如能耗管理）。
• 未来方向：包括引入概率不确定性模型、利用基于学习的可达性工具提高可扩展性，以及扩展到更复杂的感知管道。

总结：RoVer-CoRe 为自主系统在充满感知噪声的复杂环境中的安全部署提供了一套强有力的形式化验证与设计工具，特别是在处理非线性、黑盒控制器方面展现了显著优势。