Cascading Robustness Verification: Toward Efficient Model-Agnostic Certification

TL;DR

This work tackles the challenge of certifying neural network robustness under adversarial perturbations by addressing the limitations of single incomplete verifiers. It introduces Cascading Robustness Verification (CRV), a model-agnostic, multi-stage framework that aggregates multiple verifiers in a pay-as-you-go cascade, augmented with Stepwise Relaxation (SR) and Fast SR (FSR) to progressively tighten bounds and reduce computation. The authors prove that CRV achieves robustness guarantees at least as strong as the best included verifier ($RA_{ ext{CRV}} \\ge \\max_i RA_i$) and quantify verification cost with a detailed TVC formula, while empirical results on MNIST show up to ~90% runtime reduction and improved robustness coverage compared to baseline verifiers. By combining complementary verification perspectives, CRV mitigates training–verification misalignment and provides more reliable, scalable certification suitable for safety-critical deployments.

Abstract

Certifying neural network robustness against adversarial examples is challenging, as formal guarantees often require solving non-convex problems. Hence, incomplete verifiers are widely used because they scale efficiently and substantially reduce the cost of robustness verification compared to complete methods. However, relying on a single verifier can underestimate robustness because of loose approximations or misalignment with training methods. In this work, we propose Cascading Robustness Verification (CRV), which goes beyond an engineering improvement by exposing fundamental limitations of existing robustness metric and introducing a framework that enhances both reliability and efficiency. CRV is a model-agnostic verifier, meaning that its robustness guarantees are independent of the model's training process. The key insight behind the CRV framework is that, when using multiple verification methods, an input is certifiably robust if at least one method certifies it as robust. Rather than relying solely on a single verifier with a fixed constraint set, CRV progressively applies multiple verifiers to balance the tightness of the bound and computational cost. Starting with the least expensive method, CRV halts as soon as an input is certified as robust; otherwise, it proceeds to more expensive methods. For computationally expensive methods, we introduce a Stepwise Relaxation Algorithm (SR) that incrementally adds constraints and checks for certification at each step, thereby avoiding unnecessary computation. Our theoretical analysis demonstrates that CRV achieves equal or higher verified accuracy compared to powerful but computationally expensive incomplete verifiers in the cascade, while significantly reducing verification overhead. Empirical results confirm that CRV certifies at least as many inputs as benchmark approaches, while improving runtime efficiency by up to ~90%.

Figures (6)

• Figure 1: Visualization of two individual verifier performance: $V_1$ (looser verifier) and $V_2$ (tighter verifier). Shaded areas in (a) and (b) shows class boundaries and the star shows the non-convex feasible set. (a) A perturbed input, $x_1$ is correctly certified as robust by both verifiers. (b) A robust input, $x_2$ is verified as non-robust by $V_1$ as hatched areas are outside of class boundaries (false negative), but correctly certified by $V_2$.
• Figure 2: Robust accuracy and running time of $V_1$, $V_2$, and our proposed method of combined $V_1$&$V_2$ to verify MNIST under $\ell_\infty$ adversarial perturbations.
• Figure 3: Diagram of the combined CRV and SR to improve both robustness certification and computational efficiency.
• Figure 4: Visualization of classification outcomes under incomplete verifiers. The figures show class boundaries (shaded) and a non-convex feasible set (star). In (a), CRV certifies input when any verifier succeeds, which is $V_2$. In (b), SR iteratively adds constraints to tighten the approximation; here, $V_{j2}$ certifies the input as robust, so the tighter and more expensive verifier $V_{j3}$ does not need to be applied.
• Figure 5: Certified runtime (top row) and robust accuracy (bottom row) across perturbation levels $\varepsilon \in \{0.1, 0.15, 0.2, 0.25\}$ on Grad-NN and LP-NN. Each column shows: (a, d) SR on Grad-NN, (b, e) LP-NN, and (c, f) Grad-NN under different verification methods. CRV variants achieve robustness comparable to SDP-cert with substantially lower runtime. LP-cert is faster but less reliable on Grad-NN. Note: In SR, $V_{13}$ corresponds to the original SDP-cert raghunathan2018semidefinite formulation using all constraints. $V_{12}$ is obtained by removing one linear constraint and the quadratic constraint. $V_{11}$ further removes one additional constraint from $V_{12}$, yielding the loosest variant.

Theorems & Definitions (12)

• Definition 1
• Remark 1
• Definition 2
• Remark 2: On the Ordering of Verification Methods
• Theorem 1: Robust Accuracy under CRV
• proof
• Proposition 1
• Corollary 1
• Theorem 2: Robust Accuracy of SR
• proof