POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems

• URL: http://arxiv.org/abs/2304.01218v3
• Date: Thu, 6 Apr 2023 02:12:41 GMT
• Title: POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems
• Authors: Yixuan Wang, Weichao Zhou, Jiameng Fan, Zhilu Wang, Jiajun Li, Xin Chen, Chao Huang, Wenchao Li, Qi Zhu
• Abstract summary: We present POLAR-Express, an efficient and precise formal reachability analysis tool for verifying the safety of neural-network controlled systems (NNCSs) POLAR-Express uses Taylor model arithmetic to propagate Taylor models across a neural network layer-by-layer to compute an overapproximation of the neural-network function. We also present a novel approach to propagate TMs more efficiently and precisely across ReLU activation functions.
• Score: 18.369115196505657
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neural networks (NNs) playing the role of controllers have demonstrated impressive empirical performances on challenging control problems. However, the potential adoption of NN controllers in real-life applications also gives rise to a growing concern over the safety of these neural-network controlled systems (NNCSs), especially when used in safety-critical applications. In this work, we present POLAR-Express, an efficient and precise formal reachability analysis tool for verifying the safety of NNCSs. POLAR-Express uses Taylor model arithmetic to propagate Taylor models (TMs) across a neural network layer-by-layer to compute an overapproximation of the neural-network function. It can be applied to analyze any feed-forward neural network with continuous activation functions. We also present a novel approach to propagate TMs more efficiently and precisely across ReLU activation functions. In addition, POLAR-Express provides parallel computation support for the layer-by-layer propagation of TMs, thus significantly improving the efficiency and scalability over its earlier prototype POLAR. Across the comparison with six other state-of-the-art tools on a diverse set of benchmarks, POLAR-Express achieves the best verification efficiency and tightness in the reachable set analysis.

Related papers

• Building Hybrid B-Spline And Neural Network Operators [0.0]
  Control systems are indispensable for ensuring the safety of cyber-physical systems (CPS) We propose a novel strategy that combines the inductive bias of B-splines with data-driven neural networks to facilitate real-time predictions of CPS behavior.
  arXiv  Detail & Related papers  (2024-06-06T21:54:59Z)
• Improving Graph Machine Learning Performance Through Feature Augmentation Based on Network Control Theory [3.2505793054002963]
  Graph Neural Networks (GNNs) have demonstrated exceptional utility in various network-based learning tasks. Many real-world systems may lack node-level information, posing a challenge for GNNs. We introduce a novel approach, NCT-based Enhanced Feature Augmentation (NCT-EFA), that assimilates average controllability, along with other centrality indices, into the feature augmentation pipeline to enhance GNNs performance.
  arXiv  Detail & Related papers  (2024-05-03T19:11:54Z)
• Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
  Learning-based neural network (NN) control policies have shown impressive empirical performance in a wide range of tasks in robotics and control. Lyapunov stability guarantees over the region-of-attraction (ROA) for NN controllers with nonlinear dynamical systems are challenging to obtain. We demonstrate a new framework for learning NN controllers together with Lyapunov certificates using fast empirical falsification and strategic regularizations.
  arXiv  Detail & Related papers  (2024-04-11T17:49:15Z)
• ConCerNet: A Contrastive Learning Based Framework for Automated Conservation Law Discovery and Trustworthy Dynamical System Prediction [82.81767856234956]
  This paper proposes a new learning framework named ConCerNet to improve the trustworthiness of the DNN based dynamics modeling. We show that our method consistently outperforms the baseline neural networks in both coordinate error and conservation metrics.
  arXiv  Detail & Related papers  (2023-02-11T21:07:30Z)
• Closed-form control with spike coding networks [1.1470070927586016]
  Efficient and robust control using spiking neural networks (SNNs) is still an open problem. We extend neuroscience theory of Spike Coding Networks (SCNs) by incorporating closed-form optimal estimation and control. We demonstrate robust spiking control of simulated spring-mass-damper and cart-pole systems.
  arXiv  Detail & Related papers  (2022-12-25T10:32:20Z)
• Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems [59.57462129637796]
  This paper presents a backward reachability approach for safety verification of closed-loop systems with neural networks (NNs) The presence of NNs in the feedback loop presents a unique set of problems due to the nonlinearities in their activation functions and because NN models are generally not invertible. We present frameworks for calculating BP over-approximations for both linear and nonlinear systems with control policies represented by feedforward NNs.
  arXiv  Detail & Related papers  (2022-09-28T13:17:28Z)
• 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)
• FitAct: Error Resilient Deep Neural Networks via Fine-Grained Post-Trainable Activation Functions [0.05249805590164901]
  Deep neural networks (DNNs) are increasingly being deployed in safety-critical systems such as personal healthcare devices and self-driving cars. In this paper, we propose FitAct, a low-cost approach to enhance the error resilience of DNNs by deploying fine-grained post-trainable activation functions.
  arXiv  Detail & Related papers  (2021-12-27T07:07:50Z)
• Deep Kronecker neural networks: A general framework for neural networks with adaptive activation functions [4.932130498861987]
  We propose a new type of neural networks, Kronecker neural networks (KNNs), that form a general framework for neural networks with adaptive activation functions. Under suitable conditions, KNNs induce a faster decay of the loss than that by the feed-forward networks.
  arXiv  Detail & Related papers  (2021-05-20T04:54:57Z)
• Modeling from Features: a Mean-field Framework for Over-parameterized Deep Neural Networks [54.27962244835622]
  This paper proposes a new mean-field framework for over- parameterized deep neural networks (DNNs) In this framework, a DNN is represented by probability measures and functions over its features in the continuous limit. We illustrate the framework via the standard DNN and the Residual Network (Res-Net) architectures.
  arXiv  Detail & Related papers  (2020-07-03T01:37:16Z)
• Rectified Linear Postsynaptic Potential Function for Backpropagation in Deep Spiking Neural Networks [55.0627904986664]
  Spiking Neural Networks (SNNs) usetemporal spike patterns to represent and transmit information, which is not only biologically realistic but also suitable for ultra-low-power event-driven neuromorphic implementation. This paper investigates the contribution of spike timing dynamics to information encoding, synaptic plasticity and decision making, providing a new perspective to design of future DeepSNNs and neuromorphic hardware systems.
  arXiv  Detail & Related papers  (2020-03-26T11:13:07Z)

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.