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
13 Pith papers cite this work. Polarity classification is still indexing.
13
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.
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.
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.
Connects Lyapunov control theory to a provable defense against weaker adversarial attacks on 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.
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.
-
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.
-
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.
-
Connecting Lyapunov Control Theory to Adversarial Attacks
Connects Lyapunov control theory to a provable defense against weaker adversarial attacks on neural networks.
-
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.
- Adversarial Robustness of NTK Neural Networks