Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes

• URL: http://arxiv.org/abs/2212.07553v3
• Date: Mon, 15 May 2023 20:08:27 GMT
• Title: Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes
• Authors: Taha Entesari, Mahyar Fazlyab
• Abstract summary: We develop a new approach for over-approximating the reachable sets of neural network dynamical systems using adaptive template polytopes. We illustrate the utility of the proposed approach in the reachability analysis of linear systems driven by neural network controllers.
• Score: 2.66512000865131
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Over-approximating the reachable sets of dynamical systems is a fundamental problem in safety verification and robust control synthesis. The representation of these sets is a key factor that affects the computational complexity and the approximation error. In this paper, we develop a new approach for over-approximating the reachable sets of neural network dynamical systems using adaptive template polytopes. We use the singular value decomposition of linear layers along with the shape of the activation functions to adapt the geometry of the polytopes at each time step to the geometry of the true reachable sets. We then propose a branch-and-bound method to compute accurate over-approximations of the reachable sets by the inferred templates. We illustrate the utility of the proposed approach in the reachability analysis of linear systems driven by neural network controllers.

Related papers

• Neural Control Variates with Automatic Integration [49.91408797261987]
  This paper proposes a novel approach to construct learnable parametric control variates functions from arbitrary neural network architectures. We use the network to approximate the anti-derivative of the integrand. We apply our method to solve partial differential equations using the Walk-on-sphere algorithm.
  arXiv  Detail & Related papers  (2024-09-23T06:04:28Z)
• A Data-Driven Hybrid Automaton Framework to Modeling Complex Dynamical Systems [2.610470075814367]
  A data-driven hybrid automaton model is proposed to capture unknown complex dynamical system behaviors. Small-scale neural networks are trained as the local dynamical description for their corresponding topologies. A numerical example of the limit cycle is presented to illustrate that the developed models can significantly reduce the computational cost in reachable set computation.
  arXiv  Detail & Related papers  (2023-04-26T20:18:12Z)
• Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers [5.543220407902113]
  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.
  arXiv  Detail & Related papers  (2023-01-19T06:46:36Z)
• Model-Based Reinforcement Learning via Stochastic Hybrid Models [39.83837705993256]
  This paper adopts a hybrid-system view of nonlinear modeling and control. We consider a sequence modeling paradigm that captures the temporal structure of the data. We show that these time-series models naturally admit a closed-loop extension that we use to extract local feedback controllers.
  arXiv  Detail & Related papers  (2021-11-11T14:05:46Z)
• Deep Learning Approximation of Diffeomorphisms via Linear-Control Systems [91.3755431537592]
  We consider a control system of the form $dot x = sum_i=1lF_i(x)u_i$, with linear dependence in the controls. We use the corresponding flow to approximate the action of a diffeomorphism on a compact ensemble of points.
  arXiv  Detail & Related papers  (2021-10-24T08:57:46Z)
• 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)
• An Ode to an ODE [78.97367880223254]
  We present a new paradigm for Neural ODE algorithms, called ODEtoODE, where time-dependent parameters of the main flow evolve according to a matrix flow on the group O(d) This nested system of two flows provides stability and effectiveness of training and provably solves the gradient vanishing-explosion problem.
  arXiv  Detail & Related papers  (2020-06-19T22:05:19Z)
• Measuring Model Complexity of Neural Networks with Curve Activation Functions [100.98319505253797]
  We propose the linear approximation neural network (LANN) to approximate a given deep model with curve activation function. We experimentally explore the training process of neural networks and detect overfitting. We find that the $L1$ and $L2$ regularizations suppress the increase of model complexity.
  arXiv  Detail & Related papers  (2020-06-16T07:38:06Z)
• 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)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  We propose an automatic and formally sound method for synthesising Lyapunov functions. We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.
  arXiv  Detail & Related papers  (2020-03-19T17:21:02Z)
• Reachability Analysis for Feed-Forward Neural Networks using Face Lattices [10.838397735788245]
  We propose a parallelizable technique to compute exact reachable sets of a neural network to an input set. Our approach is capable of constructing the complete input set given an output set, so that any input that leads to safety violation can be tracked.
  arXiv  Detail & Related papers  (2020-03-02T22:23:57Z)

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.