Pruning and Slicing Neural Networks using Formal Verification

• URL: http://arxiv.org/abs/2105.13649v1
• Date: Fri, 28 May 2021 07:53:50 GMT
• Title: Pruning and Slicing Neural Networks using Formal Verification
• Authors: Ori Lahav, Guy Katz
• Abstract summary: Deep neural networks (DNNs) play an increasingly important role in various computer systems. In order to create these networks, engineers typically specify a desired topology, and then use an automated training algorithm to select the network's weights. Here, we propose to address this challenge by harnessing recent advances in DNN verification.
• Score: 0.2538209532048866
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Deep neural networks (DNNs) play an increasingly important role in various computer systems. In order to create these networks, engineers typically specify a desired topology, and then use an automated training algorithm to select the network's weights. While training algorithms have been studied extensively and are well understood, the selection of topology remains a form of art, and can often result in networks that are unnecessarily large - and consequently are incompatible with end devices that have limited memory, battery or computational power. Here, we propose to address this challenge by harnessing recent advances in DNN verification. We present a framework and a methodology for discovering redundancies in DNNs - i.e., for finding neurons that are not needed, and can be removed in order to reduce the size of the DNN. By using sound verification techniques, we can formally guarantee that our simplified network is equivalent to the original, either completely, or up to a prescribed tolerance. Further, we show how to combine our technique with slicing, which results in a family of very small DNNs, which are together equivalent to the original. Our approach can produce DNNs that are significantly smaller than the original, rendering them suitable for deployment on additional kinds of systems, and even more amenable to subsequent formal verification. We provide a proof-of-concept implementation of our approach, and use it to evaluate our techniques on several real-world DNNs.

Related papers

• 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)
• QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks [14.766917269393865]
  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.
  arXiv  Detail & Related papers  (2022-12-10T03:00:29Z)
• 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)
• You Can Have Better Graph Neural Networks by Not Training Weights at All: Finding Untrained GNNs Tickets [105.24703398193843]
  Untrainedworks in graph neural networks (GNNs) still remains mysterious. We show that the found untrainedworks can substantially mitigate the GNN over-smoothing problem. We also observe that such sparse untrainedworks have appealing performance in out-of-distribution detection and robustness of input perturbations.
  arXiv  Detail & Related papers  (2022-11-28T14:17:36Z)
• Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training [14.787056022080625]
  This paper presents a novel abstraction-based approach to bypass the crux of over-approximating DNNs in reachability analysis. We extend conventional DNNs by inserting an additional abstraction layer, which abstracts a real number to an interval for training. We devise the first black-box reachability analysis approach for DNN-controlled systems, where trained DNNs are only queried as black-box oracles for the actions on abstract states.
  arXiv  Detail & Related papers  (2022-11-21T00:11:50Z)
• Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks [64.23331120621118]
  We use interval reachability analysis to obtain robustness guarantees for implicit neural networks (INNs) INNs are a class of implicit learning models that use implicit equations as layers. We show that our approach performs at least as well as, and generally better than, applying state-of-the-art interval bound propagation methods to INNs.
  arXiv  Detail & Related papers  (2022-04-01T03:31:27Z)
• Neural Network Branch-and-Bound for Neural Network Verification [26.609606492971967]
  We propose a novel machine learning framework that can be used for designing an effective branching strategy. We learn two graph neural networks (GNNs) that both directly treat the network we want to verify as a graph input. We show that our GNN models generalize well to harder properties on larger unseen networks.
  arXiv  Detail & Related papers  (2021-07-27T14:42:57Z)
• Overcoming Catastrophic Forgetting in Graph Neural Networks [50.900153089330175]
  Catastrophic forgetting refers to the tendency that a neural network "forgets" the previous learned knowledge upon learning new tasks. We propose a novel scheme dedicated to overcoming this problem and hence strengthen continual learning in graph neural networks (GNNs) At the heart of our approach is a generic module, termed as topology-aware weight preserving(TWP)
  arXiv  Detail & Related papers  (2020-12-10T22:30:25Z)
• DiffRNN: Differential Verification of Recurrent Neural Networks [3.4423518864863154]
  Recurrent neural networks (RNNs) have become popular in a variety of applications such as image processing, data classification, speech recognition, and as controllers in autonomous systems. We propose DIFFRNN, the first differential verification method for RNNs to certify the equivalence of two structurally similar neural networks. We demonstrate the practical efficacy of our technique on a variety of benchmarks and show that DIFFRNN outperforms state-of-the-art verification tools such as POPQORN.
  arXiv  Detail & Related papers  (2020-07-20T14:14:35Z)
• 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)
• 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)

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.