REVIEW 9 cited by
Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification
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
abstract
Bound propagation based incomplete neural network verifiers such as CROWN are very efficient and can significantly accelerate branch-and-bound (BaB) based complete verification of neural networks. However, bound propagation cannot fully handle the neuron split constraints introduced by BaB commonly handled by expensive linear programming (LP) solvers, leading to loose bounds and hurting verification efficiency. In this work, we develop $\beta$-CROWN, a new bound propagation based method that can fully encode neuron splits via optimizable parameters $\beta$ constructed from either primal or dual space. When jointly optimized in intermediate layers, $\beta$-CROWN generally produces better bounds than typical LP verifiers with neuron split constraints, while being as efficient and parallelizable as CROWN on GPUs. Applied to complete robustness verification benchmarks, $\beta$-CROWN with BaB is up to three orders of magnitude faster than LP-based BaB methods, and is notably faster than all existing approaches while producing lower timeout rates. By terminating BaB early, our method can also be used for efficient incomplete verification. We consistently achieve higher verified accuracy in many settings compared to powerful incomplete verifiers, including those based on convex barrier breaking techniques. Compared to the typically tightest but very costly semidefinite programming (SDP) based incomplete verifiers, we obtain higher verified accuracy with three orders of magnitudes less verification time. Our algorithm empowered the $\alpha,\!\beta$-CROWN (alpha-beta-CROWN) verifier, the winning tool in VNN-COMP 2021. Our code is available at http://PaperCode.cc/BetaCROWN
Forward citations
Cited by 9 Pith papers
-
Lipschitz-Based Robustness Certification Under Floating-Point Execution
Lipschitz-based robustness certificates that assume real arithmetic can be unsound under floating-point execution; a formal FP-aware theory and certifier close that gap for dense ReLU networks.
-
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...
-
Glitches in Decision Tree Ensemble Models
Introduces glitches as monotonic-oscillation anomalies in decision models and shows that detecting them in tree ensembles is NP-complete.
-
Adversarial Examples Are Not Bugs, They Are Superposition
The paper argues that adversarial examples arise from superposition, and shows that changing superposition changes robustness and vice versa in toy models and ResNet18.
-
A Tensor-Based Compiler and a Runtime for Neuron-Level DNN Certifier Specifications
A compiler with a stack-based IR and shape analysis automatically lifts neuron-level DNN certifier specifications to tensor code, with a g-BSCR sparse backend that is competitive with hand-tuned implementations in sev...
-
Efficient Certified Reasoning for Binarized Neural Networks
A native BNN-aware solver and proof-checking pipeline certifies 99% of qualitative and 86% of quantitative robustness queries, with 9x and 218x speedups over prior certified baselines.
-
A General Framework for Property-Driven Machine Learning
A unified training objective generalizing adversarial training and differentiable-logic constraints, demonstrated on image classification and a drone controller.
-
Learning Verifiable Control Policies Using Relaxed Verification
A loss function built from differentiable reachable-set bounds lets neural control policies be trained to satisfy reach-avoid and invariance specifications, so a lightweight verifier can re-check them at run time.
-
The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results
The 2024 VNN-COMP report documents that GPU-accelerated linear bound propagation with branch-and-bound, led by α,β-CROWN, dominated both the regular and extended tracks.
Discussion (0). Continue with ORCID to comment.