用于单应性矩阵形式验证的利普希茨优化

Lipschitz Optimization for Formal Verification of Homographies

在受监管行业中采用视觉神经网络需要形式化的鲁棒性保证，尤其是在医疗健康、自动驾驶和航空航天等安全关键领域。然而，当前方法局限于对$\ell_p$-范数和仿射变换的不完全统计验证或鲁棒性，这些仅覆盖了图像形成过程中极窄的扰动子集。特别是，尽管对相机运动的鲁棒性是部署众多视觉应用的关键，但其仍是一个悬而未决的问题。我们提出了一种针对拍摄相机3D运动扰动的形式化验证方法。首先，我们建立了从相机位姿到像素值的闭式映射。通过分析由此产生的单应矩阵的连续性特征，我们证明了近期关于Lipschitz优化和分段连续性的工作可被扩展，以推导出扰动像素值上的紧致线性界。我们的方法适用于以平面结构为主的场景，如增强现实中的地面、自动驾驶中的道路标线和交通标志，或机器人操作中的平面工作空间。这实现了投影几何变换的首个形式化验证，无需复杂仿真、替代网络或显式图像形成模型。我们验证了实现方案，并展示了相比先前工作高达89%的加速比和7%的更紧致边界。随后，我们在VNN-COMP基准上评估了该方法，揭示了其对投影扰动存在的系统性弱点。最后，我们针对一个安全关键的跑道分类器进行了真实世界案例研究，凸显了相机运动带来的实际漏洞，并解决了已学习模型认证中的关键挑战。数据和代码已公开于https://github.com/jeangud/homography-verification。