Reachability Analysis of Neural Feedback Loops
- URL: http://arxiv.org/abs/2108.04140v1
- Date: Mon, 9 Aug 2021 16:11:57 GMT
- Title: Reachability Analysis of Neural Feedback Loops
- Authors: Michael Everett, Golnaz Habibi, Chuangchuang Sun, Jonathan P. How
- Abstract summary: 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.
- Score: 34.94930611635459
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Neural Networks (NNs) can provide major empirical performance improvements
for closed-loop systems, but they also introduce challenges in formally
analyzing those systems' safety properties. In particular, this work focuses on
estimating the forward reachable set of \textit{neural 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 (thus cannot be used to verify useful properties), and the
methods that yield tighter bounds are too intensive for online computation.
This work bridges the gap by formulating a convex optimization problem for the
reachability analysis of closed-loop systems with NN controllers. While the
solutions are less tight than previous (semidefinite program-based) methods,
they are substantially faster to compute, and some of those computational time
savings can be used to refine the bounds through new input set partitioning
techniques, which is shown to dramatically reduce the tightness gap. The new
framework is developed for systems with uncertainty (e.g., measurement and
process noise) and nonlinearities (e.g., polynomial dynamics), and thus is
shown to be applicable to real-world systems. To inform the design of an
initial state set when only the target state set is known/specified, a novel
algorithm for backward reachability analysis is also provided, which computes
the set of states that are guaranteed to lead to the target set. The numerical
experiments show that our approach (based on linear relaxations and
partitioning) gives a $5\times$ reduction in conservatism in $150\times$ less
computation time compared to the state-of-the-art. Furthermore, experiments on
quadrotor, 270-state, and polynomial systems demonstrate the method's ability
to handle uncertainty sources, high dimensionality, and nonlinear dynamics,
respectively.
Related papers
- Large-Scale OD Matrix Estimation with A Deep Learning Method [70.78575952309023]
The proposed method integrates deep learning and numerical optimization algorithms to infer matrix structure and guide numerical optimization.
We conducted tests to demonstrate the good generalization performance of our method on a large-scale synthetic dataset.
arXiv Detail & Related papers (2023-10-09T14:30:06Z) - Accelerated First-Order Optimization under Nonlinear Constraints [73.2273449996098]
We exploit between first-order algorithms for constrained optimization and non-smooth systems to design a new class of accelerated first-order algorithms.
An important property of these algorithms is that constraints are expressed in terms of velocities instead of sparse variables.
arXiv Detail & Related papers (2023-02-01T08:50:48Z) - 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) - 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) - Backward Reachability Analysis for Neural Feedback Loops [40.989393438716476]
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 an algorithm to iteratively find BP set estimates over a given time horizon and demonstrate the ability to reduce conservativeness by up to 88% with low additional computational cost.
arXiv Detail & Related papers (2022-04-14T01:13:14Z) - Online Limited Memory Neural-Linear Bandits with Likelihood Matching [53.18698496031658]
We study neural-linear bandits for solving problems where both exploration and representation learning play an important role.
We propose a likelihood matching algorithm that is resilient to catastrophic forgetting and is completely online.
arXiv Detail & Related papers (2021-02-07T14:19:07Z) - 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) - Robustness Analysis of Neural Networks via Efficient Partitioning with
Applications in Control Systems [45.35808135708894]
Neural networks (NNs) are now routinely implemented on systems that must operate in uncertain environments.
This paper unifies propagation and partition approaches to provide a family of robustness analysis algorithms.
New partitioning techniques are aware of their current bound estimates and desired boundary shape.
arXiv Detail & Related papers (2020-10-01T16:51:36Z) - 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) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
A fundamental component of neural network verification is the computation of bounds on the values their outputs can take.
We propose a novel approach based on Lagrangian Decomposition.
We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
arXiv Detail & Related papers (2020-02-24T17:55:10Z)
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.