An SMT-Based Approach for Verifying Binarized Neural Networks

• URL: http://arxiv.org/abs/2011.02948v2
• Date: Sun, 17 Jan 2021 08:41:37 GMT
• Title: An SMT-Based Approach for Verifying Binarized Neural Networks
• Authors: Guy Amir, Haoze Wu, Clark Barrett and Guy Katz
• Abstract summary: We propose an SMT-based technique for verifying Binarized Neural Networks. One novelty of our technique is that it allows the verification of neural networks that include both binarized and non-binarized components. We implement our technique as an extension to the Marabou framework, and use it to evaluate the approach on popular binarized neural network architectures.
• Score: 1.4394939014120451
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Deep learning has emerged as an effective approach for creating modern software systems, with neural networks often surpassing hand-crafted systems. Unfortunately, neural networks are known to suffer from various safety and security issues. Formal verification is a promising avenue for tackling this difficulty, by formally certifying that networks are correct. We propose an SMT-based technique for verifying Binarized Neural Networks - a popular kind of neural network, where some weights have been binarized in order to render the neural network more memory and energy efficient, and quicker to evaluate. One novelty of our technique is that it allows the verification of neural networks that include both binarized and non-binarized components. Neural network verification is computationally very difficult, and so we propose here various optimizations, integrated into our SMT procedure as deduction steps, as well as an approach for parallelizing verification queries. We implement our technique as an extension to the Marabou framework, and use it to evaluate the approach on popular binarized neural network architectures.

Related papers

• Graph Neural Networks for Learning Equivariant Representations of Neural Networks [55.04145324152541]
  We propose to represent neural networks as computational graphs of parameters. Our approach enables a single model to encode neural computational graphs with diverse architectures. We showcase the effectiveness of our method on a wide range of tasks, including classification and editing of implicit neural representations.
  arXiv  Detail & Related papers  (2024-03-18T18:01:01Z)
• Set-Based Training for Neural Network Verification [8.97708612393722]
  Small input perturbations can significantly affect the outputs of a neural network. In safety-critical environments, the inputs often contain noisy sensor data. We employ an end-to-end set-based training procedure that trains robust neural networks for formal verification.
  arXiv  Detail & Related papers  (2024-01-26T15:52:41Z)
• NeuralFastLAS: Fast Logic-Based Learning from Raw Data [54.938128496934695]
  Symbolic rule learners generate interpretable solutions, however they require the input to be encoded symbolically. Neuro-symbolic approaches overcome this issue by mapping raw data to latent symbolic concepts using a neural network. We introduce NeuralFastLAS, a scalable and fast end-to-end approach that trains a neural network jointly with a symbolic learner.
  arXiv  Detail & Related papers  (2023-10-08T12:33:42Z)
• Enhanced quantum state preparation via stochastic prediction of neural network [0.8287206589886881]
  In this paper, we explore an intriguing avenue for enhancing algorithm effectiveness through exploiting the knowledge blindness of neural network. Our approach centers around a machine learning algorithm utilized for preparing arbitrary quantum states in a semiconductor double quantum dot system. By leveraging prediction generated by the neural network, we are able to guide the optimization process to escape local optima.
  arXiv  Detail & Related papers  (2023-07-27T09:11:53Z)
• A Hybrid Neural Coding Approach for Pattern Recognition with Spiking Neural Networks [53.31941519245432]
  Brain-inspired spiking neural networks (SNNs) have demonstrated promising capabilities in solving pattern recognition tasks. These SNNs are grounded on homogeneous neurons that utilize a uniform neural coding for information representation. In this study, we argue that SNN architectures should be holistically designed to incorporate heterogeneous coding schemes.
  arXiv  Detail & Related papers  (2023-05-26T02:52:12Z)
• Deep Learning Meets Sparse Regularization: A Signal Processing Perspective [17.12783792226575]
  We present a mathematical framework that characterizes the functional properties of neural networks that are trained to fit to data. Key mathematical tools which support this framework include transform-domain sparse regularization, the Radon transform of computed tomography, and approximation theory. This framework explains the effect of weight decay regularization in neural network training, the use of skip connections and low-rank weight matrices in network architectures, the role of sparsity in neural networks, and explains why neural networks can perform well in high-dimensional problems.
  arXiv  Detail & Related papers  (2023-01-23T17:16:21Z)
• 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)
• Local Critic Training for Model-Parallel Learning of Deep Neural Networks [94.69202357137452]
  We propose a novel model-parallel learning method, called local critic training. We show that the proposed approach successfully decouples the update process of the layer groups for both convolutional neural networks (CNNs) and recurrent neural networks (RNNs) We also show that trained networks by the proposed method can be used for structural optimization.
  arXiv  Detail & Related papers  (2021-02-03T09:30:45Z)
• 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)
• Progressive Tandem Learning for Pattern Recognition with Deep Spiking Neural Networks [80.15411508088522]
  Spiking neural networks (SNNs) have shown advantages over traditional artificial neural networks (ANNs) for low latency and high computational efficiency. We propose a novel ANN-to-SNN conversion and layer-wise learning framework for rapid and efficient pattern recognition.
  arXiv  Detail & Related papers  (2020-07-02T15:38:44Z)
• Exploring the Connection Between Binary and Spiking Neural Networks [1.329054857829016]
  We bridge the recent algorithmic progress in training Binary Neural Networks and Spiking Neural Networks. We show that training Spiking Neural Networks in the extreme quantization regime results in near full precision accuracies on large-scale datasets.
  arXiv  Detail & Related papers  (2020-02-24T03:46:51Z)

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.