面向单应变换形式化验证的 Lipschitz 优化
Lipschitz Optimization for Formal Verification of Homographies
为视觉模型提供针对相机 3D 运动（单应变换）扰动的形式化鲁棒性验证手段：通过相机位姿到像素值的闭式映射与单应变换的分段连续性，推导扰动像素值的紧致线性界，可直接用于验证 AR 地平面、自动驾驶路面标线与交通标志、机器人平面工作区等平面主导场景下的分类器。
原文依据 This enables the first formal verification of projective geometry transforms, without complex simulation, surrogate networks, or explicit image-formation models.
摘要译文
由模型翻译 · 术语统一 · 请对照原文核对关键结论在受监管行业（尤其是医疗、自动驾驶和航空航天等安全关键领域）中采用视觉神经网络，需要形式化的鲁棒性保证。然而，现有方法局限于不完整的统计验证，或仅针对 p-范数与仿射变换的鲁棒性，这些只覆盖了成像过程扰动中很小的一部分。特别是，对相机运动的鲁棒性尽管对部署许多视觉应用至关重要，却仍是一个未解决的问题。我们提出一种形式化验证方法，针对拍摄相机的 3D 运动扰动实现鲁棒性验证。我们首先建立从相机位姿到像素值的闭式映射。通过分析所得单应变换的连续性性质，我们表明，近期关于 Lipschitz 优化与分段连续性的工作可以被扩展，从而为受扰动的像素值推导出紧致的线性界。我们的方法适用于以平面结构为主的场景，例如增强现实中的地平面、自动驾驶中的道路标线与交通标志，或机器人操作中的平面工作区。这使得首次对投影几何变换进行形式化验证成为可能，且无需复杂仿真、代理网络或显式成像模型。我们的实现相比先前工作最高取得 89% 的加速和 7% 更紧的界。我们在 VNN-COMP 基准上评估了该方法，并揭示了模型对投影扰动的系统性弱点。最后，我们在一项针对安全关键的跑道分类器的真实案例研究中进行了演示，解决了学习模型认证中的一个关键挑战。数据与代码见 https://github.com/jeangud/homography-verification。
英文原文摘要 1751 字符
The adoption of vision neural networks in regulated industries requires formal robustness guarantees, especially in safety-critical domains such as healthcare, autonomous vehicles, and aerospace. However, current approaches are confined to incomplete statistical verification or robustness to p-norm and affine transforms, which cover only a narrow subset of perturbations to the image formation process. In particular, robustness to camera motion remains an open problem despite being key to deploy many vision applications. We present a formal verification approach that targets robustness against 3D motion perturbations of the capturing camera. We first establish a closed-form mapping from camera pose to pixel values. By analyzing the continuity properties of the resulting homographies, we show that recent work on Lipschitz optimization and piecewise continuity can be extended to derive tight linear bounds on perturbed pixel values. Our approach applies to scenes with predominantly planar structure, such as ground planes in augmented reality, road markings and traffic signs in autonomous driving, or planar workspaces in robotic manipulation. This enables the first formal verification of projective geometry transforms, without complex simulation, surrogate networks, or explicit image-formation models. Our implementation achieves up to 89% speedup and 7% tighter bounds over prior work. We evaluate our method on the VNN-COMP benchmark and reveal systematic weaknesses to projective perturbations. Finally, we demonstrate a real-world case study on a safety-critical runway classifier, addressing a key challenge in the certification of learned models. Data and code are available at https://github.com/jeangud/homography-verification.