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.
hub
On the effectiveness of interval bound propagation for training verifiably robust models
18 Pith papers cite this work. Polarity classification is still indexing.
18
Pith papers citing it
hub tools
representative citing papers
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 under ETH.
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-approximation schemes that restore global convergence properties.
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.
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.
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 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.
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.
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 generation.
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.
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.
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.
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.
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.
Connects Lyapunov control theory to a provable defense against weaker adversarial attacks on neural networks.
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%.
Tutorial introducing applications of the existing α,β-CROWN verifier to scalable formal verification of neural network controllers via bound computation and domain partitioning.
citing papers explorer
-
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 under ETH.
-
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-approximation schemes that restore global convergence properties.
-
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 generation.
-
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.
-
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%.
-
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.
- The Luna Bound Propagator for Formal Analysis of Neural Networks