On the Formal Verification of 1-Lipschitz Neural Networks

Certifying neural networks against ${\ell }_2$-norm adversarial perturbations is essential for safety-critical deployment. While 1-Lipschitz architectures offer scalable, computationally inexpensive ${\ell }_2$ certified radii, a persistent gap remains between their empirical robustness and guaranteed bounds. To bridge this gap, we investigate formal verification (e.g., LiRPA) on 1-Lipschitz models. Focusing on Gradient Norm Preserving (GNP) networks—a state-of-the-art approach for ${\ell }_2$ certified robustness—we establish a necessary condition for LiRPA to outperform \certrad, proving that this condition fails when parsing standard GNP architectures off-the-shelf. To resolve this limitation, we introduce a LiRPA-compatible graph factorization of GNP activations (e.g. GroupSort2). Leveraging this formulation, we conduct the first evaluation comparing LiRPA against standard Lipschitz certified radii across diverse hyperparameter configurations. Notably, our analysis reveals the first family of networks where analytical Lipschitz bounds outperform consistently LiRPA. We identify two key hyperparameter dimensions governing this behavior: optimization trade-offs and Lipschitz constraint strictness. Specifically, relaxing optimization to enable higher clean accuracy, combined with looser Lipschitz constraints, creates a regime where LiRPA yields provably superior certificates. Based on this insight, we introduce a hybrid certification framework that unifies the scalable geometry of 1-Lipschitz networks with the localized precision of linear bound propagation. This hybrid strategy scales LiRPA certification to deeper architectures. Empirically, on Imagenette—where standalone solvers fail—our framework scales to a VGG16 architecture, achieving 84.5% clean accuracy and advancing certified robust accuracy from 54.0% (standard Lipschitz bounds) to 72.5%.