REVIEW 5 cited by
Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition
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
read the original abstract
We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. First, we propose novel bounding algorithms based on Lagrangian Decomposition. Previous works have used off-the-shelf solvers to solve relaxations at each node of the BaB tree, or constructed weaker relaxations that can be solved efficiently, but lead to unnecessarily weak bounds. Our formulation restricts the optimization to a subspace of the dual domain that is guaranteed to contain the optimum, resulting in accelerated convergence. Furthermore, it allows for a massively parallel implementation, which is amenable to GPU acceleration via modern deep learning frameworks. Second, we present a novel activation-based branching strategy. By coupling an inexpensive heuristic with fast dual bounding, our branching scheme greatly reduces the size of the BaB tree compared to previous heuristic methods. Moreover, it performs competitively with a recent strategy based on learning algorithms, without its large offline training cost. Finally, we design a BaB framework, named Branch and Dual Network Bound (BaDNB), based on our novel bounding and branching algorithms. We show that BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial robustness properties.
Forward citations
Cited by 5 Pith papers
-
IoUCert: Robustness Verification for Anchor-based Object Detectors
IoUCert derives exact IoU bounds over anchor-offset boxes via a coordinate transformation and uses them to formally verify single-object SSD, YOLOv2, and YOLOv3 models under brightness, contrast, and motion-blur pertu...
-
Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification
A solution-aware ReLU scoring function selects the few binary ReLU variables that matter, letting a hybrid MILP verifier cut undecided robustness instances from 20-58% to 8-15%.
-
Mining Verdict Boundaries for Neural Network Verification
BMiner speeds up Branch-and-Bound neural network verification by using exponential and gradient-guided search to skip subproblems on the way to each path's verdict boundary, cutting average verification time by 17–30%.
-
Certified Training for Convolutional Perturbations
A certified-training method using parameterized blur kernels and symbolic bound propagation gives provable robustness to motion blur and related convolutional perturbations, reaching over 80% verified accuracy on CIFAR10.
-
Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
Reordering branch-and-bound sub-problems by a counterexample-potentiality heuristic accelerates neural network verification, especially for falsified instances.
Discussion (0). Sign in to comment.