Neural Network Verification with Branch-and-Bound for General Nonlinearities

• URL: http://arxiv.org/abs/2405.21063v2
• Date: Wed, 13 Nov 2024 08:13:36 GMT
• Title: Neural Network Verification with Branch-and-Bound for General Nonlinearities
• Authors: Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh, Huan Zhang,
• Abstract summary: Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification. We develop a general framework, named GenBaB, to conduct BaB on general nonlinearities to verify NNs with general architectures. 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.
• Score: 63.39918329535165
• License:
• 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).

Related papers

• Forward Learning of Graph Neural Networks [17.79590285482424]
  Backpropagation (BP) is the de facto standard for training deep neural networks (NNs) BP imposes several constraints, which are not only biologically implausible, but also limit the scalability, parallelism, and flexibility in learning NNs. We propose ForwardGNN, which avoids the constraints imposed by BP via an effective layer-wise local forward training.
  arXiv  Detail & Related papers  (2024-03-16T19:40:35Z)
• Provably Safe Neural Network Controllers via Differential Dynamic Logic [2.416907802598482]
  We present the first general approach that allows reusing control theory results for NNCS verification. Based on provably safe control envelopes in dL, we derive specifications for the NN which is proven via NN verification. We show that a proof of the NN adhering to the specification is mirrored by a dL proof on the infinite-time safety of the NNCS.
  arXiv  Detail & Related papers  (2024-02-16T16:15:25Z)
• Benign Overfitting in Deep Neural Networks under Lazy Training [72.28294823115502]
  We show that when the data distribution is well-separated, DNNs can achieve Bayes-optimal test error for classification. Our results indicate that interpolating with smoother functions leads to better generalization.
  arXiv  Detail & Related papers  (2023-05-30T19:37:44Z)
• Posterior Regularized Bayesian Neural Network Incorporating Soft and Hard Knowledge Constraints [12.050265348673078]
  We propose a novel Posterior-Regularized Bayesian Neural Network (PR-BNN) model by incorporating different types of knowledge constraints. Experiments in simulation and two case studies about aviation landing prediction and solar energy output prediction have shown the knowledge constraints and the performance improvement of the proposed model.
  arXiv  Detail & Related papers  (2022-10-16T18:58:50Z)
• Recurrent Bilinear Optimization for Binary Neural Networks [58.972212365275595]
  BNNs neglect the intrinsic bilinear relationship of real-valued weights and scale factors. Our work is the first attempt to optimize BNNs from the bilinear perspective. We obtain robust RBONNs, which show impressive performance over state-of-the-art BNNs on various models and datasets.
  arXiv  Detail & Related papers  (2022-09-04T06:45:33Z)
• On Feature Learning in Neural Networks with Global Convergence Guarantees [49.870593940818715]
  We study the optimization of wide neural networks (NNs) via gradient flow (GF) We show that when the input dimension is no less than the size of the training set, the training loss converges to zero at a linear rate under GF. We also show empirically that, unlike in the Neural Tangent Kernel (NTK) regime, our multi-layer model exhibits feature learning and can achieve better generalization performance than its NTK counterpart.
  arXiv  Detail & Related papers  (2022-04-22T15:56:43Z)
• Neural Network Branch-and-Bound for Neural Network Verification [26.609606492971967]
  We propose a novel machine learning framework that can be used for designing an effective branching strategy. We learn two graph neural networks (GNNs) that both directly treat the network we want to verify as a graph input. We show that our GNN models generalize well to harder properties on larger unseen networks.
  arXiv  Detail & Related papers  (2021-07-27T14:42:57Z)
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition [161.09660864941603]
  We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. We present a novel activation-based branching strategy and a BaB framework, named Branch and Dual Network Bound (BaDNB) BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial properties.
  arXiv  Detail & Related papers  (2021-04-14T09:22:42Z)
• Binarized Graph Neural Network [65.20589262811677]
  We develop a binarized graph neural network to learn the binary representations of the nodes with binary network parameters. Our proposed method can be seamlessly integrated into the existing GNN-based embedding approaches. Experiments indicate that the proposed binarized graph neural network, namely BGN, is orders of magnitude more efficient in terms of both time and space.
  arXiv  Detail & Related papers  (2020-04-19T09:43:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.