arXiv:2605.23203cs.CVcs.AI2026-05

首次实现对相机运动导致的图像投影变换的严格验证,提升安全关键场景的可信度。

Lipschitz Optimization for Formal Verification of Homographies

论文配图:Lipschitz Optimization for Formal Verification of Homographies
图 1 · 摘自论文原文
  • 基于相机位姿与像素值的闭式映射,利用Lipschitz优化推导紧致线性边界
  • 在VNN-COMP基准上发现系统性漏洞,速度比之前快89%,边界更紧7%
  • 适用于平面场景,无需仿真或图像形成模型,适合自动驾驶等应用

视觉神经网络在医疗、自动驾驶和航空航天等受监管领域部署需形式化鲁棒性保障。现有方法仅覆盖ℓ_p范数和仿射变换等有限扰动,难以应对相机运动这一关键挑战。本文提出针对3D相机运动扰动的形式化验证方法,建立相机姿态到像素值的闭式映射,通过分析同调变换的连续性,将最新Lipschitz优化与分段连续性理论扩展至扰动像素值的紧致线性界。该方法适用于以地面平面、道路标记或机器人操作平面为主的场景。无需复杂仿真、代理网络或显式图像形成模型,首次实现对投影几何变换的形式化验证。在实际实现中,相较先前工作最高提速89%、边界收紧7%。在VNN-COMP基准测试中揭示了对投影扰动的系统性弱点。进一步通过跑道分类器案例研究,暴露了学习模型在真实场景下因相机运动引发的安全隐患,解决了模型认证的关键难题。数据与代码公开于https://github.com/jeangud/homography-verification。

原文摘要 · Abstract (English)

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 $\ell_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. We validate our implementation and show up to 89% speedup and 7% tighter bounds over prior work. We then 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, highlighting practical vulnerabilities to camera motion, and addressing a key challenge in the certification of learned models. Data and code are publicly available at https://github.com/jeangud/homography-verification .

形式验证图像变换自动驾驶鲁棒性

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。