Online Verification of Deep Neural Networks under Domain or Weight Shift

• URL: http://arxiv.org/abs/2106.12732v1
• Date: Thu, 24 Jun 2021 02:38:27 GMT
• Title: Online Verification of Deep Neural Networks under Domain or Weight Shift
• Authors: Tianhao Wei, Changliu Liu
• Abstract summary: Existing verification methods are limited to relatively simple specifications and fixed networks. We propose three types of techniques to accelerate the online verification of deep neural networks. Experiment results show that our online verification algorithm is up to two orders of magnitude faster than existing verification algorithms.
• Score: 2.512827436728378
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Although neural networks are widely used, it remains challenging to formally verify the safety and robustness of neural networks in real-world applications. Existing methods are designed to verify the network before use, which is limited to relatively simple specifications and fixed networks. These methods are not ready to be applied to real-world problems with complex and/or dynamically changing specifications and networks. To effectively handle dynamically changing specifications and networks, the verification needs to be performed online when these changes take place. However, it is still challenging to run existing verification algorithms online. Our key insight is that we can leverage the temporal dependencies of these changes to accelerate the verification process, e.g., by warm starting new online verification using previous verified results. This paper establishes a novel framework for scalable online verification to solve real-world verification problems with dynamically changing specifications and/or networks, known as domain shift and weight shift respectively. We propose three types of techniques (branch management, perturbation tolerance analysis, and incremental computation) to accelerate the online verification of deep neural networks. Experiment results show that our online verification algorithm is up to two orders of magnitude faster than existing verification algorithms, and thus can scale to real-world applications.

Related papers

• Expediting Neural Network Verification via Network Reduction [4.8621567234713305]
  We propose a network reduction technique as a pre-processing method prior to verification. The proposed method reduces neural networks via eliminating stable ReLU neurons, and transforming them into a sequential neural network. We instantiate the reduction technique on the state-of-the-art complete and incomplete verification tools.
  arXiv  Detail & Related papers  (2023-08-07T06:23:24Z)
• 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)
• Dynamics-aware Adversarial Attack of Adaptive Neural Networks [75.50214601278455]
  We investigate the dynamics-aware adversarial attack problem of adaptive neural networks. We propose a Leaded Gradient Method (LGM) and show the significant effects of the lagged gradient. Our LGM achieves impressive adversarial attack performance compared with the dynamic-unaware attack methods.
  arXiv  Detail & Related papers  (2022-10-15T01:32:08Z)
• Neural Network Verification using Residual Reasoning [0.0]
  We present an enhancement to abstraction-based verification of neural networks, by using emphresidual reasoning. In essence, the method allows the verifier to store information about parts of the search space in which the refined network is guaranteed to behave correctly.
  arXiv  Detail & Related papers  (2022-08-05T10:39:04Z)
• CheckINN: Wide Range Neural Network Verification in Imandra [0.0]
  We show how Imandra, a functional programming language and a theorem prover can offer a holistic infrastructure for neural network verification. We develop a novel library CheckINN that formalises neural networks in Imandra, and covers different important facets of neural network verification.
  arXiv  Detail & Related papers  (2022-07-21T16:06:58Z)
• Learning Fast and Slow for Online Time Series Forecasting [76.50127663309604]
  Fast and Slow learning Networks (FSNet) is a holistic framework for online time-series forecasting. FSNet balances fast adaptation to recent changes and retrieving similar old knowledge. Our code will be made publicly available.
  arXiv  Detail & Related papers  (2022-02-23T18:23:07Z)
• Towards Repairing Neural Networks Correctly [6.600380575920419]
  We propose a runtime verification method to ensure the correctness of neural networks. Experiment results show that our approach effectively generates neural networks which are guaranteed to satisfy the properties.
  arXiv  Detail & Related papers  (2020-12-03T12:31:07Z)
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming [97.40955121478716]
  We propose a first-order dual SDP algorithm that requires memory only linear in the total number of network activations. We significantly improve L-inf verified robust accuracy from 1% to 88% and 6% to 40% respectively. We also demonstrate tight verification of a quadratic stability specification for the decoder of a variational autoencoder.
  arXiv  Detail & Related papers  (2020-10-22T12:32:29Z)
• Network Adjustment: Channel Search Guided by FLOPs Utilization Ratio [101.84651388520584]
  This paper presents a new framework named network adjustment, which considers network accuracy as a function of FLOPs. Experiments on standard image classification datasets and a wide range of base networks demonstrate the effectiveness of our approach.
  arXiv  Detail & Related papers  (2020-04-06T15:51:00Z)
• Verifying Recurrent Neural Networks using Invariant Inference [0.0]
  We propose a novel approach for verifying properties of a widespread variant of neural networks, called recurrent neural networks. Our approach is based on the inference of invariants, which allow us to reduce the complex problem of verifying recurrent networks into simpler, non-recurrent problems.
  arXiv  Detail & Related papers  (2020-04-06T08:08:24Z)
• Robustness Verification for Transformers [165.25112192811764]
  We develop the first robustness verification algorithm for Transformers. The certified robustness bounds computed by our method are significantly tighter than those by naive Interval Bound propagation. These bounds also shed light on interpreting Transformers as they consistently reflect the importance of different words in sentiment analysis.
  arXiv  Detail & Related papers  (2020-02-16T17:16:31Z)

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.