Fully Automatic Neural Network Reduction for Formal Verification

• URL: http://arxiv.org/abs/2305.01932v2
• Date: Tue, 23 Apr 2024 14:45:41 GMT
• Title: Fully Automatic Neural Network Reduction for Formal Verification
• Authors: Tobias Ladner, Matthias Althoff,
• Abstract summary: We introduce a fully automatic and sound reduction of neural networks using reachability analysis. The soundness ensures that the verification of the reduced network entails the verification of the original network. We show that our approach can reduce the number of neurons to a fraction of the original number of neurons with minor outer-approximation.
• Score: 8.017543518311196
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification of neural networks is essential before their deployment in safety-critical applications. However, existing methods for formally verifying neural networks are not yet scalable enough to handle practical problems involving a large number of neurons. We address this challenge by introducing a fully automatic and sound reduction of neural networks using reachability analysis. The soundness ensures that the verification of the reduced network entails the verification of the original network. To the best of our knowledge, we present the first sound reduction approach that is applicable to neural networks with any type of element-wise activation function, such as ReLU, sigmoid, and tanh. The network reduction is computed on the fly while simultaneously verifying the original network and its specifications. All parameters are automatically tuned to minimize the network size without compromising verifiability. We further show the applicability of our approach to convolutional neural networks by explicitly exploiting similar neighboring pixels. Our evaluation shows that our approach can reduce the number of neurons to a fraction of the original number of neurons with minor outer-approximation and thus reduce the verification time to a similar degree.

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)
• 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)
• 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)
• Neural Networks with Sparse Activation Induced by Large Bias: Tighter Analysis with Bias-Generalized NTK [86.45209429863858]
  We study training one-hidden-layer ReLU networks in the neural tangent kernel (NTK) regime. We show that the neural networks possess a different limiting kernel which we call textitbias-generalized NTK We also study various properties of the neural networks with this new kernel.
  arXiv  Detail & Related papers  (2023-01-01T02:11:39Z)
• Spiking neural network for nonlinear regression [68.8204255655161]
  Spiking neural networks carry the potential for a massive reduction in memory and energy consumption. They introduce temporal and neuronal sparsity, which can be exploited by next-generation neuromorphic hardware. A framework for regression using spiking neural networks is proposed.
  arXiv  Detail & Related papers  (2022-10-06T13:04:45Z)
• Consistency of Neural Networks with Regularization [0.0]
  This paper proposes the general framework of neural networks with regularization and prove its consistency. Two types of activation functions: hyperbolic function(Tanh) and rectified linear unit(ReLU) have been taken into consideration.
  arXiv  Detail & Related papers  (2022-06-22T23:33:39Z)
• 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)
• Generate and Verify: Semantically Meaningful Formal Analysis of Neural Network Perception Systems [2.2559617939136505]
  Testing remains to evaluate accuracy of neural network perception systems. We employ neural network verification to prove that a model will always produce estimates within some error bound to the ground truth.
  arXiv  Detail & Related papers  (2020-12-16T23:09:53Z)
• 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)
• Compressive sensing with un-trained neural networks: Gradient descent finds the smoothest approximation [60.80172153614544]
  Un-trained convolutional neural networks have emerged as highly successful tools for image recovery and restoration. We show that an un-trained convolutional neural network can approximately reconstruct signals and images that are sufficiently structured, from a near minimal number of random measurements.
  arXiv  Detail & Related papers  (2020-05-07T15:57:25Z)
• Verifying Recurrent Neural Networks using Invariant Inference [0.0]
  We propose a novel approach for verifying properties of a widespread variant of neural networks, called recurrent neural networks. Our approach is based on the inference of invariants, which allow us to reduce the complex problem of verifying recurrent networks into simpler, non-recurrent problems.
  arXiv  Detail & Related papers  (2020-04-06T08:08:24Z)

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.