On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models
read the original abstract
Recent work has shown that it is possible to train deep neural networks that are provably robust to norm-bounded adversarial perturbations. Most of these methods are based on minimizing an upper bound on the worst-case loss over all possible adversarial perturbations. While these techniques show promise, they often result in difficult optimization procedures that remain hard to scale to larger networks. Through a comprehensive analysis, we show how a simple bounding technique, interval bound propagation (IBP), can be exploited to train large provably robust neural networks that beat the state-of-the-art in verified accuracy. While the upper bound computed by IBP can be quite weak for general networks, we demonstrate that an appropriate loss and clever hyper-parameter schedule allow the network to adapt such that the IBP bound is tight. This results in a fast and stable learning algorithm that outperforms more sophisticated methods and achieves state-of-the-art results on MNIST, CIFAR-10 and SVHN. It also allows us to train the largest model to be verified beyond vacuous bounds on a downscaled version of ImageNet.
This paper has not been read by Pith yet.
Forward citations
Cited by 19 Pith papers
-
Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators
Small FNOs are piecewise-linear and can be encoded exactly into Z3 for sound proofs and counterexamples on positivity and mass properties, exposing a clear soundness-scalability tradeoff.
-
Parameterized Hardness of Zonotope Containment and Neural Network Verification
The paper proves W[1]-hardness parameterized by dimension d for positivity, zonotope containment, max approximation, and L_p-Lipschitz constants in 2- and 3-layer ReLU networks, showing enumeration methods are optimal...
-
Input Convex Neural Network as a Surrogate in Stability-Constrained Optimization for IBR-dominated Power Systems
The paper shows that generic Big-M reformulations and reversed stability inequalities destroy the convexity benefits of ICNN surrogates and supplies an exact LP epigraph reformulation plus outer- and inner-approximati...
-
Stress-Testing Neural Network Verifiers with Provably Robust Instances
A reusable framework generates verification instances with provably known robustness labels, revealing numeric tolerance issues and bugs in five verifiers while introducing difficulty profiles to diagnose failure modes.
-
Adversarial Robustness of NTK Neural Networks
NTK neural networks achieve minimax optimal adversarial regression rates in Sobolev spaces using gradient flow with early stopping, but minimum norm interpolants are vulnerable in the overfitting regime.
-
Relaxation-Informed Training of Neural Network Surrogate Models
Regularizers that penalize big-M constants, unstable neurons, and per-sample LP relaxation gaps during neural network training reduce MILP solve times by up to four orders of magnitude while preserving surrogate accuracy.
-
SafeAdapt: Provably Safe Policy Updates in Deep Reinforcement Learning
SafeAdapt certifies a Rashomon set of safe policies from demonstration data and projects updates from arbitrary RL algorithms onto it to guarantee preservation of safety on source tasks.
-
Fast and Certified Bounding of Security-Constrained DCOPF via Interval Bound Propagation
Interval Bound Propagation computes certified bounds on SC-DCOPF optimal costs with mean gaps below 3.98% on small cases and scales efficiently to 8316-bus systems with thousands of contingencies.
-
Making Logic a First-Class Citizen in Generative ML for Networking
NetNomos is a multi-stage framework that extracts, filters, and enforces first-order logic rules in generative ML models for networking tasks including telemetry imputation, traffic forecasting, and synthetic trace ge...
-
Adversarial Hubness in Multi-Modal Retrieval
Adversarial hubs can be generated to be retrieved as top-1 for over 84% of test queries in text-to-image retrieval, far exceeding natural hubs.
-
Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control
CT-BaB integrates branch-and-bound during training to tighten certified Lyapunov bounds, yielding neural controllers with 164X larger verifiable ROA and 11X faster verification than CEGIS on a 2D quadrotor.
-
Towards Generalized Certified Robustness with Multi-Norm Training
CURE is the first multi-norm certified training method that improves union robustness across l_p norms and unseen perturbations on MNIST, CIFAR-10 and TinyImagenet.
-
Vulnerability of Natural Language Classifiers to Evolutionary Generated Adversarial Text
GAversary, a black-box genetic algorithm with GloVe-based mutations, generates adversarial examples that reduce NLP model accuracy more than BAE or A2T on benchmarks while perturbing more words.
-
Hybrid Robustness Verification for Spatio-Temporal Neural Networks
STBP computes exact closed-form bounds for the first convolutional layer of spatio-temporal networks and propagates scalable approximations through the rest to certify robustness under subset-frame or patch perturbations.
-
Adversarial Robustness of NTK Neural Networks
NTK networks achieve minimax optimal adversarial regression rates in Sobolev spaces with early stopping, but minimum-norm interpolants are vulnerable.
-
Connecting Lyapunov Control Theory to Adversarial Attacks
Connects Lyapunov control theory to a provable defense against weaker adversarial attacks on neural networks.
-
Veriphi: Attack-Guided Neural Network Verification with Dataset-Dependent Training Methods
Veriphi reports 5x verification speedup and finds that certified training is not universally superior to adversarial training, with IBP at 78% on MNIST but negligible on CIFAR-10 where PGD reaches 94%.
-
The Luna Bound Propagator for Formal Analysis of Neural Networks
Luna delivers a C++ bound propagator supporting interval, DeepPoly/CROWN, and alpha-CROWN analyses that reports tighter bounds and higher speed than the leading Python alpha-CROWN implementation on VNN-COMP 2025 benchmarks.
-
Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial
Tutorial introducing applications of the existing α,β-CROWN verifier to scalable formal verification of neural network controllers via bound computation and domain partitioning.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.