Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes

• URL: http://arxiv.org/abs/2501.00200v1
• Date: Tue, 31 Dec 2024 00:43:11 GMT
• Title: Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes
• Authors: Duo Zhou, Christopher Brix, Grani A Hanasusanto, Huan Zhang,
• Abstract summary: We develop Branch-and-bound Inferred Cuts with COnstraint Strengthening (BICCOS) BICCOS is part of the $alpha,beta$-CROWN verifier, the VNN-COMP 2024 winner.
• Score: 9.061956085975519
• License:
• Abstract: Recently, cutting-plane methods such as GCP-CROWN have been explored to enhance neural network verifiers and made significant advances. However, GCP-CROWN currently relies on generic cutting planes (cuts) generated from external mixed integer programming (MIP) solvers. Due to the poor scalability of MIP solvers, large neural networks cannot benefit from these cutting planes. In this paper, we exploit the structure of the neural network verification problem to generate efficient and scalable cutting planes specific for this problem setting. We propose a novel approach, Branch-and-bound Inferred Cuts with COnstraint Strengthening (BICCOS), which leverages the logical relationships of neurons within verified subproblems in the branch-and-bound search tree, and we introduce cuts that preclude these relationships in other subproblems. We develop a mechanism that assigns influence scores to neurons in each path to allow the strengthening of these cuts. Furthermore, we design a multi-tree search technique to identify more cuts, effectively narrowing the search space and accelerating the BaB algorithm. Our results demonstrate that BICCOS can generate hundreds of useful cuts during the branch-and-bound process and consistently increase the number of verifiable instances compared to other state-of-the-art neural network verifiers on a wide range of benchmarks, including large networks that previous cutting plane methods could not scale to. BICCOS is part of the $\alpha,\beta$-CROWN verifier, the VNN-COMP 2024 winner. The code is available at http://github.com/Lemutisme/BICCOS .

Related papers

• Learning Cut Generating Functions for Integer Programming [1.1510009152620668]
  The branch-and-cut algorithm is the method of choice to solve large scale integer programming problems. Recent advances have employed a data-driven approach to select optimal cutting planes from a parameterized family. We show that the selected CGF can outperform the GMI cuts for certain distributions.
  arXiv  Detail & Related papers  (2024-05-22T20:56:34Z)
• General Cutting Planes for Bound-Propagation-Based Neural Network Verification [144.7290035694459]
  We generalize the bound propagation procedure to allow the addition of arbitrary cutting plane constraints. We find that MIP solvers can generate high-quality cutting planes for strengthening bound-propagation-based verifiers. Our method is the first verifier that can completely solve the oval20 benchmark and verify twice as many instances on the oval21 benchmark.
  arXiv  Detail & Related papers  (2022-08-11T10:31:28Z)
• SAR Despeckling Using Overcomplete Convolutional Networks [53.99620005035804]
  despeckling is an important problem in remote sensing as speckle degrades SAR images. Recent studies show that convolutional neural networks(CNNs) outperform classical despeckling methods. This study employs an overcomplete CNN architecture to focus on learning low-level features by restricting the receptive field. We show that the proposed network improves despeckling performance compared to recent despeckling methods on synthetic and real SAR images.
  arXiv  Detail & Related papers  (2022-05-31T15:55:37Z)
• An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks [0.0]
  We present the Cnn-Abs framework, which is aimed at the verification of convolutional networks. The core of Cnn-Abs is an abstraction-refinement technique, which simplifies the verification problem. Cnn-Abs can significantly boost the performance of a state-of-the-art verification engine, reducing runtime by 15.7% on average.
  arXiv  Detail & Related papers  (2022-01-06T08:57:43Z)
• Learning to Detect Critical Nodes in Sparse Graphs via Feature Importance Awareness [53.351863569314794]
  The critical node problem (CNP) aims to find a set of critical nodes from a network whose deletion maximally degrades the pairwise connectivity of the residual network. This work proposes a feature importance-aware graph attention network for node representation. It combines it with dueling double deep Q-network to create an end-to-end algorithm to solve CNP for the first time.
  arXiv  Detail & Related papers  (2021-12-03T14:23:05Z)
• Second-Order Component Analysis for Fault Detection [0.0]
  High-order neural networks might bring the risk of overfitting and learning both the key information from original data and noises or anomalies. This paper proposes a novel fault detection method called second-order component analysis (SCA)
  arXiv  Detail & Related papers  (2021-03-12T14:25:37Z)
• An Uncertainty-Driven GCN Refinement Strategy for Organ Segmentation [53.425900196763756]
  We propose a segmentation refinement method based on uncertainty analysis and graph convolutional networks. We employ the uncertainty levels of the convolutional network in a particular input volume to formulate a semi-supervised graph learning problem. We show that our method outperforms the state-of-the-art CRF refinement method by improving the dice score by 1% for the pancreas and 2% for spleen.
  arXiv  Detail & Related papers  (2020-12-06T18:55:07Z)
• A Sequential Framework Towards an Exact SDP Verification of Neural Networks [14.191310794366075]
  A number of techniques based on convex optimization have been proposed in the literature to study the robustness of neural networks. The challenge to a robust certification approach is that it is prone to a large relaxation gap. In this work, we address the issue by developing a sequential programming framework to shrink this gap to zero.
  arXiv  Detail & Related papers  (2020-10-16T19:45:11Z)
• ESPN: Extremely Sparse Pruned Networks [50.436905934791035]
  We show that a simple iterative mask discovery method can achieve state-of-the-art compression of very deep networks. Our algorithm represents a hybrid approach between single shot network pruning methods and Lottery-Ticket type approaches.
  arXiv  Detail & Related papers  (2020-06-28T23:09:27Z)
• DHP: Differentiable Meta Pruning via HyperNetworks [158.69345612783198]
  This paper introduces a differentiable pruning method via hypernetworks for automatic network pruning. Latent vectors control the output channels of the convolutional layers in the backbone network and act as a handle for the pruning of the layers. Experiments are conducted on various networks for image classification, single image super-resolution, and denoising.
  arXiv  Detail & Related papers  (2020-03-30T17:59:18Z)

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.