REVIEW 6 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
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 6 Pith papers
-
Semantic Robustness Certification for Vision-Language Models
Framework certifies VLM robustness under semantic transformations via text prompt proxies, enabling quantitative certification of safe extent intervals without per-variation data.
-
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.
-
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...
-
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.
-
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.
Discussion (0). Sign in to comment.