Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers

• URL: http://arxiv.org/abs/2301.07912v2
• Date: Mon, 7 Aug 2023 06:20:31 GMT
• Title: Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers
• Authors: Saber Jafarpour, Akash Harapanahalli, Samuel Coogan
• Abstract summary: This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system.
• Score: 5.543220407902113
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Given a neural network, we use an existing verification algorithm to construct inclusion functions for its input-output behavior. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. This embedding provides a scalable approach for safety analysis of the neural control loop while preserving the nonlinear structure of the system. We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system. We design an algorithm to leverage this computational advantage through partitioning strategies, improving our reachable set estimates while balancing its runtime with tunable parameters. We demonstrate the performance of this algorithm through two case studies. First, we demonstrate this method's strength in complex nonlinear environments. Then, we show that our approach matches the performance of the state-of-the art verification algorithm for linear discretized systems.

Related papers

• Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops [4.768272342753616]
  We propose a computationally efficient framework for interval reachability of systems with neural network controllers. We use inclusion functions for the open-loop system and the neural network controller to embed the closed-loop system into a larger-dimensional embedding system.
  arXiv  Detail & Related papers  (2023-07-27T15:30:22Z)
• A Recursively Recurrent Neural Network (R2N2) Architecture for Learning Iterative Algorithms [64.3064050603721]
  We generalize Runge-Kutta neural network to a recurrent neural network (R2N2) superstructure for the design of customized iterative algorithms. We demonstrate that regular training of the weight parameters inside the proposed superstructure on input/output data of various computational problem classes yields similar iterations to Krylov solvers for linear equation systems, Newton-Krylov solvers for nonlinear equation systems, and Runge-Kutta solvers for ordinary differential equations.
  arXiv  Detail & Related papers  (2022-11-22T16:30:33Z)
• Stabilizing Q-learning with Linear Architectures for Provably Efficient Learning [53.17258888552998]
  This work proposes an exploration variant of the basic $Q$-learning protocol with linear function approximation. We show that the performance of the algorithm degrades very gracefully under a novel and more permissive notion of approximation error.
  arXiv  Detail & Related papers  (2022-06-01T23:26:51Z)
• Supervised DKRC with Images for Offline System Identification [77.34726150561087]
  Modern dynamical systems are becoming increasingly non-linear and complex. There is a need for a framework to model these systems in a compact and comprehensive representation for prediction and control. Our approach learns these basis functions using a supervised learning approach.
  arXiv  Detail & Related papers  (2021-09-06T04:39:06Z)
• Reachability Analysis of Neural Feedback Loops [34.94930611635459]
  This work focuses on estimating the forward reachable set of textitneural feedback loops (closed-loop systems with NN controllers) Recent work provides bounds on these reachable sets, but the computationally tractable approaches yield overly conservative bounds. This work bridges the gap by formulating a convex optimization problem for the reachability analysis of closed-loop systems with NN controllers.
  arXiv  Detail & Related papers  (2021-08-09T16:11:57Z)
• Efficient Reachability Analysis of Closed-Loop Systems with Neural Network Controllers [39.27951763459939]
  This work focuses on estimating the forward reachable set of closed-loop systems with NN controllers. Recent work provides bounds on these reachable sets, yet the computationally efficient approaches provide overly conservative bounds. This work bridges the gap by formulating a convex optimization problem for reachability analysis for closed-loop systems with NN controllers.
  arXiv  Detail & Related papers  (2021-01-05T22:30:39Z)
• Connecting Weighted Automata, Tensor Networks and Recurrent Neural Networks through Spectral Learning [58.14930566993063]
  We present connections between three models used in different research fields: weighted finite automata(WFA) from formal languages and linguistics, recurrent neural networks used in machine learning, and tensor networks. We introduce the first provable learning algorithm for linear 2-RNN defined over sequences of continuous vectors input.
  arXiv  Detail & Related papers  (2020-10-19T15:28:00Z)
• Provably Efficient Neural Estimation of Structural Equation Model: An Adversarial Approach [144.21892195917758]
  We study estimation in a class of generalized Structural equation models (SEMs) We formulate the linear operator equation as a min-max game, where both players are parameterized by neural networks (NNs), and learn the parameters of these neural networks using a gradient descent. For the first time we provide a tractable estimation procedure for SEMs based on NNs with provable convergence and without the need for sample splitting.
  arXiv  Detail & Related papers  (2020-07-02T17:55:47Z)
• Parallelization Techniques for Verifying Neural Networks [52.917845265248744]
  We introduce an algorithm based on the verification problem in an iterative manner and explore two partitioning strategies. We also introduce a highly parallelizable pre-processing algorithm that uses the neuron activation phases to simplify the neural network verification problems.
  arXiv  Detail & Related papers  (2020-04-17T20:21:47Z)
• Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming [19.51345816555571]
  We propose a novel forward reachability analysis method for the safety verification of linear time-varying systems with neural networks in feedback. We show that we can compute these approximate reachable sets using semidefinite programming. We illustrate our method in a quadrotor example, in which we first approximate a nonlinear model predictive controller via a deep neural network and then apply our analysis tool to certify finite-time reachability and constraint satisfaction of the closed-loop system.
  arXiv  Detail & Related papers  (2020-04-16T18:48:25Z)
• Active Learning for Identification of Linear Dynamical Systems [12.056495277232118]
  We show a finite time bound estimation rate our algorithm attains. We analyze several examples where our algorithm provably improves over rates obtained by playing noise.
  arXiv  Detail & Related papers  (2020-02-02T21:30:38Z)

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.