REVIEW 7 cited by
Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound
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
Signed reviews
read the original abstract
State-of-the-art neural network verifiers are fundamentally based on one of two paradigms: either encoding the whole verification problem via tight multi-neuron convex relaxations or applying a Branch-and-Bound (BaB) procedure leveraging imprecise but fast bounding methods on a large number of easier subproblems. The former can capture complex multi-neuron dependencies but sacrifices completeness due to the inherent limitations of convex relaxations. The latter enables complete verification but becomes increasingly ineffective on larger and more challenging networks. In this work, we present a novel complete verifier which combines the strengths of both paradigms: it leverages multi-neuron relaxations to drastically reduce the number of subproblems generated during the BaB process and an efficient GPU-based dual optimizer to solve the remaining ones. An extensive evaluation demonstrates that our verifier achieves a new state-of-the-art on both established benchmarks as well as networks with significantly higher accuracy than previously considered. The latter result (up to 28% certification gains) indicates meaningful progress towards creating verifiers that can handle practically relevant networks.
Forward citations
Cited by 7 Pith papers
-
Towards Verified and Targeted Explanations through Formal Methods
ViTaX certifies targeted semifactual robustness: a minimal feature subset can be perturbed by ε without flipping a neural network from class y to a user-specified high-risk class t.
-
Fast SDP certification of neural networks : towards large multi-class datasets
An untargeted SDP relaxation certifies full multi-class ReLU robustness in a single solve, with stable-active neuron pruning that shrinks the matrices and accelerates convergence.
-
Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification
A DQfD-trained ReLU-splitting policy modestly improves Marabou's average verification time on ACAS Xu, but not the number of iterations as claimed.
-
Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification
ABONN orders branch-and-bound sub-problems by a counterexample potentiality score and reports speedups of up to 15.2x on MNIST and 24.7x on CIFAR-10 over a naive branch-and-bound baseline.
-
BaB-ND: Long-Horizon Motion Planning with Branch-and-Bound and Neural Dynamics
A GPU-accelerated branch-and-bound planner over neural dynamics models uses adapted CROWN bounds to prune subdomains and beat sampling-based and MIP baselines on long-horizon manipulation tasks.
-
A Survey on the Verification of Reinforcement Learning Policies
A unifying taxonomy of post-training RL-policy verification methods along formal/probabilistic, step-wise/multi-step, and guarantee-strength axes, plus benchmark-based tool-selection guidance.
-
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). Continue with ORCID to comment.