Verifying Low-dimensional Input Neural Networks via Input Quantization

• URL: http://arxiv.org/abs/2108.07961v1
• Date: Wed, 18 Aug 2021 03:42:05 GMT
• Title: Verifying Low-dimensional Input Neural Networks via Input Quantization
• Authors: Kai Jia, Martin Rinard
• Abstract summary: This paper revisits the original problem of verifying ACAS Xu networks. We propose to prepend an input quantization layer to the network. Our technique can deliver exact verification results immune to floating-point error.
• Score: 12.42030531015912
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Deep neural networks are an attractive tool for compressing the control policy lookup tables in systems such as the Airborne Collision Avoidance System (ACAS). It is vital to ensure the safety of such neural controllers via verification techniques. The problem of analyzing ACAS Xu networks has motivated many successful neural network verifiers. These verifiers typically analyze the internal computation of neural networks to decide whether a property regarding the input/output holds. The intrinsic complexity of neural network computation renders such verifiers slow to run and vulnerable to floating-point error. This paper revisits the original problem of verifying ACAS Xu networks. The networks take low-dimensional sensory inputs with training data provided by a precomputed lookup table. We propose to prepend an input quantization layer to the network. Quantization allows efficient verification via input state enumeration, whose complexity is bounded by the size of the quantization space. Quantization is equivalent to nearest-neighbor interpolation at run time, which has been shown to provide acceptable accuracy for ACAS in simulation. Moreover, our technique can deliver exact verification results immune to floating-point error if we directly enumerate the network outputs on the target inference implementation or on an accurate simulation of the target implementation.

Related papers

• VeriFlow: Modeling Distributions for Neural Network Verification [4.3012765978447565]
  Formal verification has emerged as a promising method to ensure the safety and reliability of neural networks. We propose the VeriFlow architecture as a flow based density model tailored to allow any verification approach to restrict its search to the some data distribution of interest.
  arXiv  Detail & Related papers  (2024-06-20T12:41:39Z)
• 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)
• Signal Detection in MIMO Systems with Hardware Imperfections: Message Passing on Neural Networks [101.59367762974371]
  In this paper, we investigate signal detection in multiple-input-multiple-output (MIMO) communication systems with hardware impairments. It is difficult to train a deep neural network (DNN) with limited pilot signals, hindering its practical applications. We design an efficient message passing based Bayesian signal detector, leveraging the unitary approximate message passing (UAMP) algorithm.
  arXiv  Detail & Related papers  (2022-10-08T04:32:58Z)
• SignalNet: A Low Resolution Sinusoid Decomposition and Estimation Network [79.04274563889548]
  We propose SignalNet, a neural network architecture that detects the number of sinusoids and estimates their parameters from quantized in-phase and quadrature samples. We introduce a worst-case learning threshold for comparing the results of our network relative to the underlying data distributions. In simulation, we find that our algorithm is always able to surpass the threshold for three-bit data but often cannot exceed the threshold for one-bit data.
  arXiv  Detail & Related papers  (2021-06-10T04:21:20Z)
• DAAIN: Detection of Anomalous and Adversarial Input using Normalizing Flows [52.31831255787147]
  We introduce a novel technique, DAAIN, to detect out-of-distribution (OOD) inputs and adversarial attacks (AA) Our approach monitors the inner workings of a neural network and learns a density estimator of the activation distribution. Our model can be trained on a single GPU making it compute efficient and deployable without requiring specialized accelerators.
  arXiv  Detail & Related papers  (2021-05-30T22:07:13Z)
• Scalable Verification of Quantized Neural Networks (Technical Report) [14.04927063847749]
  We show that bit-exact implementation of quantized neural networks with bit-vector specifications is PSPACE-hard. We propose three techniques for making SMT-based verification of quantized neural networks more scalable.
  arXiv  Detail & Related papers  (2020-12-15T10:05:37Z)
• Neural-network-based parameter estimation for quantum detection [0.0]
  In the context of quantum detection schemes, neural networks find a natural playground. We demonstrate that adequately trained neural networks enable to characterize a target with minimal knowledge of the underlying physical model. We exemplify the method with a development for $171$Yb$+$ atomic sensors.
  arXiv  Detail & Related papers  (2020-12-14T16:26:05Z)
• 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)
• AQD: Towards Accurate Fully-Quantized Object Detection [94.06347866374927]
  We propose an Accurate Quantized object Detection solution, termed AQD, to get rid of floating-point computation. Our AQD achieves comparable or even better performance compared with the full-precision counterpart under extremely low-bit schemes.
  arXiv  Detail & Related papers  (2020-07-14T09:07:29Z)
• Exploiting Verified Neural Networks via Floating Point Numerical Error [15.639601066641099]
  Verifiers aspire to answer whether a neural network guarantees certain properties with respect to all inputs in a space. We show that the negligence of floating point error leads to unsound verification that can be systematically exploited in practice.
  arXiv  Detail & Related papers  (2020-03-06T03:58:26Z)

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.