Branch and Bound for Piecewise Linear Neural Network Verification

• URL: http://arxiv.org/abs/1909.06588v5
• Date: Tue, 26 Aug 2025 14:58:14 GMT
• Title: Branch and Bound for Piecewise Linear Neural Network Verification
• Authors: Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, M. Pawan Kumar,
• Abstract summary: We propose a family of algorithms based on Branch-and-Bound (BaB)<n>We identify new methods that combine the strengths of multiple existing approaches.<n>We introduce an effective branching strategy on ReLU non-linearities.
• Score: 46.49816596173425
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The success of Deep Learning and its potential use in many safety-critical applications has motivated research on formal verification of Neural Network (NN) models. In this context, verification involves proving or disproving that an NN model satisfies certain input-output properties. Despite the reputation of learned NN models as black boxes, and the theoretical hardness of proving useful properties about them, researchers have been successful in verifying some classes of models by exploiting their piecewise linear structure and taking insights from formal methods such as Satisifiability Modulo Theory. However, these methods are still far from scaling to realistic neural networks. To facilitate progress on this crucial area, we exploit the Mixed Integer Linear Programming (MIP) formulation of verification to propose a family of algorithms based on Branch-and-Bound (BaB). We show that our family contains previous verification methods as special cases. With the help of the BaB framework, we make three key contributions. Firstly, we identify new methods that combine the strengths of multiple existing approaches, accomplishing significant performance improvements over previous state of the art. Secondly, we introduce an effective branching strategy on ReLU non-linearities. This branching strategy allows us to efficiently and successfully deal with high input dimensional problems with convolutional network architecture, on which previous methods fail frequently. Finally, we propose comprehensive test data sets and benchmarks which includes a collection of previously released testcases. We use the data sets to conduct a thorough experimental comparison of existing and new algorithms and to provide an inclusive analysis of the factors impacting the hardness of verification problems.

Related papers

• Learning-Based Testing for Deep Learning: Enhancing Model Robustness with Adversarial Input Prioritization [0.0]
  This project aims to enhance fault detection and model robustness in Deep Neural Networks (DNNs)<n>Our method selects a subset of adversarial inputs with a high likelihood of exposing model faults without relying on architecture-specific characteristics or formal verification.<n>By efficiently organizing test permutations, it uncovers all potential faults significantly faster across various datasets, model architectures, and adversarial attack techniques.
  arXiv  Detail & Related papers  (2025-09-28T16:31:30Z)
• Algorithms for Adversarially Robust Deep Learning [58.656107500646364]
  We discuss recent progress toward designing algorithms that exhibit desirable robustness properties.<n>We present new algorithms that achieve state-of-the-art generalization in medical imaging, molecular identification, and image classification.<n>We propose new attacks and defenses, which represent the frontier of progress toward designing robust language-based agents.
  arXiv  Detail & Related papers  (2025-09-23T14:48:58Z)
• SMLE: Safe Machine Learning via Embedded Overapproximation [4.129133569151574]
  We consider the task of training differentiable ML models guaranteed to satisfy designer-chosen properties. This is very challenging, due to the computational complexity of rigorously verifying and enforcing compliance in modern neural models. We provide an innovative approach based on three components: 1) a general, simple architecture enabling efficient verification with a conservative semantic. We evaluate our approach on properties defined by linear inequalities in regression, and on mutually exclusive classes in multilabel classification.
  arXiv  Detail & Related papers  (2024-09-30T17:19:57Z)
• Visual Prompting Upgrades Neural Network Sparsification: A Data-Model Perspective [64.04617968947697]
  We introduce a novel data-model co-design perspective: to promote superior weight sparsity. Specifically, customized Visual Prompts are mounted to upgrade neural Network sparsification in our proposed VPNs framework.
  arXiv  Detail & Related papers  (2023-12-03T13:50:24Z)
• Inductive Knowledge Graph Completion with GNNs and Rules: An Analysis [18.11743347414004]
  Rule-based methods significantly outperform state-of-the-art methods based on Graph Neural Networks (GNNs) We study a number of variants of a rule-based approach, which are specifically aimed at addressing the aforementioned issues. We find that the resulting models can achieve a performance which is close to that of NBFNet.
  arXiv  Detail & Related papers  (2023-08-14T21:01:29Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  We study the problem of training and certifying adversarially robust quantized neural networks (QNNs) Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization. We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
  arXiv  Detail & Related papers  (2022-11-29T13:32:38Z)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  This work proposes easy to interpret validation diagnostics for multi-dimensional conditional (posterior) density estimators based on NF. It also offers theoretical guarantees based on results of local consistency. This work should help the design of better specified models or drive the development of novel SBI-algorithms.
  arXiv  Detail & Related papers  (2022-11-17T15:48:06Z)
• Gone Fishing: Neural Active Learning with Fisher Embeddings [55.08537975896764]
  There is an increasing need for active learning algorithms that are compatible with deep neural networks. This article introduces BAIT, a practical representation of tractable, and high-performing active learning algorithm for neural networks.
  arXiv  Detail & Related papers  (2021-06-17T17:26:31Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  We develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference. Our approach was able to verify and produce examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods.
  arXiv  Detail & Related papers  (2020-12-21T10:03:44Z)
• Designing Interpretable Approximations to Deep Reinforcement Learning [14.007731268271902]
  Deep neural networks (DNNs) set the bar for algorithm performance. It may not be feasible to actually use such high-performing DNNs in practice. This work seeks to identify reduced models that not only preserve a desired performance level, but also, for example, succinctly explain the latent knowledge represented by a DNN.
  arXiv  Detail & Related papers  (2020-10-28T06:33:09Z)
• Rethinking Generalization of Neural Models: A Named Entity Recognition Case Study [81.11161697133095]
  We take the NER task as a testbed to analyze the generalization behavior of existing models from different perspectives. Experiments with in-depth analyses diagnose the bottleneck of existing neural NER models. As a by-product of this paper, we have open-sourced a project that involves a comprehensive summary of recent NER papers.
  arXiv  Detail & Related papers  (2020-01-12T04:33:53Z)

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.