Scalable Neural Network Geometric Robustness Validation via Hölder Optimisation

We thank the reviewer for the comments. We address the specific questions and provide clarifying points to he identified weaknesses.

Question 1.

We have run HOVer on 500 verification queries from the SoundBench benchmark, for which the ground truth result is known. We have observed no unsound results. HOver is based on global optimisation and, unlike other methods like SIP, it does not compute bounds for the nodes of the model. So it is unclear to us how it could be combined with SIP or IBP. For a comparison we did use IBP (auto_LiRPA) to compute bounds for a small ResNet model (WideResNet trained on TinyImageNet) - the bounds derived were too loose to establish a good robustness result (see Appendix B1).

Question 2.

[Guidance on parameter r]

Consolidated results from the optimisation literature suggest the that a value slightly higher than 1, e.g., 1.3, yields close to optimal solutions [1]. We report an ablation study on r in Table 1 on two benchmarks with ground-truth: TLL Verify Bench from VNN-COMP (2 dimensions) and MLP5 from SoundnessBench (10 dimensions). We report the counts of SAFE, UNSAFE, and Unknown cases, along with the average runtime in seconds (SAFE+UNSAFE, excluding Timeout), where the result also confirms [1] . Hence, we would just recommend that the consolidated results from the optimisation literature are appropriate to be used here.

Table 1: Ablation study on the reliability parameter r

[Guidance on the Hilbert curve resolution parameter m]

The computational complexity of the Hilbert space mapping grows linearly in m. Any value of m > 30, which already provides small calibration errors (see mathematical expression (10) in the paper), would be adequate to use. We report an ablation study on m in Table 2, which confirms this intuition - any value of m > 10 resolves all verification queries with stable overheads.

Table 2: Ablation study on the Hilbert curve resolution parameter m

[Guidance on the Optimisation budget parameter ϵ]

The optimisation budget corresponds to the typical optimisation gap present in all convergent algorithms. As the ablation study in Table 3 shows, the smaller its value the more verification queries can be resolved, albeit with longer runtime. Its value is thus contingent to the complexity on the queries in question and resources. Our recommendation is to tune ϵ in line with the comprehensive ablation study provided.

Table 3. Ablation study on the optimisation budget parameter ϵ

Question 3.

We have attempted to run αβ‑CROWN on ImageNet‑scale networks (with more than 24 million NN parameters) that we analyse here (e.g. ResNet‑50 on a 3 × 224 × 224 input and Inception‑v3 on 2 × 299 × 299), but we were not able to. One major obstacle is operator coverage: although the Spatial Transformer Network (STN) can be represented in the computation graph, in our understanding the current αβ‑CROWN implementation does not provide the bounded operations for geometric perturbations, specifically, affine_grid and grid_sample.

A further obstacle is scalability: αβ‑CROWN’s memory footprint grows roughly linearly with both the number of neurons and the full input resolution which makes branching/splitting prohibitively expensive. To illustrate this, we constructed a one‑pixel perturbation (corresponding to 3 dimensions) as a comparable low‑dimensional proxy, as our geometric experiments involve low‑dimensional perturbations.

We used the ResNet18_cifar model provided in αβ‑CROWN’s repository and used its wider variant to increase the inplanes from 2 to 8, yielding a larger model. We then performed verification queries at ε = 0.1 and ε = 0.3 on these two models over a random pixel, reasonably assuming that they are expected to be robust (i.e., safe) within these perturbation radii.

Table 4 reports the results for this simplified setting, where αβ‑CROWN verifies the smallest case at ε=0.1 but TIMEOUT or runs out of memory (OOM) as ε increases or the model grows; in contrast, HOVer consistently returns safe with lower and more stable memory as it only requires the forward pass. In our experiments αβ‑CROWN runs out of memory (OOM) on a relatively small model with 175,802 parameters. In conclusion we see no way to scale it to models with tens/hundreds of millions of parameters as we do here, or to ImageNet‑scale inputs with geometric perturbations.

Table 4: Verification results on one‑pixel perturbation for CIFAR10 models

[Comment on Low-dimensional perturbation spaces]

Geometric transformations are important in many practical applications including object detection since geometric adversarial vulnerability is evidenced in practice [2]. HOVer is specifically designed for robustness analysis with respect to geometric perturbations. Within this scope, we do not consider said perturbation as a limitation, as all combinations of geometric transformations can be encoded using HOVer. We noted elsewhere that the same approach will be effective on other low-dimensional perturbations, such as bias-field, contrast, luminosity and blur. However, we acknowledge that if the goal were to develop a general-purpose method for neural network analysis, this focus would indeed constitute a limitation.

Clarification

The missing baseline result for GeoRobust in Table 1 is due to an update in the timm (PyTorch Image Models) library, which previously caused the ResNet model to achieve only ∼9% robust accuracy (abnormally low). The updated model now achieves a more reasonable ∼25% robust accuracy. We will rerun GeoRobust using the updated model and include the result in the revised version.

[1] Introduction to global optimization exploiting space-filling curves, 2013

[2] Adversarial examples based on object detection tasks, 2023

Dear Reviewer BsfB,

Thank you for acknowledging our response. May we ask whether our answer addressed your question? We are asking this as we were not sure of the question and remain more than happy to clarify further.

We took your comments further today (with our interpretation), and to provide a further quantitative assessment related to your question, we conducted additional experiments. We took the publicly available CIFAR10 and RESNET models from VNNCOMP and evaluated HOVer on provably sound Lipschitz overapproximations (by multiplying the spectral norms of the network), denoted as HOVer* in the table, and compared with HOVer, defined as in the paper on commonly accepted parameters in global optimisation. The queries are 1-pixel perturbations. As previously discussed, in this setting HOVer* reports provably sound results.

Table 5: Verification results on different cifar10 models (HOVer*: HOVer with True uppper bound of Lipschitz constant)

As the results show HOVer* verifies some models but timeouts when the Lipschitz constant exceeds a certain value. In contrast, of course HOVer validates all models and scales to models with much larger Lipschitz constants (e.g., around 8e+50 for ResNet34) and much larger models (over 300M parameters), as reported in the paper. We are adding this table as perhaps this is the explicit quantitative assessment you would have liked to see to identify exactly where the barrier is.

As in the previous message, we stress that, unlike much of the existing verification literature, model size itself is not the primary bottleneck in our setting. This is instead the value of the Lipschitz constant, as the experiments above demonstrate.

We hope this further clarifies the issue raised previously.

Question 1.

We fully agree with the reviewer’s remarks. Our goal was to be as transparent and scientifically precise as possible, and we welcome the opportunity to further improve this. We are happy to refer to our approach as a method for "robustness analysis" or "robustness validation" and change the title accordingly and all referenced text within accordingly. Indeed, we may prefer these over "approximate verification" as they more clearly emphasise the contrast to "verification", in the spirit of the reviewer's comment, which we endorse. That said, we believe that the method here presented strictly goes beyond, and is conceptually different from, the kind of empirical robustness analysis typically performed using PGD and derivatives. We welcome further comments on this.

If the paper is accepted, we will revise the paper to acknowledge that, in principle, a sound method can indeed be implemented correctly. We had absolutely no intention of being dismissive to existing work, which we believe has great value, and are grateful for the opportunity to clarify our position.

Question 2.

As discussed in the paper tools from VNNCOMP cannot solve queries on geometric perturbations on large models that we evaluate here; this is not only due to the nature of the perturbations but also the large input size and large models.

We have attempted to run αβ‑CROWN on the ImageNet‑scale networks (with more than 24 million NN parameters) that we analyse here (e.g. ResNet‑50 on a 3 × 224 × 224 input and Inception‑v3 on 2 × 299 × 299), but we were not able to. One major obstacle is operator coverage: although the Spatial Transformer Network (STN) can be represented in the computation graph, to our knowledge the current αβ‑CROWN implementation does not provide the bounded operations for geometric perturbations, specifically, affine_grid and grid_sample.

A further obstacle is scalability: αβ‑CROWN’s memory footprint grows roughly linearly with both the number of neurons and the full input resolution, which makes branching/splitting prohibitively expensive. To illustrate this, we constructed a one‑pixel perturbation (corresponding to 3 dimensions) as a comparable low‑dimensional proxy, as our geometric experiments involve low‑dimensional perturbations.

We used the ResNet18_cifar model provided in αβ‑CROWN’s repository and used its wider variant to increase the inplanes from 2 to 8, yielding a larger model. We then performed verification queries at ε = 0.1 and ε = 0.3 on these two models over a random pixel, reasonably assuming that they are expected to be robust (i.e., safe) within these perturbation radii.

Table 1 reports the results for this simplified setting, where αβ‑CROWN verifies the smallest case at ε=0.1 but reports TIMEOUT or runs out of memory (OOM) as ε increases or the model grows; in contrast, HOVer consistently returns safe with lower and more stable memory as it only requires the forward pass. In our experiments αβ‑CROWN runs out of memory (OOM) on a relatively small model with 175,802 parameters. In conclusion we see no way to scale it to models with tens/hundreds of millions of parameters as we do here, or to ImageNet‑scale inputs.

Table 1: Verification results on one‑pixel perturbation for CIFAR10 models

Minor Notes.

We thank the reviewer for pointing out these typos which will be correct in the final version if the paper is accepted. $h_k$ is defined in lines 182-183, which is the global Hölder constant so far.

We thank the reviewer for the comments. We address the specific questions as follows.

Question 1.

[Reliability parameter r]

Empirical results from the optimisation literature suggest the usage of a small value close to 1, e.g., 1.3, yields close to optimal solutions [1]. We report an ablation study on r in Table 1, which confirms the observations in [1]. Specifically, we conducted three ablation studies on the reliability parameter r on two benchmarks with ground-truth: TLL Verify Bench from VNN-COMP (2 dimensions) and MLP5 from SoundnessBench (10 dimensions). We report the counts of SAFE, UNSAFE, and Unknown cases, along with the average runtime in seconds (SAFE+UNSAFE, excluding Timeout). The results show that HOVer outputs no unsound results for any value of r>1, but it becomes hard to answer verification queries with bigger values of r, which, given the above, should not be used. In summary: we have never witnessed a false positives in any of the experiments. Any counterexample is provably correct, so we cannot have any false negatives, and indeed never encountered one.

Table 1: Ablation study on the reliability parameter r

[Hilbert curve resolution parameter m]

The computational complexity of modern libraries providing the Hilbert space mapping grows linearly in m, so any value of m > ~30, which already provides small calibration errors (see mathematical expression (10) in the paper), would be adequate to use. We report an ablation study on m in Table 2 which confirms this intuition - any value of m > 10 resolves all verification queries with stable overheads.

Table 2: Ablation study on the Hilbert curve resolution parameter m

[Optimisation budget parameter ϵ]

The optimisation budget corresponds to the typical optimisation gap present in all convergent algorithms. As the ablation study in Table 3 shows, the smaller its value the more verification queries can be solved, albeit with longer runtime. Its value is thus contingent to available computation and temporal resources.

Table 3: Ablation study on the optimisation budget parameter ϵ

Question 2.

HOVer is designed for geometric verification, and therefore inherently restricted to low‑dimensional perturbation spaces. As shown in Theorem 1, the convergence bound includes an irreducible residual term $H \cdot (\epsilon/2)^{1/N}$. Because $(\epsilon/2)^{1/N}\rightarrow 1$ as $N$ grows, the resulting approximation gap, governed by the Hölder constant, also grows with N, thereby deteriorating convergence and giving overly loose certificates in higher dimensions. Consequently, pushing the method to high dimensionality transformations such as noise remains an open challenge. However, note that extending Hover to other smaller dimensionality perturbations such as contrast, luminosity, bias field, blur, etc, is entirely feasible.

Question 3.

In our extensive evaluations, we have observed no cases where HOVer produces an incorrect robustness result. In principle, by further increasing r beyond what we used in the experiments, we reduce even further the possibility of any unsound results. Currently however, HOVer provides no formal mitigation for potential unsoundness. We believe this to be an acceptable trade-off in the context of a robustness analysis across many test points for the very large models here that can now be analysed.

Question 4.

[GeoRobust and PGD]

We ran 100 randomly sampled ImageNet images through ResNet‑50 considered in the paper and compared the performance of our method (HOVer) against PGD and GeoRobust under the 4‑parameter perturbations. The termination threshold was set to 500 seconds or 50,000 queries per sample. Table 4 reports the average runtime observed. As expected, while fast PGD cannot in principle establish any safe cases. In comparison to GeoRobust, HOVer is markedly more performant.

Table 4: Comparison with GeoRobust and PGD

[$\alpha\beta$-CROWN]

We have attempted to run αβ‑CROWN on the ImageNet‑scale networks (with more than 24 million NN parameters) that we analyse here (e.g. ResNet‑50 on a 3 × 224 × 224 input and Inception‑v3 on 2 × 299 × 299), but we were not able to. One major obstacle is operator coverage: although the Spatial Transformer Network (STN) can be represented in the computation graph, to our knowledge the current αβ‑CROWN implementation (nor any other IBP/SIP tools) does not provide the bounded operations for geometric perturbations, specifically, affine_grid and grid_sample.

A further obstacle is scalability: αβ‑CROWN’s memory footprint grows roughly linearly with both the number of neurons and the full input resolution, which makes branching/splitting prohibitively expensive. To clarify this, we constructed a one‑pixel perturbation (corresponding to 3 dimensions) as a comparable low‑dimensional proxy, as our geometric experiments involve low‑dimensional perturbations. In this simplified setting and in contrast to HOVer, αβ‑CROWN often times out or runs out of memory (OOM). We refer to the response to Question 2 of Reviewer rxtg for the experimental results.

Question 5.

Please see the answer for Question 1.

[Comment on Low-dimensional perturbation spaces]

Geometric transformations are important in many practical applications, including object detection since geometric adversarial vulnerability is evidenced in practice [2]. HOVer is specifically designed for robustness analysis with respect to geometric perturbations. Within this scope, we do not consider said perturbation as a limitation, as all combinations of geometric transformations can be encoded using HOVer. We noted elsewhere that the same approach will be effective on other low-dimensional perturbations, such as bias-field, contrast, luminosity and blur. However, we acknowledge that if the goal were to develop a general-purpose method for neural network analysis, this focus would indeed constitute a limitation.

[Comment on Soundness]

We agree it would be ideal to have a theoretical guarantee on no false positives. As argued in the paper, we believe this is an acceptable trade-off in the context of robustness analysis for very large models that could not be analysed before. We remark that we observed no false positives in all the experiments run.

[Comment on Underperformance wrt GeoRobust]

We observed in the paper that GeoRobust reported incorrect results in some cases. We believe this is due to an underestimation of the Lipschitz constant in their approach; this leads to faster resolution of some cases.

Limitations (possible overconfidence).

We have found no cases where the answer of the tool was incorrect. But we would like to stress that no safety critical systems, such as aviation systems, are validated purely on the basis of formal verification. An assurance case in the industry is much more comprehensive and verification is only a part of the process. Even verification results on sound tools are evaluated in the context of tool qualification and confidence and the possibility of errors creeping up in various ways. This is also likely to be the case with ML systems also in view of the difficulty of coverage quantification of the Operational Design Domain. Therefore we do not believe this risk to be high. Still, we do not believe this removes value from the method, as it significantly pushes forward robustness validation for large models, something that was not possible before.

[1] Introduction to global optimization exploiting space-filling curves, 2013

[2] Adversarial examples based on object detection tasks, 2023

Thank you for the comprehensive and thoughtful rebuttal. I appreciate the detailed experimental additions and clarifications you've provided, which significantly strengthen the submission.

1. Your response addressed my concern about heuristic tuning by including ablation studies on the reliability parameter r (Table 1) and discretization parameter m (Table 2), as well as the optimization budget. These studies confirm the practical robustness of your choices and demonstrate how parameter tuning impacts verification reliability and runtime. This added empirical grounding is appreciated and increases confidence in the proposed framework's stability.

2. Your honest discussion of the method’s current limitation to low-dimensional geometric perturbations is appreciated. The theoretical explanation based on the Hölder bound scaling with NN (i.e., convergence degrading in higher dimensions) is clear, and I agree that focusing on geometric transformations (and their combinations) is a practical and important niche. Your indication that other low-dimensional transformations (e.g., contrast, blur) are within scope is promising. That said, I also appreciate your acknowledgement that generalization to higher-dimensional perturbation spaces—such as pixel-level noise—remains an open challenge. Clarifying this boundary helps position the contribution appropriately.

3. I value your transparency around the absence of formal unsoundness guarantees, and your clarification that no incorrect results were observed in extensive experiments. While this tradeoff is likely acceptable in many practical contexts—especially for large-scale models that previous tools cannot handle—an explicit mitigation strategy or fallback mechanism for safety-critical scenarios would further strengthen the work. Your contextualization of formal verification as just one part of a broader assurance case is well-taken.

4. Thank you for the new runtime comparisons against PGD and GeoRobust (Table 4). These results highlight HOVER’s practical advantages at scale and reinforce the claim that existing sound tools cannot feasibly handle large architectures like ResNet-50 under geometric perturbations. Your observations about αβ-CROWN’s scalability limitations and operator coverage gaps help clarify why direct comparisons weren’t possible in those cases.

Overall, I find this to be a compelling paper that introduces a novel and practical approach to robustness verification under geometric transformations. While it does not offer theoretical novelty in the strictest sense, the integration of space-filling curves, Hölder-based optimization, and reliability-aware heuristics is well-engineered and empirically validated across challenging domains, including video models and large-scale image classifiers.

I am maintaining my original score, but I now view the contribution more favorably in light of the added experiments and your thoughtful rebuttal. This is a strong and relevant submission that pushes the boundary of scalable robustness analysis in a focused domain. Thank you again for the detailed clarifications and engagement.

Question 1.
Empirical results from the optimisation literature suggest that using a small value close to 1, e.g., 1.3, yields close to optimal solutions [1]. We report an ablation study on r in Table 1, which confirms these empirical observations. Specifically, we conducted three ablation studies on the reliability parameter r on two benchmarks where the ground-truth for the verification queries is known: TLL Verify Bench from VNN-COMP (2 dimensions) and MLP5 from SoundnessBench (10 dimensions). We report the counts of SAFE, UNSAFE, and Unknown cases, along with the average runtime in seconds (SAFE+UNSAFE, excluding Timeout). The results show that HOVer outputs no unsound results for any value of r>1, but it becomes increasingly challenging to solve verification queries with bigger values of r. This is in line with literature findings [1] which suggest that big values for r should not be used.

Table 1: Ablation study on the reliability parameter r on Benchmark TLL and MLP5

Question 2.

Since any composition of scaling, shearing, rotation, and translation can be represented as an affine transformation of only 7 parameters, HOVer scales to the models reported in the paper for any composition of transformations.

Specifically, although our initial experiments considered only 4 parameters, our approach extends seamlessly to the 7‑parameter affine group by replacing the transformation matrix with:

where $\lambda_x$ and $\lambda_y$ are independent scaling factors along the horizontal and vertical axes; $\gamma$ is the rotation angle; $s_x$ and $s_y$ are the horizontal and vertical shear coefficients; $t_x$ and $t_y$ represent translations along the x-axis and y-axis.

We evaluated 100 randomly sampled ImageNet images using ResNet‑50 with our method (HOVer) under both 4‑parameter and 7‑parameter perturbations. The termination threshold was set to 500 seconds or 50,000 queries per sample. As shown in Table 2, which reports the SAFE/UNSAFE/Unknown cases and the average runtime for the SAFE + UNSAFE cases, there is only a modest performance drop when moving from isotropic scaling to anisotropic scaling plus shearing (due to the increased number of geometric parameters and the resulting higher number of unsolved cases). Nevertheless, HOVer remains able to verify higher‑dimensional geometric transformation spaces.

Table 2: Robust performance on 100 ImageNet images (ResNet‑50), with clean Acc 70%

[Scaling]

In Appendix B, we have also reported the performance comparisons on smaller models for the MNIST, CIFAR‑10, and TinyImageNet datasets, where we evaluate against prior geometric certification techniques, including DeepG, GSmooth, TSS, and Auto_LiRPA with CGT.

The timing tables below report the average running time (in seconds) for SAFE + UNSAFE cases, excluding timeouts. Measurements are based on 100 ImageNet images and 50 Kinetics videos, evaluated across neural networks ranging from 22M to 300M parameters and data sizes from image to video. We will include all the runtimes in all tables in our revised version.

Table 3: Runtime comparison on the ImageNet dataset

Table 4: Runtime comparison on the Kinetics dataset

[Geometric transformations]

Geometric transformations are important in many practical applications including object detection, since geometric adversarial vulnerability is evidenced in practice [2][3]. We emphasise that our method is specifically designed for robustness analysis with respect to geometric perturbations. Within this scope, we do not consider said perturbation as a limitation, as all combinations of geometric transformations can be effectively encoded using our approach. However, we acknowledge that if the goal were to develop a general-purpose method for neural network analysis, this focus would indeed constitute a limitation.

[Comparison with the SoA]

The Appendix includes a comparison on small models against the previous SoA that can solve geometric certification queries.

[1] Introduction to global optimization exploiting space-filling curves, 2013

[2] Exploring the Landscape of Spatial Robustness, 2017

[3] Adversarial examples based on object detection tasks, 2023