pith. sign in

arxiv: 2605.23203 · v1 · pith:PDF6AJCVnew · submitted 2026-05-22 · 💻 cs.CV · cs.AI· cs.LG· cs.RO

Lipschitz Optimization for Formal Verification of Homographies

Jean-Guillaume Durand , Panagiotis Kouvaros , Maxime Gariel , Alessio Lomuscio This is my paper

Pith reviewed 2026-05-25 04:55 UTC · model grok-4.3

classification 💻 cs.CV cs.AIcs.LGcs.RO
keywords formal verificationhomographyLipschitz optimizationrobustnesscamera motionprojective geometryneural networksplanar scenes
0
0 comments X

The pith

A closed-form homography mapping from camera pose to pixels allows Lipschitz optimization to produce tight linear bounds for verifying neural network robustness to 3D motion.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a formal verification method for neural networks that checks robustness to camera motion perturbations in 3D. It derives a closed-form mapping via homographies for planar scenes, then extends recent Lipschitz optimization techniques to the continuity properties of these transforms to bound pixel value changes. This produces the first formal guarantees on projective geometry transforms without relying on simulation or surrogate models. The approach targets applications like autonomous driving and runway classification where camera motion is a realistic threat. Validation shows faster and tighter bounds than prior methods while exposing systematic weaknesses on standard benchmarks.

Core claim

By establishing a closed-form mapping from camera pose to pixel values through homographies and analyzing their continuity properties, recent Lipschitz optimization and piecewise continuity results can be extended to derive tight linear bounds on perturbed pixel values, enabling formal verification of robustness against 3D motion perturbations for scenes with predominantly planar structure.

What carries the argument

Closed-form homography mapping from camera pose to pixel values, extended via its continuity properties to support Lipschitz optimization for linear bounds on perturbations.

If this is right

  • Formal verification becomes possible for projective geometry transforms without complex simulation or explicit image-formation models.
  • The method yields up to 89 percent speedup and 7 percent tighter bounds compared with prior work.
  • Evaluation on the VNN-COMP benchmark reveals systematic weaknesses of networks to projective perturbations.
  • A real-world runway classifier case study demonstrates practical vulnerabilities to camera motion.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same continuity analysis could be tested on other geometric transforms such as affine or perspective mappings beyond homographies.
  • Integration with existing neural network verifiers might allow combined checks for both lp-norm and motion perturbations.
  • The bounds could serve as a basis for generating adversarial camera poses in training loops for improved robustness.

Load-bearing premise

Scenes have predominantly planar structure so that homographies provide an accurate closed-form mapping from camera pose to pixel values.

What would settle it

A concrete counterexample in which actual pixel changes under small camera pose perturbations exceed the derived linear bounds for a planar scene.

Figures

Figures reproduced from arXiv: 2605.23203 by Alessio Lomuscio, Jean-Guillaume Durand, Maxime Gariel, Panagiotis Kouvaros.

Figure 1
Figure 1. Figure 1: Example application: autonomous driving. The scene geometry defines the coordinate transform T R C ∈ SE(3) from road frame (R) to camera frame (C). Assuming a planar traffic sign and a pinhole camera model, the stop sign features (blue points) are projected from the 3D world to the 2D image plane through projective geometry. Such a plane-to-plane mapping is a homography. We then study the robustness of tra… view at source ↗
Figure 2
Figure 2. Figure 2: The space of image perturbations (notional). Most vectors in [0, 1]h×w are noise (a). The subset of natural images forms a complex manifold of lower dimension (grey surface), on which lies our original image x0. The ball Bp(x0, ε) of ℓp-norm perturbations (blue) can capture noise (b), hue (c) and brightness (d) variations for example. Beyond Bp(x0, ε) and along con￾strained walks on the manifold, we may fo… view at source ↗
Figure 3
Figure 3. Figure 3: Pixel values under perspective transform. As original image x0 (b) undergoes a yaw angle perturbation κ ∈ B = [0◦ , 10◦ ], we look at the values G x0 34,47(κ) of pixel p = (34, 47), the red square in transformed image (a). Transform T is a homography and, as non-affine, is able to represent a change of perspective of the traffic sign. Applying the inverse transform, we find the corresponding position T −1 … view at source ↗
Figure 4
Figure 4. Figure 4: Lipschitz optimization. Adapted from [7], procedure 4a finds an ϵ-maximum of function J. On Fig. 4b, a few samples (black) approximate the true function (magenta). The Lipschitz property of J constrains, with slope ±L, possible values for the function (gray bands). In this example, since the maximum of the Lipschitz bound (black) is above Jmax + ϵ, the interval is split a few more times to better estimate … view at source ↗
Figure 5
Figure 5. Figure 5: Example bounds. Pixel values (magenta) are over￾approximated. Unsound bounds (dashed) are shifted to sound bounds (solid) by Lipschitz optimization. Depending on complex￾ity, curves have zero (linear), one (PWL [7]), or two splits (ours). that are similar between datasets (see supplementary mate￾rial Sec. 10). Additionally, we use a runway visibility clas￾sifier developed on the LARD dataset [14]. Verifica… view at source ↗
Figure 6
Figure 6. Figure 6: Sample images from each dataset. 9. Padding Geometric transformations frequently map target coordinates beyond the boundaries of the source image. In this case, bilinear interpolation relies on padding mechanisms to impute missing pixel values. Depending on the application, different padding 1 [PITH_FULL_IMAGE:figures/full_fig_p011_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Overview of different padding techniques. [PITH_FULL_IMAGE:figures/full_fig_p012_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Samples for a roll perturbation, with κ = ∆ϕ ∈ B = [0, 15]◦ We notice that under our assumptions, the roll perturbation is an affine transform and corresponds exactly to a 2D rotation of the image. It is also independent of the camera focal length f. H−1 (∆ϕ) =   cos (∆ϕ) − sin (∆ϕ) −xc cos (∆ϕ) + xc + yc sin (∆ϕ) sin (∆ϕ) cos (∆ϕ) −xc sin (∆ϕ) − yc cos (∆ϕ) + yc 0 0 1   (15)  u0(∆ϕ), v0(∆ϕ)  =  xc … view at source ↗
Figure 9
Figure 9. Figure 9: Samples for a pitch perturbation, with κ = ∆θ ∈ B = [0, 15]◦ H−1 (∆θ) =     1 xc sin (∆θ) f xc(f cos (∆θ)−f−yc sin (∆θ)) f 0 cos(∆θ) + yc sin(∆θ) f − (f 2+y 2 c ) sin (∆θ) f 0 sin (∆θ) f cos (∆θ) − yc sin (∆θ) f     (20)  u0(∆θ), v0(∆θ)  =  xc + f · u−xc f cos(∆θ)+(v−yc) sin(∆θ) , yc − f · f sin(∆θ)−(v−yc) cos(∆θ) f cos(∆θ)+(v−yc) sin(∆θ)  (21) ∇⊤ ∆θT −1 (∆θ) =  − f(u−xc)[−f sin(∆θ)+(v−yc) cos… view at source ↗
Figure 10
Figure 10. Figure 10: Samples for a yaw perturbation, with κ = ∆ψ ∈ B = [0, 15]◦ H−1 (∆ψ) =     cos (∆ψ) − xc sin (∆ψ) f 0 (f 2+x 2 c) sin (∆ψ) f − yc sin (∆ψ) f 1 yc(f(cos (∆ψ)−1)+xc sin (∆ψ)) f − sin (∆ψ) f 0 cos (∆ψ) + xc sin (∆ψ) f     (25)  u0(∆ψ), v0(∆ψ)  =  xc + f · f sin(∆ψ)+(u−xc) cos(∆ψ) f cos(∆ψ)−(u−xc) sin(∆ψ) , yc + f · v−yc f cos(∆ψ)−(u−xc) sin(∆ψ)  (26) ∇⊤ ∆ψT −1 (∆ψ) =  f[f 2+(u−xc) 2 ] [f cos (∆ψ)… view at source ↗
Figure 11
Figure 11. Figure 11: Samples for a x-translation perturbation, with κ = ∆x ∈ B = [0, 1]m 3 [PITH_FULL_IMAGE:figures/full_fig_p013_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Samples for a y-translation perturbation, with κ = ∆y ∈ B = [0, 1]m Since there is no orientation change between both viewpoints, we retrieve a simple shear along the camera x-axis: once again an affine transform. H−1 (∆y) =   1 − ∆y z ∆yyc z 0 1 0 0 0 1   with z ̸= 0 (i.e. camera not on ground plane) (35)  u0(∆y), v0(∆y)  =  u + ∆y  yc f − v z  , v (36) ∇⊤ ∆yT −1 (∆y) = yc f − v z , 0  (37) Di… view at source ↗
Figure 13
Figure 13. Figure 13: Samples for a z-translation perturbation, with κ = ∆z ∈ B = [0, 1]m 4 [PITH_FULL_IMAGE:figures/full_fig_p014_13.png] view at source ↗
read the original 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 .

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims to introduce the first formal verification method for neural network robustness under 3D camera motion perturbations on planar scenes. It derives a closed-form homography mapping from camera pose to pixel values, extends Lipschitz optimization using continuity properties to obtain tight linear bounds on perturbed pixels, and demonstrates the approach via implementation speedups, VNN-COMP evaluation revealing weaknesses to projective transforms, and a runway classifier case study.

Significance. If the central derivation holds, the result would be significant for safety-critical vision applications by providing sound bounds on projective transforms without simulation or surrogates. The public code release and real-world case study strengthen the contribution; reported gains of 89% speedup and 7% tighter bounds over prior work would indicate practical efficiency if substantiated.

major comments (2)
  1. [Abstract and §3] Abstract and §3 (bound derivation): the extension of Lipschitz optimization to homographies assumes the pose-to-pixel mapping is Lipschitz continuous over the perturbation domain. However, the projective division by the third homogeneous coordinate yields unbounded derivatives near singularities (grazing angles where the denominator approaches zero). The manuscript provides no explicit restriction of the perturbation set or proof that a finite Lipschitz constant exists on the chosen domain, which is load-bearing for the soundness of the linear bounds.
  2. [§5] §5 (VNN-COMP evaluation): the claim that the method reveals 'systematic weaknesses to projective perturbations' requires the specific perturbation ranges and network architectures used; without these, it is unclear whether the observed failures stem from the homography bounds or from the underlying Lipschitz optimizer.
minor comments (2)
  1. [§2] Notation for the homography matrix and pose parameters should be introduced with explicit definitions before the continuity analysis to improve readability.
  2. [Abstract] The abstract states 'up to 89% speedup and 7% tighter bounds' but does not specify the exact baseline implementations or the metric (e.g., bound width or verification time) used for the 7% figure.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive report. We address each major comment below and will revise the manuscript to strengthen the presentation and soundness arguments.

read point-by-point responses

  1. Referee: [Abstract and §3] Abstract and §3 (bound derivation): the extension of Lipschitz optimization to homographies assumes the pose-to-pixel mapping is Lipschitz continuous over the perturbation domain. However, the projective division by the third homogeneous coordinate yields unbounded derivatives near singularities (grazing angles where the denominator approaches zero). The manuscript provides no explicit restriction of the perturbation set or proof that a finite Lipschitz constant exists on the chosen domain, which is load-bearing for the soundness of the linear bounds.

    Authors: We agree that the Lipschitz property requires careful domain restriction. The manuscript analyzes continuity properties of homographies but does not explicitly bound the perturbation set away from singularities. We will revise §3 to add an explicit assumption that the perturbation domain is a compact set on which the third homogeneous coordinate is bounded below by a positive constant (ensuring no grazing angles), and we will include a short proof that the resulting mapping is Lipschitz continuous on this domain, with the constant obtained from the supremum of the Jacobian norm over the compact set. This restriction is consistent with the practical planar-scene scenarios considered in the paper. revision: yes

  2. Referee: [§5] §5 (VNN-COMP evaluation): the claim that the method reveals 'systematic weaknesses to projective perturbations' requires the specific perturbation ranges and network architectures used; without these, it is unclear whether the observed failures stem from the homography bounds or from the underlying Lipschitz optimizer.

    Authors: The specific perturbation ranges and network architectures are already stated in §5, but we acknowledge that they could be presented more prominently for clarity. We will revise §5 to include an explicit table or subsection listing the exact perturbation intervals (e.g., rotation and translation bounds), the VNN-COMP networks evaluated, and the precise failure criteria. This will make it unambiguous that the observed weaknesses arise from the inability of existing affine/ℓp methods to handle projective transforms rather than from the Lipschitz optimizer itself. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation extends prior methods independently.

full rationale

The abstract and description present the core contribution as an extension of existing Lipschitz optimization and piecewise continuity results to homographies via analysis of their continuity properties for planar scenes. No equations or steps are shown that reduce a claimed prediction or first-principles result to a fitted parameter or self-citation by construction. The approach is described as applying established techniques to a new domain without redefining inputs in terms of outputs or relying on load-bearing self-citations for uniqueness. This is the common case of a self-contained extension with independent mathematical content.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Review based on abstract only; no free parameters, invented entities, or detailed axioms are extractable. The core extension assumes standard properties of homographies and Lipschitz continuity.

axioms (1)
  • domain assumption Homographies exhibit continuity properties amenable to Lipschitz optimization and piecewise linear bounding.
    Invoked in abstract as the basis for deriving tight linear bounds on perturbed pixel values.

pith-pipeline@v0.9.0 · 5830 in / 1123 out tokens · 24362 ms · 2026-05-25T04:55:26.554347+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

69 extracted references · 69 canonical work pages · 4 internal anchors

  1. [1]

    Roadmap for artificial in- telligence safety assurance

    Federal Aviation Administration. Roadmap for artificial in- telligence safety assurance. Technical Report Version I, FAA, 2024. 31 pages. 7

    work page 2024

  2. [2]

    EASA concept pa- per: Guidance for level 1 & 2 machine-learning applications

    European Union Aviation Safety Agency. EASA concept pa- per: Guidance for level 1 & 2 machine-learning applications. Technical Report Issue 02, EASA, 2024. 7

    work page 2024

  3. [3]

    The sample complexities of global Lipschitz opti- mization

    Franc ¸ois Bachoc, Tommaso R Cesari, and S´ebastien Gerchi- novitz. The sample complexities of global Lipschitz opti- mization. hal-03129721v2, 2021. 4

    work page 2021

  4. [4]

    The sec- ond international verification of neural networks competition (VNN-COMP 2021): Summary and results.arXiv preprint arXiv:2109.00498, 2021

    Stanley Bak, Changliu Liu, and Taylor Johnson. The sec- ond international verification of neural networks competition (VNN-COMP 2021): Summary and results.arXiv preprint arXiv:2109.00498, 2021. 7

    work page arXiv 2021

  5. [5]

    Neural network based runway landing guidance for general aviation au- toland

    Giovanni Balduzzi, Martino Ferrari Bravo, Anna Chernova, Calin Cruceru, Luuk van Dijk, Peter de Lange, Juan Jerez, Nathana¨el Koehler, Mathias Koerner, Corentin Perret-Gentil, Zoltan Pillio, Ruben Polak, Hugo Silva, Romeo Valentin, Ian Whittington, and Grigory Yakushev. Neural network based runway landing guidance for general aviation au- toland. Technica...

    work page 2021

  6. [6]

    Certifying geometric ro- bustness of neural networks

    Mislav Balunovic, Maximilian Baader, Gagandeep Singh, Timon Gehr, and Martin Vechev. Certifying geometric ro- bustness of neural networks. InNeurIPS, 2019. 6, 8

    work page 2019

  7. [7]

    Verification of geometric robustness of neural networks via piecewise linear approx- imation and Lipschitz optimisation

    Ben Batten, Yang Zheng, Alessandro De Palma, Panagiotis Kouvaros, and Alessio Lomuscio. Verification of geometric robustness of neural networks via piecewise linear approx- imation and Lipschitz optimisation. InECAI, pages 2362– 2369, 2024. 2, 3, 4, 5, 6, 7, 8

    work page 2024

  8. [8]

    Efficient verification of ReLU- based neural networks via dependency analysis

    Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. Efficient verification of ReLU- based neural networks via dependency analysis. InAAAI Conference on Artificial Intelligence, 2020. 6, 8

    work page 2020

  9. [9]

    The fourth international verification of neural net- works competition (VNN-COMP 2023): Summary and re- sults

    Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T Johnson. The fourth international verification of neural net- works competition (VNN-COMP 2023): Summary and re- sults. InCAV, 2023. 2, 6, 7, 8

    work page 2023

  10. [10]

    The right (angled) perspective: Improving the understanding of road scenes using boosted inverse perspective mapping

    Tom Bruls, Horia Porav, Lars Kunze, and Paul Newman. The right (angled) perspective: Improving the understanding of road scenes using boosted inverse perspective mapping. 2019 IEEE Intelligent Vehicles Symposium (IV), pages 302– 309, 2018. 8

    work page 2019

  11. [11]

    Homography-based state estimation for autonomous UA V landing

    Andres Chavez, Dalton L’Heureux, Nirmit Prabhakar, Matthew Clark, Wai-Leuk Law, and Richard J Prazenica. Homography-based state estimation for autonomous UA V landing. InAIAA Information Systems-AIAA Infotech@ Aerospace, 2017. 8

    work page 2017

  12. [12]

    Real-time geometry-aware augmented reality in minimally invasive surgery.Healthcare technology letters, 4(5):163–167, 2017

    Long Chen, Wen Tang, and Nigel W John. Real-time geometry-aware augmented reality in minimally invasive surgery.Healthcare technology letters, 4(5):163–167, 2017. 8

    work page 2017

  13. [13]

    Po- sition: Beyond robustness against single attack types.arXiv preprint arXiv:2405.01349, 2024

    Sihui Dai, Chong Xiang, Tong Wu, and Prateek Mittal. Po- sition: Beyond robustness against single attack types.arXiv preprint arXiv:2405.01349, 2024. 8

    work page arXiv 2024

  14. [14]

    LARD - Landing Approach Runway Detection - Dataset for Vision Based Landing

    M ´elanie Ducoffe, Maxime Carrere, L ´eo F ´eliers, Adrien Gauffriau, Vincent Mussot, Claire Pagetti, and Thierry Sam- mour. LARD - Landing Approach Runway Detection - Dataset for Vision Based Landing. 2023. 2, 6, 7

    work page 2023

  15. [15]

    Robustness of Rotation-Equivariant Networks to Adversarial Perturbations

    Beranger Dumont, Simona Maggio, and Pablo Montalvo. Robustness of rotation-equivariant networks to adversarial perturbations.arXiv preprint arXiv:1802.06627, 2018. 8

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  16. [16]

    Exploring the landscape of spatial robustness

    Logan Engstrom, Brandon Tran, Dimitris Tsipras, Ludwig Schmidt, and Aleksander Madry. Exploring the landscape of spatial robustness. InICML, 2019. 2, 8

    work page 2019

  17. [17]

    The robustness of deep networks: A ge- ometrical perspective.IEEE Signal Processing Magazine, 34(6):50–62, 2017

    Alhussein Fawzi, Seyed-Mohsen Moosavi-Dezfooli, and Pascal Frossard. The robustness of deep networks: A ge- ometrical perspective.IEEE Signal Processing Magazine, 34(6):50–62, 2017. 8

    work page 2017

  18. [18]

    Fuzz testing based data augmentation to improve robustness of deep neural networks

    Xiang Gao, Ripon K Saha, Mukul R Prasad, and Abhik Roy- choudhury. Fuzz testing based data augmentation to improve robustness of deep neural networks. InICSE, pages 1147–

    work page

  19. [19]

    Explaining and harnessing adversarial examples

    Ian Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. InICLR,

    work page

  20. [20]

    Efficient verifica- tion of neural networks against LVM-based specifications

    Harleen Hanspal and Alessio Lomuscio. Efficient verifica- tion of neural networks against LVM-based specifications. InCVPR, pages 3894–3903. IEEE, 2023. 8

    work page 2023

  21. [21]

    Cambridge University Press,

    Richard Hartley and Andrew Zisserman.Multiple view ge- ometry in computer vision. Cambridge University Press,

    work page

  22. [22]

    Towards compositional adversarial robustness: Generalizing adversarial training to composite semantic perturbations

    Lei Hsiung, Yun-Yun Tsai, Pin-Yu Chen, and Tsung-Yi Ho. Towards compositional adversarial robustness: Generalizing adversarial training to composite semantic perturbations. In CVPR, pages 24658–24667, 2023. 8

    work page 2023

  23. [23]

    Robustness certification of visual perception models via camera motion smoothing

    Hanjiang Hu, Zuxin Liu, Linyi Li, Jiacheng Zhu, and Ding Zhao. Robustness certification of visual perception models via camera motion smoothing. InCoRL, pages 1309–1320. PMLR, 2022. 8

    work page 2022

  24. [24]

    Robustness ver- ification for perception models against camera motion per- turbations

    Hanjiang Hu, Changliu Liu, and Ding Zhao. Robustness ver- ification for perception models against camera motion per- turbations. InICML Workshop on Formal Verification of Ma- chine Learning (WFVML), 2023. 8

    work page 2023

  25. [25]

    Pixel-wise smoothing for certified robustness against camera motion perturbations

    Hanjiang Hu, Zuxin Liu, Linyi Li, Jiacheng Zhu, and Ding Zhao. Pixel-wise smoothing for certified robustness against camera motion perturbations. InAISTATS, pages 217–225. PMLR, 2024. 2, 8

    work page 2024

  26. [26]

    When deep learning meets polyhedral theory: A sur- vey.INFORMS Journal on Computing, 2026

    Joey Huchette, Gonzalo Mu ˜noz, Thiago Serra, and Calvin Tsay. When deep learning meets polyhedral theory: A sur- vey.INFORMS Journal on Computing, 2026. 8

    work page 2026

  27. [27]

    Towards Generalized Certified Robustness with Multi-Norm Training

    Enyi Jiang and Gagandeep Singh. Towards Universal Cer- tified Robustness with Multi-Norm Training.arXiv preprint arXiv:2410.03000, 2024. 8

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  28. [28]

    Geometric robustness of deep networks: analysis and improvement

    Can Kanbak, Seyed-Mohsen Moosavi-Dezfooli, and Pascal Frossard. Geometric robustness of deep networks: analysis and improvement. InCVPR, pages 4441–4449. IEEE, 2018. 8 9

    work page 2018

  29. [29]

    Reluplex: An efficient SMT solver for verifying deep neural networks

    Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. InCAV, pages 97–117. Springer, 2017. 8

    work page 2017

  30. [30]

    The 6th international verification of neural networks competition (VNN-COMP 2025): Summary and results.arXiv preprint arXiv:2512.19007, 2025

    Konstantin Kaulen, Tobias Ladner, Stanley Bak, Christopher Brix, Hai Duong, Thomas Flinkow, Taylor T Johnson, Lukas Koller, Edoardo Manino, ThanhVu H Nguyen, et al. The 6th international verification of neural networks competition (VNN-COMP 2025): Summary and results.arXiv preprint arXiv:2512.19007, 2025. 7

    work page arXiv 2025

  31. [31]

    Formal Verification of CNN-based Perception Systems

    Panagiotis Kouvaros and Alessio Lomuscio. Formal veri- fication of CNN-based perception systems.arXiv preprint arXiv:1811.11373, 2018. 8

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  32. [32]

    Deep learning.Nature, 521(7553):436–444, 2015

    Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. Deep learning.Nature, 521(7553):436–444, 2015. 2

    work page 2015

  33. [33]

    SoK: Certified robustness for deep neural networks

    Linyi Li, Tao Xie, and Bo Li. SoK: Certified robustness for deep neural networks. InIEEE Symposium on Security and Privacy, 2023. 2, 8

    work page 2023

  34. [34]

    Al- gorithms for verifying deep neural networks.Foundations and Trends in Optimization, 4(3-4):244–404, 2021

    Changliu Liu, Tomer Arnon, Christopher Lazarus, Christo- pher Strong, Clark Barrett, Mykel J Kochenderfer, et al. Al- gorithms for verifying deep neural networks.Foundations and Trends in Optimization, 4(3-4):244–404, 2021. 8

    work page 2021

  35. [35]

    Vision-centric BEV perception: A survey.IEEE TPAMI, 2024

    Yuexin Ma, Tai Wang, Xuyang Bai, Huitong Yang, Yuenan Hou, Yaming Wang, Yu Qiao, Ruigang Yang, and Xinge Zhu. Vision-centric BEV perception: A survey.IEEE TPAMI, 2024. 8

    work page 2024

  36. [36]

    Global optimization of Lipschitz functions

    C ´edric Malherbe and Nicolas Vayatis. Global optimization of Lipschitz functions. InICML, pages 2314–2323. PMLR,

    work page

  37. [37]

    Is certifyingℓ p robustness still worthwhile?arXiv preprint arXiv:2310.09361, 2023

    Ravi Mangal, Klas Leino, Zifan Wang, Kai Hu, Weicheng Yu, Corina Pasareanu, Anupam Datta, and Matt Fredrikson. Is certifyingℓ p robustness still worthwhile?arXiv preprint arXiv:2310.09361, 2023. 2, 8

    work page arXiv 2023

  38. [38]

    Universal adversarial perturba- tions

    Seyed-Mohsen Moosavi-Dezfooli, Alhussein Fawzi, Omar Fawzi, and Pascal Frossard. Universal adversarial perturba- tions. InCVPR. IEEE, 2017. 8

    work page 2017

  39. [39]

    Moss, Mykel J

    Robert J. Moss, Mykel J. Kochenderfer, Maxime Gariel, and Arthur Dubois. Bayesian safety validation for failure prob- ability estimation of black-box systems.AIAA Journal of Aerospace Information Systems (JAIS), 2024. 2, 8

    work page 2024

  40. [40]

    Reachability analysis of deep neural networks with provable guarantees

    Wenjie Ruan, Xiaowei Huang, and Marta Kwiatkowska. Reachability analysis of deep neural networks with provable guarantees. InIJCAI, 2018. 8

    work page 2018

  41. [41]

    Landing system development based on inverse homography range camera fu- sion (IHRCF).Sensors, 22(5):1870, 2022

    Mohammad Sefidgar and Rene Landry Jr. Landing system development based on inverse homography range camera fu- sion (IHRCF).Sensors, 22(5):1870, 2022. 8

    work page 2022

  42. [42]

    Neural network verification with branch-and-bound for general nonlinearities

    Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho- Jui Hsieh, and Huan Zhang. Neural network verification with branch-and-bound for general nonlinearities. InTACAS, pages 315–335, 2025. 8

    work page 2025

  43. [43]

    An abstract domain for certifying neural networks

    Gagandeep Singh, Timon Gehr, Markus P ¨uschel, and Martin Vechev. An abstract domain for certifying neural networks. PACMPL, 3(POPL):1–30, 2019. 2, 8

    work page 2019

  44. [44]

    Certifying some distributional robustness with principled adversarial training.arXiv preprint arXiv:1710.10571, 2017

    Aman Sinha, Hongseok Namkoong, Riccardo V olpi, and John Duchi. Certifying some distributional robustness with principled adversarial training.arXiv preprint arXiv:1710.10571, 2017. 8

    work page arXiv 2017

  45. [45]

    In- triguing properties of neural networks

    Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. In- triguing properties of neural networks. InICLR, 2014. 2, 8

    work page 2014

  46. [46]

    A new technique for fully autonomous and efficient 3D robotics hand/eye calibra- tion.IEEE Transactions on Robotics and Automation, 5(3): 345–358, 1989

    Roger Y Tsai, Reimar K Lenz, et al. A new technique for fully autonomous and efficient 3D robotics hand/eye calibra- tion.IEEE Transactions on Robotics and Automation, 5(3): 345–358, 1989. 8

    work page 1989

  47. [47]

    To- wards verifying the geometric robustness of large-scale neu- ral networks.Proceedings of the AAAI conference on AI,

    Fu Wang, Peipei Xu, Wenjie Ruan, and Xiaowei Huang. To- wards verifying the geometric robustness of large-scale neu- ral networks.Proceedings of the AAAI conference on AI,

    work page

  48. [48]

    Art-point: Im- proving rotation robustness of point cloud classifiers via ad- versarial rotation

    Ruibin Wang, Yibo Yang, and Dacheng Tao. Art-point: Im- proving rotation robustness of point cloud classifiers via ad- versarial rotation. InProceedings of the IEEE/CVF Confer- ence on Computer Vision and Pattern Recognition, 2022. 8

    work page 2022

  49. [49]

    Beta-CROWN: Efficient bound propagation with per-neuron split constraints for com- plete and incomplete neural network verification.NeurIPS, 34, 2021

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for com- plete and incomplete neural network verification.NeurIPS, 34, 2021. 8

    work page 2021

  50. [50]

    Deobfuscating machine learning assurance and approval

    Kimberly Wasson and Robert V oros. Deobfuscating machine learning assurance and approval. In43rd Digital Avionics Systems Conference (DASC), pages 1–10. IEEE, 2024. 2

    work page 2024

  51. [51]

    Toward certified ro- bustness against real-world distribution shifts

    Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George Pappas, Hamed Hassani, Co- rina Pasareanu, and Clark Barrett. Toward certified ro- bustness against real-world distribution shifts. InIEEE Conference on Secure and Trustworthy Machine Learning (SaTML), pages 537–553. IEEE, 2023. 8

    work page 2023

  52. [52]

    Marabou 2.0: a versatile formal analyzer of neural networks

    Haoze Wu, Omri Isac, Aleksandar Zelji ´c, Teruhiro Tago- mori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, et al. Marabou 2.0: a versatile formal analyzer of neural networks. InCAV, pages 249–264. Springer, 2024. 7, 8

    work page 2024

  53. [53]

    Spatially Transformed Adversarial Examples

    Chaowei Xiao, Jun-Yan Zhu, Bo Li, Warren He, Mingyan Liu, and Dawn Song. Spatially transformed adversarial ex- amples.arXiv preprint arXiv:1801.02612, 2018. 8

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  54. [54]

    Automatic perturbation analysis for scalable certified robustness and beyond

    Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai- Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. InNeurIPS, pages 1129– 1141, 2020. 8

    work page 2020

  55. [55]

    Fast and Complete: En- abling complete neural network verification with rapid and massively parallel incomplete verifiers

    Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and Complete: En- abling complete neural network verification with rapid and massively parallel incomplete verifiers. InICLR, 2021. 7, 8

    work page 2021

  56. [56]

    Provable defense against geometric transformations

    Rem Yang, Jacob Laurel, Sasa Misailovic, and Gagandeep Singh. Provable defense against geometric transformations. InICLR, 2023. 8

    work page 2023

  57. [57]

    Efficient neural network robustness certi- fication with general activation functions

    Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certi- fication with general activation functions. pages 4939–4948,

    work page

  58. [58]

    General cutting planes for bound-propagation-based neural network verifica- tion

    Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. General cutting planes for bound-propagation-based neural network verifica- tion. InNeurIPS, pages 1656–1670, 2022. 8 10 Lipschitz Optimization for Formal Verification of Homographies Supplementary Material

    work page 2022

  59. [59]

    Notation ≜Equality by definition J1, nKSet of natural integers between1andn, both included A,B,C, . . .Sets (cursive script) Diff (B)Subset ofBwhere the bound errorf is differentiable f ∗ Optimum value (maximum or minimum) of functionf cf ∗ Estimate off ∗ Gx0 i,j (κ)Value of pixel(i, j)in the transformed image, when imagex 0 is transformed byκ xVectors, w...

    work page

  60. [60]

    Sample images from each dataset

    Datasets MNIST CIF AR10 GTSRB LARD Figure 6. Sample images from each dataset

    work page

  61. [61]

    In this case, bilinear interpolation relies on padding mechanisms to impute missing pixel values

    Padding Geometric transformations frequently map target coordinates beyond the boundaries of the source image. In this case, bilinear interpolation relies on padding mechanisms to impute missing pixel values. Depending on the application, different padding 1 techniques exist, with varying levels of complexity and realism. For the traffic sign of Fig. 7, “...

    work page

  62. [62]

    Transforms glossary We detail a few scenarios that simplify the general homography form given in Eq. (7). Under our assumptions, we show that some of these scenarios simplify into exact affine transforms. We also notice that rotation perturbations are independent of the pose of the initial viewpoint. For brevity of the translation cases, we simplify furth...

    work page

  63. [63]

    Full closed-form expressions We detail here the remaining closed-form expressions needed in Eq. (7). Note that the roll, pitch, yaw angles are not defined in the camera frame(C)(x-right,y-down,z-forward), but in a body frame(B)withx-forward,y-right,z-down. The transform T CAM BODY is thus needed to obtain the correct transforms. There is no translation be...

    work page

  64. [64]

    In this context, t=0and Eq

    Example: yaw deviation∆ψ For the yaw deviation example, we set the pose of the first camera (i.e.ϕ, θ, ψ, x, y, z) to be arbitrary, and set∆ϕ= ∆θ= ∆x= ∆y= ∆z= 0so that only the yaw deviation∆ψexplains the motion from first to second viewpoint. In this context, t=0and Eq. (7) reduces to the special caseH(∆ψ) =K·R·K −1, valid even if scene points are not co...

    work page

  65. [65]

    Maximization of|∇ κJ| In [7], an upper bound on the Lipschitz constant is estimated assup κ∈Diff(B) ∇⊤ κ J(κ)·e m for coordinatem. We justify here the maximization of the independent components for the case where there is only one transform parameter(m= 1): |∇κJ(κ)|≜|∇ κ [LB(κ)−G(κ)]|(55) ≜ ∇κ max j∈J1,qK w⊤ j κ+b j −G(κ) (56) ≤ ∇κ max j∈J1,qK w⊤ j κ+b j ...

    work page

  66. [66]

    13 and derive a majorant for the gradient of the inverse transform ∇⊤ ∆ψT −1 , more particularly along each coordinate by maximizing ∂u0 ∂∆ψ and ∂v0 ∂∆ψ independently

    Upper bound locations for gradient|∇ ∆ψT −1| In the yaw perturbation example, we follow Sec. 13 and derive a majorant for the gradient of the inverse transform ∇⊤ ∆ψT −1 , more particularly along each coordinate by maximizing ∂u0 ∂∆ψ and ∂v0 ∂∆ψ independently. u-coordinate.We study the variations of the gradient ∂u0 ∂∆ψ given by Eq. (12). We compute its d...

    work page

  67. [67]

    [7] proposes to usefbound =f κ1+κ2 2 + L 2 (κ2 −κ 1)

    Derivation off bound By considering the subdomain midpoint, Equation 18 in Batten et al. [7] proposes to usefbound =f κ1+κ2 2 + L 2 (κ2 −κ 1). In our implementation, we propose a slightly different bound by working rather with the subdomain extremities. Letκ∈ [κ1, κ2]⊂R. Using the Lipschitz property off, we derive the following bound forf(κ): ( f(κ)≤f(κ 1...

    work page

  68. [68]

    Models To verify robustness against the VNN datasets [9], we use the official benchmark networks available from the competition repositories athttps://github.com/VNN- COMP(see Tab. 5). There is no existing VNN benchmark for runway visibility, so we train a custom runway classifier on the LARD dataset [14], network and training details are given below. 7 D...

    work page 2021

  69. [69]

    2, this section presents extended robustness results on additional networks of the VNN-COMP benchmarks

    Extended results To complete Tab. 2, this section presents extended robustness results on additional networks of the VNN-COMP benchmarks. We indicate the number of timeouts in brackets, if any. A high number of timeouts indicates a potential need to increase the timeout limit and leave more time for the verifier to output a certified result. Perturbation ...

    work page 2026