There has been an increasing interest in using neural networks in closed-loop control systems to improve performance and reduce computational costs for on-line implementation. However, providing safety and stability guarantees for these systems is challenging due to the nonlinear and compositional structure of neural networks. In this paper, we propose a novel forward reachability analysis method for the safety verification of linear time-varying systems with neural networks in feedback interconnection. Our technical approach relies on abstracting the nonlinear activation functions by quadratic constraints, which leads to an outer-approximation of forward reachable sets of the closed-loop system. 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.
more »
« less
Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers
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.
more »
« less
- Award ID(s):
- 2219755
- NSF-PAR ID:
- 10499306
- Editor(s):
- N. Matni, M. Morari
- Publisher / Repository:
- Proceedings of Machine Learning Research
- Date Published:
- Journal Name:
- 5th Annual Learning for Dynamics & Control Conference
- Format(s):
- Medium: X
- Location:
- Univ. of Pennsylvania
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We present a framework based on interval analysis and monotone systems theory to certify and search for forward invariant sets in nonlinear systems with neural network controllers. The framework (i) constructs localized first-order inclusion functions for the closed-loop system using Jacobian bounds and existing neural network verification tools; (ii) builds a dynamical embedding system where its evaluation along a single trajectory directly corre- sponds with a nested family of hyper-rectangles provably converging to an attractive set of the original system; (iii) utilizes linear transformations to build families of nested paralleletopes with the same properties. The framework is automated in Python using our interval analysis tool- box npinterval, in conjunction with the symbolic arith- metic toolbox sympy, demonstrated on an 8-dimensional leader-follower system.more » « less
-
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.more » « less
-
null (Ed.)We present a data-driven method for computing approximate forward reachable sets using separating kernels in a reproducing kernel Hilbert space. We frame the problem as a support estimation problem, and learn a classifier of the support as an element in a reproducing kernel Hilbert space using a data-driven approach. Kernel methods provide a computationally efficient representation for the classifier that is the solution to a regularized least squares problem. The solution converges almost surely as the sample size increases, and admits known finite sample bounds. This approach is applicable to stochastic systems with arbitrary disturbances and neural network verification problems by treating the network as a dynamical system, or by considering neural network controllers as part of a closed-loop system. We present our technique on several examples, including a spacecraft rendezvous and docking problem, and two nonlinear system benchmarks with neural network controllers.more » « less
-
In this paper, we present a toolbox for interval analysis in numpy, with an application to formal verification of neural network controlled systems. Using the notion of natural inclusion functions, we systematically construct interval bounds for a general class of mappings. The toolbox offers ef- ficient computation of natural inclusion functions using compiled C code, as well as a familiar inter- face in numpy with its canonical features, such as n-dimensional arrays, matrix/vector operations, and vectorization. We then use this toolbox in for- mal verification of dynamical systems with neural network controllers, through the composition of their inclusion functions.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Proceeding:
- The DOI is not currently available.
