REVIEW 9 cited by
Neural Network Verification with Branch-and-Bound for General Nonlinearities
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
Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification. However, existing works on BaB for NN verification have mostly focused on NNs with piecewise linear activations, especially ReLU networks. In this paper, we develop a general framework, named GenBaB, to conduct BaB on general nonlinearities to verify NNs with general architectures, based on linear bound propagation for NN verification. To decide which neuron to branch, we design a new branching heuristic which leverages linear bounds as shortcuts to efficiently estimate the potential improvement after branching. To decide nontrivial branching points for general nonlinear functions, we propose to pre-optimize branching points, which can be efficiently leveraged during verification with a lookup table. We demonstrate the effectiveness of our GenBaB on verifying a wide range of NNs, including NNs with activation functions such as Sigmoid, Tanh, Sine and GeLU, as well as NNs involving multi-dimensional nonlinear operations such as multiplications in LSTMs and Vision Transformers. Our framework also allows the verification of general nonlinear computation graphs and enables verification applications beyond simple NNs, particularly for AC Optimal Power Flow (ACOPF). GenBaB is part of the latest $\alpha$,$\beta$-CROWN, the winner of the 4th and the 5th International Verification of Neural Networks Competition (VNN-COMP 2023 and 2024). Code for reproducing the experiments is available at https://github.com/shizhouxing/GenBaB.
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.
-
Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
A dL/dGL-based method that verifies infinite-horizon safety of neural network controllers under bounded finite-precision perturbations and synthesizes sound mixed-precision fixed-point implementations.
-
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.
-
Neural Network Certification Informed Power System Transient Stability Preventive Control with Renewable Energy
The paper integrates a deep belief network surrogate into optimal power flow and uses α,β-CROWN certification to iteratively adjust the transient stability safety margin under uncertainty.
-
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 Ensembles of Vision-based Safety Control Filters
Ensembles of vision-based safety filters with diverse backbones and aggregation methods improve safe/unsafe classification accuracy over individual models on the DeepAccident dataset.
-
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.
-
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.
-
Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report
A case study shows that differentiable-logic training improves local robustness of a small path-centring network, but current verifiers fail on the regression architecture and the title's 'formally verified' claim is ...
Discussion (0). Continue with ORCID to comment.