Scalable Verification of Quantized Neural Networks (Technical Report)

• URL: http://arxiv.org/abs/2012.08185v1
• Date: Tue, 15 Dec 2020 10:05:37 GMT
• Title: Scalable Verification of Quantized Neural Networks (Technical Report)
• Authors: Thomas A. Henzinger, Mathias Lechner, {\DJ}or{\dj}e \v{Z}ikeli\'c
• Abstract summary: 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.
• Score: 14.04927063847749
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for verification of an idealized model of the actual network which works over real arithmetic and ignores rounding imprecisions. This idealization is in stark contrast to network quantization, which is a technique that trades numerical precision for computational efficiency and is, therefore, often applied in practice. Neglecting rounding errors of such low-bit quantized neural networks has been shown to lead to wrong conclusions about the network's correctness. Thus, the desired approach for verifying quantized neural networks would be one that takes these rounding errors into account. In this paper, we show that verifying the bit-exact implementation of quantized neural networks with bit-vector specifications is PSPACE-hard, even though verifying idealized real-valued networks and satisfiability of bit-vector specifications alone are each in NP. Furthermore, we explore several practical heuristics toward closing the complexity gap between idealized and bit-exact verification. In particular, we propose three techniques for making SMT-based verification of quantized neural networks more scalable. Our experiments demonstrate that our proposed methods allow a speedup of up to three orders of magnitude over existing approaches.

Related papers

• Verified Neural Compressed Sensing [58.98637799432153]
  We develop the first (to the best of our knowledge) provably correct neural networks for a precise computational task. We show that for modest problem dimensions (up to 50), we can train neural networks that provably recover a sparse vector from linear and binarized linear measurements. We show that the complexity of the network can be adapted to the problem difficulty and solve problems where traditional compressed sensing methods are not known to provably work.
  arXiv  Detail & Related papers  (2024-05-07T12:20:12Z)
• On the Convergence of Locally Adaptive and Scalable Diffusion-Based Sampling Methods for Deep Bayesian Neural Network Posteriors [2.3265565167163906]
  Bayesian neural networks are a promising approach for modeling uncertainties in deep neural networks. generating samples from the posterior distribution of neural networks is a major challenge. One advance in that direction would be the incorporation of adaptive step sizes into Monte Carlo Markov chain sampling algorithms. In this paper, we demonstrate that these methods can have a substantial bias in the distribution they sample, even in the limit of vanishing step sizes and at full batch size.
  arXiv  Detail & Related papers  (2024-03-13T15:21:14Z)
• 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)
• CEG4N: Counter-Example Guided Neural Network Quantization Refinement [2.722899166098862]
  We propose Counter-Example Guided Neural Network Quantization Refinement (CEG4N) This technique combines search-based quantization and equivalence verification. We produce models with up to 72% better accuracy than state-of-the-art techniques.
  arXiv  Detail & Related papers  (2022-07-09T09:25:45Z)
• Post-training Quantization for Neural Networks with Provable Guarantees [9.58246628652846]
  We modify a post-training neural-network quantization method, GPFQ, that is based on a greedy path-following mechanism. We prove that for quantizing a single-layer network, the relative square error essentially decays linearly in the number of weights.
  arXiv  Detail & Related papers  (2022-01-26T18:47:38Z)
• Why Lottery Ticket Wins? A Theoretical Perspective of Sample Complexity on Pruned Neural Networks [79.74580058178594]
  We analyze the performance of training a pruned neural network by analyzing the geometric structure of the objective function. We show that the convex region near a desirable model with guaranteed generalization enlarges as the neural network model is pruned.
  arXiv  Detail & Related papers  (2021-10-12T01:11:07Z)
• Searching for Low-Bit Weights in Quantized Neural Networks [129.8319019563356]
  Quantized neural networks with low-bit weights and activations are attractive for developing AI accelerators. We present to regard the discrete weights in an arbitrary quantized neural network as searchable variables, and utilize a differential method to search them accurately.
  arXiv  Detail & Related papers  (2020-09-18T09:13:26Z)
• 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)
• 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.