Safety Verification of Neural Network Control Systems Using Guaranteed Neural Network Model Reduction

• URL: http://arxiv.org/abs/2301.07531v1
• Date: Tue, 17 Jan 2023 03:25:57 GMT
• Title: Safety Verification of Neural Network Control Systems Using Guaranteed Neural Network Model Reduction
• Authors: Weiming Xiang and Zhongzhu Shao
• Abstract summary: A concept of model reduction precision is proposed to describe the guaranteed distance between the outputs of a neural network and its reduced-size version. A reachability-based algorithm is proposed to accurately compute the model reduction precision. An algorithm to compute the reachable set of the original system is developed, which is able to support much more computationally efficient safety verification processes.
• Score: 3.0839245814393728
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper aims to enhance the computational efficiency of safety verification of neural network control systems by developing a guaranteed neural network model reduction method. First, a concept of model reduction precision is proposed to describe the guaranteed distance between the outputs of a neural network and its reduced-size version. A reachability-based algorithm is proposed to accurately compute the model reduction precision. Then, by substituting a reduced-size neural network controller into the closed-loop system, an algorithm to compute the reachable set of the original system is developed, which is able to support much more computationally efficient safety verification processes. Finally, the developed methods are applied to a case study of the Adaptive Cruise Control system with a neural network controller, which is shown to significantly reduce the computational time of safety verification and thus validate the effectiveness of the method.

Related papers

• Fully Automatic Neural Network Reduction for Formal Verification [8.017543518311196]
  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.
  arXiv  Detail & Related papers  (2023-05-03T07:13:47Z)
• Guaranteed Quantization Error Computation for Neural Network Model Compression [2.610470075814367]
  Neural network model compression techniques can address the computation issue of deep neural networks on embedded devices in industrial systems. A merged neural network is built from a feedforward neural network and its quantized version to produce the exact output difference between two neural networks.
  arXiv  Detail & Related papers  (2023-04-26T20:21:54Z)
• 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)
• Can pruning improve certified robustness of neural networks? [106.03070538582222]
  We show that neural network pruning can improve empirical robustness of deep neural networks (NNs) Our experiments show that by appropriately pruning an NN, its certified accuracy can be boosted up to 8.2% under standard training. We additionally observe the existence of certified lottery tickets that can match both standard and certified robust accuracies of the original dense models.
  arXiv  Detail & Related papers  (2022-06-15T05:48:51Z)
• Large-Scale Sequential Learning for Recommender and Engineering Systems [91.3755431537592]
  In this thesis, we focus on the design of an automatic algorithms that provide personalized ranking by adapting to the current conditions. For the former, we propose novel algorithm called SAROS that take into account both kinds of feedback for learning over the sequence of interactions. The proposed idea of taking into account the neighbour lines shows statistically significant results in comparison with the initial approach for faults detection in power grid.
  arXiv  Detail & Related papers  (2022-05-13T21:09:41Z)
• Scalable computation of prediction intervals for neural networks via matrix sketching [79.44177623781043]
  Existing algorithms for uncertainty estimation require modifying the model architecture and training procedure. This work proposes a new algorithm that can be applied to a given trained neural network and produces approximate prediction intervals.
  arXiv  Detail & Related papers  (2022-05-06T13:18:31Z)
• Robust lEarned Shrinkage-Thresholding (REST): Robust unrolling for sparse recover [87.28082715343896]
  We consider deep neural networks for solving inverse problems that are robust to forward model mis-specifications. We design a new robust deep neural network architecture by applying algorithm unfolding techniques to a robust version of the underlying recovery problem. The proposed REST network is shown to outperform state-of-the-art model-based and data-driven algorithms in both compressive sensing and radar imaging problems.
  arXiv  Detail & Related papers  (2021-10-20T06:15:45Z)
• Fast Falsification of Neural Networks using Property Directed Testing [0.1529342790344802]
  We propose a falsification algorithm for neural networks that directs the search for a counterexample. Our algorithm uses a derivative-free sampling-based optimization method. We show that our falsification procedure detects all the unsafe instances that other verification tools also report as unsafe.
  arXiv  Detail & Related papers  (2021-04-26T09:16:27Z)
• Generating Probabilistic Safety Guarantees for Neural Network Controllers [30.34898838361206]
  We use a dynamics model to determine the output properties that must hold for a neural network controller to operate safely. We develop an adaptive verification approach to efficiently generate an overapproximation of the neural network policy. We show that our method is able to generate meaningful probabilistic safety guarantees for aircraft collision avoidance neural networks.
  arXiv  Detail & Related papers  (2021-03-01T18:48:21Z)
• 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)
• Bayesian Optimization with Machine Learning Algorithms Towards Anomaly Detection [66.05992706105224]
  In this paper, an effective anomaly detection framework is proposed utilizing Bayesian Optimization technique. The performance of the considered algorithms is evaluated using the ISCX 2012 dataset. Experimental results show the effectiveness of the proposed framework in term of accuracy rate, precision, low-false alarm rate, and recall.
  arXiv  Detail & Related papers  (2020-08-05T19:29:35Z)

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.