QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks

• URL: http://arxiv.org/abs/2212.11138v1
• Date: Sat, 10 Dec 2022 03:00:29 GMT
• Title: QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks
• Authors: Yedi Zhang and Zhe Zhao and Fu Song and Min Zhang and Taolue Chen and Jun Sun
• Abstract summary: Quantization has emerged as a promising technique to reduce the size of neural networks with comparable accuracy as their floating-point numbered counterparts. We propose a novel and efficient formal verification approach for QNNs. In particular, we are the first to propose an encoding that reduces the verification problem of QNNs into the solving of integer linear constraints.
• Score: 14.766917269393865
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Deep learning has become a promising programming paradigm in software development, owing to its surprising performance in solving many challenging tasks. Deep neural networks (DNNs) are increasingly being deployed in practice, but are limited on resource-constrained devices owing to their demand for computational power. Quantization has emerged as a promising technique to reduce the size of DNNs with comparable accuracy as their floating-point numbered counterparts. The resulting quantized neural networks (QNNs) can be implemented energy-efficiently. Similar to their floating-point numbered counterparts, quality assurance techniques for QNNs, such as testing and formal verification, are essential but are currently less explored. In this work, we propose a novel and efficient formal verification approach for QNNs. In particular, we are the first to propose an encoding that reduces the verification problem of QNNs into the solving of integer linear constraints, which can be solved using off-the-shelf solvers. Our encoding is both sound and complete. We demonstrate the application of our approach on local robustness verification and maximum robustness radius computation. We implement our approach in a prototype tool QVIP and conduct a thorough evaluation. Experimental results on QNNs with different quantization bits confirm the effectiveness and efficiency of our approach, e.g., two orders of magnitude faster and able to solve more verification tasks in the same time limit than the state-of-the-art methods.

Related papers

• ARQ: A Mixed-Precision Quantization Framework for Accurate and Certifiably Robust DNNs [15.43153209571646]
  Mixed precision quantization has become an important technique for enabling the execution of deep neural networks (DNNs) on limited resource computing platforms. This paper introduces ARQ, an innovative mixed-precision quantization method that not only preserves the clean accuracy of the smoothed classifiers but also maintains their certified robustness.
  arXiv  Detail & Related papers  (2024-10-31T17:59:37Z)
• An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks [13.271286153792058]
  Quantized neural networks (QNNs) have been developed, with binarized neural networks (BNNs) restricted to binary values as a special case. This paper presents an automata-theoretic approach to synthesizing BNNs that meet designated properties.
  arXiv  Detail & Related papers  (2023-07-29T06:27:28Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• QEBVerif: Quantization Error Bound Verification of Neural Networks [6.327780998441913]
  quantization is widely regarded as one promising technique for deploying deep neural networks (DNNs) on edge devices. Existing verification methods focus on either individual neural networks (DNNs or QNNs) or quantization error bound for partial quantization. We propose a quantization error bound verification method, named QEBVerif, where both weights and activation tensors are quantized.
  arXiv  Detail & Related papers  (2022-12-06T06:34:38Z)
• 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)
• Low-bit Shift Network for End-to-End Spoken Language Understanding [7.851607739211987]
  We propose the use of power-of-two quantization, which quantizes continuous parameters into low-bit power-of-two values. This reduces computational complexity by removing expensive multiplication operations and with the use of low-bit weights.
  arXiv  Detail & Related papers  (2022-07-15T14:34:22Z)
• FATNN: Fast and Accurate Ternary Neural Networks [89.07796377047619]
  Ternary Neural Networks (TNNs) have received much attention due to being potentially orders of magnitude faster in inference, as well as more power efficient, than full-precision counterparts. In this work, we show that, under some mild constraints, computational complexity of the ternary inner product can be reduced by a factor of 2. We elaborately design an implementation-dependent ternary quantization algorithm to mitigate the performance gap.
  arXiv  Detail & Related papers  (2020-08-12T04:26:18Z)
• 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)
• Boosting Deep Neural Networks with Geometrical Prior Knowledge: A Survey [77.99182201815763]
  Deep Neural Networks (DNNs) achieve state-of-the-art results in many different problem settings. DNNs are often treated as black box systems, which complicates their evaluation and validation. One promising field, inspired by the success of convolutional neural networks (CNNs) in computer vision tasks, is to incorporate knowledge about symmetric geometrical transformations.
  arXiv  Detail & Related papers  (2020-06-30T14:56:05Z)
• Widening and Squeezing: Towards Accurate and Efficient QNNs [125.172220129257]
  Quantization neural networks (QNNs) are very attractive to the industry because their extremely cheap calculation and storage overhead, but their performance is still worse than that of networks with full-precision parameters. Most of existing methods aim to enhance performance of QNNs especially binary neural networks by exploiting more effective training techniques. We address this problem by projecting features in original full-precision networks to high-dimensional quantization features.
  arXiv  Detail & Related papers  (2020-02-03T04:11:13Z)

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.