arxiv: 2604.24379 · v1 · submitted 2026-04-27 · 💻 cs.AI · cs.LG· cs.SC

Recognition: unknown

Certified geometric robustness -- Super-DeepG

No\'emie Cohen , M\'elanie Ducoffe (Airbus CR\&T) , Christophe Gabreau , Claire Pagetti , Xavier Pucel

Authors on Pith no claims yet

Pith reviewed 2026-05-08 03:24 UTC · model grok-4.3

classification 💻 cs.AI cs.LGcs.SC

keywords neural network verificationgeometric robustnesslinear relaxationLipschitz optimizationGPU accelerationformal certificationimage perturbationssafety-critical AI

0 comments

The pith

Super-DeepG refines linear relaxation and Lipschitz techniques to certify neural network robustness against geometric image perturbations with higher precision and speed than prior tools.

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

The paper presents Super-DeepG as a method to formally verify that neural networks for image processing remain reliable when inputs undergo small rotations, scalings, shears, or translations. It improves the core reasoning steps in linear relaxation bounds and Lipschitz constant optimization while adding a GPU-accelerated implementation. A reader would care because safety-critical systems need guaranteed behavior under realistic input variations, and current certification methods often trade off too much precision for speed or vice versa. The work shows that these targeted refinements deliver both better tightness in the certified bounds and faster runtimes on standard benchmarks.

Core claim

Super-DeepG improves the reasoning used in linear relaxation techniques and Lipschitz optimization, and provides an implementation that leverages GPU hardware. By doing so, Super-DeepG achieves both precision and computational efficiency of robustness certification, to an extent that outperforms prior work. The method targets geometric perturbations on image datasets and is released as open-source software.

What carries the argument

Super-DeepG, an enhanced verifier that tightens linear relaxation bounds and Lipschitz constants for geometric transformations while running on GPU hardware.

If this is right

Networks that previously could not be certified within time limits become verifiable.
Certification can handle larger ranges of rotation, scaling, and shear while staying sound.
The open-source tool allows direct comparison and integration into existing verification pipelines for image classifiers.
Safety arguments for deployed image-processing models can cite tighter certified robustness margins.

Where Pith is reading between the lines

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

The same refinement pattern could be tested on other input transformations such as perspective changes or lighting shifts.
Combining Super-DeepG bounds with adversarial training might produce models that are both more accurate and easier to certify.
The GPU implementation opens the possibility of certifying robustness during training rather than only after.

Load-bearing premise

The refinements to linear relaxation reasoning and Lipschitz optimization preserve the formal soundness of the certification guarantees.

What would settle it

Run Super-DeepG and a prior verifier on the same set of networks and geometric perturbation ranges; if Super-DeepG ever certifies a network that the prior verifier correctly rejects as non-robust, or if its certified bounds are looser while claiming tighter precision, the claimed improvement fails.

Figures

Figures reproduced from arXiv: 2604.24379 by Christophe Gabreau, Claire Pagetti, M\'elanie Ducoffe (Airbus CR\&T), No\'emie Cohen, Xavier Pucel.

**Figure 1.** Figure 1: Initial lower linear bound for the sampled values of one pixel at varying transformation values. view at source ↗

**Figure 2.** Figure 2: Illustration of the DOO algorithm used in view at source ↗

**Figure 3.** Figure 3: Super-DeepG approach with N = 13 partitions. The correction term is in red. constant over [θ, θ], a subdivision number of N entails, by equation (10), that the correction term is δ = mini r( θi+θi+1 2 , A, B) − L|θ − θ|/2N. We obtain it in one pass as illustrated in view at source ↗

**Figure 4.** Figure 4: Increasing P beyond 10 brings no significant gains (log scale). Rotation in [−30◦ , 30◦ ] on MNIST. Influence of the hyper-parameters N and interval size Reducing the interval size improves certified accuracy significantly, reaching the clean accuracy baseline, as illustrated in view at source ↗

**Figure 5.** Figure 5: Smaller interval sizes improve certified accuracy more than increasing view at source ↗

read the original abstract

Safety-critical applications are required to perform as expected in normal operations. Image processing functions are often required to be insensitive to small geometric perturbations such as rotation, scaling, shearing or translation. This paper addresses the formal verification of neural networks against geometric perturbations on their image dataset. Our method Super-DeepG improves the reasoning used in linear relaxation techniques and Lipschitz optimization, and provides an implementation that leverages GPU hardware. By doing so, Super-DeepG achieves both precision and computational efficiency of robustness certification, to an extent that outperforms prior work. Super-DeepG is shared as an open-source tool on GitHub.

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.

Desk Editor's Note private letter to a colleague

Super-DeepG refines linear relaxation and Lipschitz methods for geometric robustness certification with a GPU implementation and open-source release, but the abstract supplies no concrete comparisons or derivations to support the outperformance claims.

read the letter

The punchline is that Super-DeepG refines linear relaxation and Lipschitz methods for certifying neural nets against geometric perturbations like rotation and scaling, runs them on GPUs for better speed, and releases the code openly. It claims better precision and efficiency than previous tools. It builds directly on prior work in the area, which is a strength because it doesn't reinvent the wheel but tries to optimize the existing reasoning. The focus on GPU hardware is practical since verification can be computationally heavy, and making it open source means the community can inspect and use the implementation. This could help in domains where formal guarantees are required for safety. The authors are from Airbus, which suggests they have real use cases in mind for certified systems. The main weakness is that without detailed derivations or experimental results in the provided abstract, it's difficult to see exactly what the improvements are or how they maintain the formal certification properties. The claim of outperforming prior work needs concrete comparisons and error analysis to be convincing. If the full paper includes those, it would be much stronger; otherwise the contribution looks incremental at best. Also, since the full text wasn't reviewed here, there might be more in the experiments that addresses this. Readers working on robustness certification for image-based AI systems would get the most out of this, especially if they need a tool to try out. It shows clear thinking about the practical constraints of verification. I think it deserves to go to peer review because the topic is relevant and the method extends known techniques in a targeted way, though the referees will probably ask for more evidence on the performance gains and soundness preservation. Overall, the approach seems sound in principle but the presentation needs to be more specific to be fully useful.

Referee Report

2 major / 0 minor

Summary. The paper introduces Super-DeepG, a method for certified robustness of neural networks against geometric perturbations (rotation, scaling, shearing, translation) on image inputs. It refines the reasoning in linear relaxation techniques and Lipschitz optimization, provides a GPU-accelerated implementation claimed to improve both precision and computational efficiency over prior work such as DeepG, preserves formal guarantees, and releases the tool as open-source on GitHub.

Significance. If the refinements are sound and the claimed gains in tightness and speed are demonstrated with rigorous comparisons, the work could advance practical certified verification for safety-critical image-processing systems. The open-source release supports reproducibility.

major comments (2)

Abstract: the central claim of outperformance in precision and efficiency supplies no specific derivations, experimental comparisons, error bounds, or verification details, preventing assessment of whether the math and data support the claim.
Abstract: the description gives no indication of how the refinements to linear relaxation and Lipschitz optimization are formalized or proven to preserve soundness while improving bounds, which is load-bearing for the certification guarantee.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and constructive comments on the abstract. We address each major comment below. The full manuscript contains the supporting derivations, proofs, and experimental results, but we agree that the abstract can be strengthened to better highlight these elements without altering the core claims.

read point-by-point responses

Referee: Abstract: the central claim of outperformance in precision and efficiency supplies no specific derivations, experimental comparisons, error bounds, or verification details, preventing assessment of whether the math and data support the claim.

Authors: We acknowledge that the abstract is high-level and does not embed quantitative results. The manuscript provides these in the technical and experimental sections: refined linear relaxations yield tighter interval bounds with explicit error analysis relative to DeepG; Lipschitz optimization improvements are benchmarked via runtime and tightness metrics on geometric perturbation tasks (rotations, scalings, etc.) using standard image datasets; all comparisons preserve the original soundness guarantees. To facilitate assessment, we will revise the abstract to include concise references to these comparisons and key performance indicators. revision: yes
Referee: Abstract: the description gives no indication of how the refinements to linear relaxation and Lipschitz optimization are formalized or proven to preserve soundness while improving bounds, which is load-bearing for the certification guarantee.

Authors: The abstract summarizes at a high level, but Sections 3 and 4 of the manuscript formalize the refinements: we strengthen the linear relaxation rules for geometric transformations with tighter convex enclosures and optimize the Lipschitz constant computation via a refined interval arithmetic strategy. Soundness (i.e., the computed bounds remain valid over-approximations) is proven by induction on the network layers, extending the DeepG framework without introducing unsound relaxations. We will update the abstract to explicitly note that these refinements preserve formal guarantees as established in the paper. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The abstract describes Super-DeepG as an improvement to linear relaxation and Lipschitz optimization techniques for geometric robustness certification, with a GPU implementation that outperforms prior work while preserving formal guarantees. No equations, derivations, fitted parameters, or self-citations are presented that would reduce any claimed prediction or result to its own inputs by construction. The central claim rests on the soundness and empirical superiority of the (unprovided) refinements, which are treated as independent contributions rather than self-referential definitions or renamings. This is the expected self-contained case for a methods paper whose load-bearing steps are algorithmic and externally verifiable.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available; no free parameters, axioms, or invented entities are described.

pith-pipeline@v0.9.0 · 5413 in / 1023 out tokens · 21317 ms · 2026-05-08T03:24:36.493441+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

24 extracted references · 3 canonical work pages

[1]

K. M. Ashish Goel, Benjamin Van Roy. Introduction to Optimization. https://web.stanford.edu/ ~ashishg/msande111/notes/chapter3.pdf, 2008

2008
[2]

Balunovic, M

M. Balunovic, M. Baader, G. Singh, T. Gehr, and M. Vechev. Certifying geometric robustness of neural networks. Advances in Neural Information Processing Systems , 32, 2019

2019
[3]

Batten, Y

B. Batten, Y. Zheng, A. De Palma, P. Kouvaros, and A. Lomuscio. Verification of geometric robustness of neural networks via piecewise linear approximation and lipschitz optimisation. In ECAI 2024, pages 2362–2369. IOS Press, 2024

2024
[4]

Bertsimas and J

D. Bertsimas and J. N. Tsitsiklis. Introduction to linear optimization , volume 6. Athena scientific Belmont, MA, 1997

1997
[5]

Bougacha, G

Y. Bougacha, G. Delhomme, M. Ducoffe, A. Fuchs, J.-B. Ginestet, J. Girard, S. Kraiem, F. Mamalet, V. Mussot, C. Pagetti, et al. Lard 2.0: Enhanced datasets and benchmarking for autonomous landing systems. In 13th European Congress of Embedded Real Time Systems (ERTS) , 2026

2026
[6]

C. Brix, S. Bak, T. T. Johnson, and H. Wu. The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results. arXiv preprint arXiv:2412.19985 , 2024

work page arXiv 2024
[7]

Cousot and R

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , pages 238–252, 1977

1977
[8]

Fischer, M

M. Fischer, M. Baader, and M. Vechev. Scalable certified segmentation via randomized smoothing. In International Conference on Machine Learning , pages 3340–3351. PMLR, 2021

2021
[9]

T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE symposium on security and privacy (SP) , pages 3–18. IEEE, 2018

2018
[10]

F. S. Hillier and G. J. Lieberman. Introduction to operations research. McGraw-Hill, 2015

2015
[11]

G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zelji´ c, et al. The marabou framework for verification and analysis of deep neural networks. In Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31, pages 443–452. Springer, 2019

2019
[12]

L. Li, M. Weber, X. Xu, L. Rimanic, B. Kailkhura, T. Xie, C. Zhang, and B. Li. Tss: Transformation- specific smoothing for robustness certification. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security , pages 535–557, 2021

2021
[13]

C. Liu, T. Arnon, C. Lazarus, C. Strong, C. Barrett, M. J. Kochenderfer, et al. Algorithms for verifying deep neural networks. Foundations and Trends® in Optimization, 4(3-4):244–404, 2021

2021
[14]

M. H. Meng, G. Bai, S. G. Teo, Z. Hou, Y. Xiao, Y. Lin, and J. S. Dong. Adversarial robustness of deep neural networks: A survey from a formal verification perspective. IEEE Transactions on Dependable and Secure Computing, 2022

2022
[15]

Mohapatra, T.-W

J. Mohapatra, T.-W. Weng, P.-Y. Chen, S. Liu, and L. Daniel. Towards verifying robustness of neural networks against a family of semantic perturbations. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition , pages 244–252, 2020. 18

2020
[16]

R. Munos. Optimistic optimization of a deterministic function without the knowledge of its smoothness. Advances in neural information processing systems , 24, 2011

2011
[17]

Singh, M

G. Singh, M. Balunovic, A. Ruoss, C. M¨ uller, J. Maurer, A. Hoffmann, M. Baader, M. Mirman, T. Gehr, P. Tsankov, et al. Eran user manual. ETH Z¨ urich, 2020

2020
[18]

Singh, T

G. Singh, T. Gehr, M. P¨ uschel, and M. Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages , 3(POPL):1–30, 2019

2019
[19]

A Review of Formal Methods applied to Machine Learning

C. Urban and A. Min´ e. A review of formal methods applied to machine learning. arXiv preprint arXiv:2104.02466, 2021

work page arXiv 2021
[20]

K. Xu, Z. Shi, H. Zhang, Y. Wang, K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33:1129–1141, 2020

2020
[21]

R. Yang, J. Laurel, S. Misailovic, and G. Singh. Provable defense against geometric transformations. arXiv preprint arXiv:2207.11177 , 2022

work page arXiv 2022
[22]

H. Zhang. VNN-COMP 2024 TinyImageNet Benchmark. https://github.com/huanzhang12/ vnncomp2024_tinyimagenet_benchmark, 2024

2024
[23]

Zhang, T.-W

H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems , 31, 2018

2018
[24]

Zhang, P

Y. Zhang, P. Kouvaros, and A. Lomuscio. Scalable neural network geometric robustness validation via h¨ older optimisation. InThe Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. 19 Transf. Dataset Clean acc. Tool Interval size Cert. (%) Time per im (s) R(10) CIFAR10 PGD (74.0%) FGV 2 × 10−3 6.0 0.57 2 × 10−4 19.0 5.39 2 × 10−...

2025