Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2605.23203

Lipschitz Optimization for Formal Verification of Homographies

Jean-Guillaume Durand·Panagiotis Kouvaros·Maxime Gariel·Alessio Lomuscio
View original source ↗Read source document ↗Export metadata ↓

Abstract

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 .

Explore related subjects

cs.CVcs.AIcs.LGcs.RO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jean-Guillaume Durand, Panagiotis Kouvaros, Maxime Gariel, Alessio Lomuscio. 2026-05-22. Lipschitz Optimization for Formal Verification of Homographies. https://arxiv.org/abs/2605.23203

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Lifelong Learning of Video Diffusion Models From a Single Video Stream

Video diffusion models can enable embodied agents to anticipate plausible futures from the recent past, but they are typically trained offline on curated datasets--a mismatch with the agents' learning setup at deployment: online, from a single video stream that sequentially outputs one frame at a time. We bridge this training gap and demonstrate that training autoregressive video diffusion models from such a stream, resembling the experience of embodied agents, is not only possible but can also perform comparably to standard offline training given the same number of gradient steps. We find that this robustness to video stream autocorrelation and nonstationarity can be achieved using experience replay methods that retain a subset of the video stream. To support training and evaluation in this setting, we introduce five new datasets for streaming lifelong generative video modeling: Lifelong Bouncing Balls (O), Lifelong Bouncing Balls (C), Lifelong 3D Maze, Lifelong Drive, and Lifelong PLAICraft, each consisting of one million consecutive frames from environments of increasing complexity. Together, our datasets and experiments lay the groundwork for video generative models and world models that continuously learn from single-sensor video streams rather than fixed datasets.

cs.CV↗
arXiv2026

Bayesian Fusion of Active Contour Models and ConvNet Priors for Standing Dead Tree Segmentation

Instance segmentation is a core computer vision task with great practical significance. Recent advances, driven by large-scale benchmark datasets, have yielded good general-purpose Convolutional Neural Network (CNN)-based methods. Natural Resource Monitoring (NRM) utilizes remote sensing imagery with generally known scale and containing multiple overlapping instances of the same class, wherein the object contours are jagged and highly irregular. This is in stark contrast with the regular man-made objects found in classic benchmark datasets. We address this problem and propose a novel instance segmentation method geared towards NRM imagery. We formulate the problem as Bayesian maximum a posteriori inference which, in learning the individual object contours, incorporates shape, location, and position priors from state-of-the-art CNN architectures, driving a simultaneous level-set evolution of multiple object contours. We employ loose coupling between the CNNs that supply the priors and the active contour process, allowing a drop-in replacement of new network architectures. Moreover, we introduce a novel prior for contour shape, namely, a class of Deep Shape Models based on architectures from Generative Adversarial Networks (GANs). These Deep Shape Models are in essence a non-linear generalization of the classic Eigenshape formulation. In experiments, we tackle the challenging, real-world problem of segmenting individual dead tree crowns and delineating precise contours. We compare our method to two leading general-purpose instance segmentation methods - Mask R-CNN and K-net - on color infrared aerial imagery. Results show our approach to significantly outperform both methods in terms of reconstruction quality of tree crown contours. Furthermore, use of the GAN-based deep shape model prior yields significant improvement of all results over the vanilla Eigenshape prior.

cs.CV↗
arXiv2026

Sonicmesh: Enhancing 3D Human Mesh Reconstruction in Vision-Impaired Environments With Acoustic Signals

3D human mesh reconstruction (HMR) from RGB images often degrades under poor illumination, occlusion, and non-line-of-sight conditions. Acoustic sensing provides complementary spatial cues but suffers from low spatial resolution. We propose SonicMesh, which, to the best of our knowledge, is the first acoustic--visual framework for robust 3D human mesh reconstruction. SonicMesh first converts ultrasonic echoes into range--azimuth acoustic images through an Inverse Synthetic Aperture Radar (ISAR)-based imaging process. It then introduces a cross-dimensional anatomical registration module that maps modality-specific 2D joint features into a common canonical 3D human space. The registered anatomical representations are further integrated with acoustic and visual features through a two-stage fusion network for final mesh reconstruction. Experiments demonstrate that SonicMesh achieves accurate and robust 3D human reconstruction across normal, poor-light, occluded, and non-line-of-sight environments, consistently outperforming existing RGB-, radio-frequency (RF)-, and mmWave-based approaches under challenging sensing conditions.

cs.CV↗