用于单应性形式验证的Lipschitz优化

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