REVIEW 11 cited by
Evaluating Robustness of Neural Networks with Mixed Integer Programming
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Evaluating Robustness of Neural Networks with Mixed Integer Programming
read the original abstract
Neural networks have demonstrated considerable success on a wide variety of real-world problems. However, networks trained only to optimize for training accuracy can often be fooled by adversarial examples - slightly perturbed inputs that are misclassified with high confidence. Verification of networks enables us to gauge their vulnerability to such adversarial examples. We formulate verification of piecewise-linear neural networks as a mixed integer program. On a representative task of finding minimum adversarial distortions, our verifier is two to three orders of magnitude quicker than the state-of-the-art. We achieve this computational speedup via tight formulations for non-linearities, as well as a novel presolve algorithm that makes full use of all information available. The computational speedup allows us to verify properties on convolutional networks with an order of magnitude more ReLUs than networks previously verified by any complete verifier. In particular, we determine for the first time the exact adversarial accuracy of an MNIST classifier to perturbations with bounded $l_\infty$ norm $\epsilon=0.1$: for this classifier, we find an adversarial example for 4.38% of samples, and a certificate of robustness (to perturbations with bounded norm) for the remainder. Across all robust training procedures and network architectures considered, we are able to certify more samples than the state-of-the-art and find more adversarial examples than a strong first-order attack.
Forward citations
Cited by 11 Pith papers
-
ShardNet: Training Neural Controllers with Hard, Non-Convex Constraints
ShardNet enforces non-convex polyhedral safety constraints in neural controllers by construction via a differentiable projection layer, achieving 100% verified safety and over 3x larger safe sets than prior methods on...
-
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.
-
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.
-
Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism
Adapts TP and FSDP to bound-propagation verification, with FSDP delivering bitwise-identical bounds and 80-90% baseline memory reduction while TP trades some tightness for ~2x peak-memory savings.
-
Neural Network Verification using Partial Multi-Neuron Relaxation
Introduces partial multi-neuron relaxation using existing branching heuristics to balance bound tightness and scalability in neural network verification, with integration into Marabou showing positive experimental com...
-
Neural Two-Stage Stochastic Volt-VAR Optimization for Three-Phase Unbalanced Distribution Systems with Network Reconfiguration
A neural network approximates the second-stage recourse model in two-stage stochastic Volt-VAR optimization, allowing the full problem to be solved as a mixed-integer linear program with over 50x speedup and sub-0.3% ...
-
Neural Two-Stage Stochastic Optimization for Solving Unit Commitment Problem
A neural network approximates recourse costs in two-stage stochastic unit commitment, is embedded as an MILP, and uses a scenario-embedding network for scalable solving with low optimality gaps.
-
Polyhedral Enclosures: An Efficient Combinatorial Abstraction for Nonlinear Neural Feedback Systems
Presents a polyhedral enclosure algorithm encoded as MILP to produce sound over-approximations of forward reachable sets for nonlinear neural feedback systems.
-
A Performance Analyzer for a Public Cloud's ML-Augmented VM Allocator
SANJESH applies bi-level optimization to production traces and reveals VM allocation scenarios that cause 4x worse performance than the operator's existing evaluator detected.
-
veriFIRE: an Industrial Case Study in Verifying Consistency Properties for a DNN-Based Wildfire Detection System
An industrial case study applies neural network verifiers to check monotonicity and bounded-response consistency properties in a DNN-based wildfire detection system on real background samples.
-
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.