Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions

Rayan Mazouz, Karan Muvvala, Akash Ratheesh, Luca Laurenti, Morteza Lahijanian

TL;DR

The paper addresses safety guarantees for neural network dynamic models by introducing stochastic barrier functions that provide a lower bound on the probability that trajectories remain in a safe set over a horizon, without unfolding the NN. By leveraging local convex relaxations of the NN to obtain piecewise-linear bounds and formulating barrier synthesis as an SOS program, it yields a computable certificate $B(x)$ that ensures forward invariance with probability at least $1 - (\eta + \beta N)$. When certification fails, the authors synthesize a minimally-invasive affine controller via a linear program to maximize safety probability while limiting intervention. Empirical results across multiple NNDMs with up to hundreds of neurons per layer demonstrate scalability and that the proposed controller can significantly improve safety probability, highlighting practical impact for safety-critical RL and model-based control.

Abstract

Neural Networks (NNs) have been successfully employed to represent the state evolution of complex dynamical systems. Such models, referred to as NN dynamic models (NNDMs), use iterative noisy predictions of NN to estimate a distribution of system trajectories over time. Despite their accuracy, safety analysis of NNDMs is known to be a challenging problem and remains largely unexplored. To address this issue, in this paper, we introduce a method of providing safety guarantees for NNDMs. Our approach is based on stochastic barrier functions, whose relation with safety are analogous to that of Lyapunov functions with stability. We first show a method of synthesizing stochastic barrier functions for NNDMs via a convex optimization problem, which in turn provides a lower bound on the system's safety probability. A key step in our method is the employment of the recent convex approximation results for NNs to find piece-wise linear bounds, which allow the formulation of the barrier function synthesis problem as a sum-of-squares optimization program. If the obtained safety probability is above the desired threshold, the system is certified. Otherwise, we introduce a method of generating controls for the system that robustly maximizes the safety probability in a minimally-invasive manner. We exploit the convexity property of the barrier function to formulate the optimal control synthesis problem as a linear program. Experimental results illustrate the efficacy of the method. Namely, they show that the method can scale to multi-dimensional NNDMs with multiple layers and hundreds of neurons per layer, and that the controller can significantly improve the safety probability.

Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions

TL;DR

The paper addresses safety guarantees for neural network dynamic models by introducing stochastic barrier functions that provide a lower bound on the probability that trajectories remain in a safe set over a horizon, without unfolding the NN. By leveraging local convex relaxations of the NN to obtain piecewise-linear bounds and formulating barrier synthesis as an SOS program, it yields a computable certificate that ensures forward invariance with probability at least . When certification fails, the authors synthesize a minimally-invasive affine controller via a linear program to maximize safety probability while limiting intervention. Empirical results across multiple NNDMs with up to hundreds of neurons per layer demonstrate scalability and that the proposed controller can significantly improve safety probability, highlighting practical impact for safety-critical RL and model-based control.

Abstract

Neural Networks (NNs) have been successfully employed to represent the state evolution of complex dynamical systems. Such models, referred to as NN dynamic models (NNDMs), use iterative noisy predictions of NN to estimate a distribution of system trajectories over time. Despite their accuracy, safety analysis of NNDMs is known to be a challenging problem and remains largely unexplored. To address this issue, in this paper, we introduce a method of providing safety guarantees for NNDMs. Our approach is based on stochastic barrier functions, whose relation with safety are analogous to that of Lyapunov functions with stability. We first show a method of synthesizing stochastic barrier functions for NNDMs via a convex optimization problem, which in turn provides a lower bound on the system's safety probability. A key step in our method is the employment of the recent convex approximation results for NNs to find piece-wise linear bounds, which allow the formulation of the barrier function synthesis problem as a sum-of-squares optimization program. If the obtained safety probability is above the desired threshold, the system is certified. Otherwise, we introduce a method of generating controls for the system that robustly maximizes the safety probability in a minimally-invasive manner. We exploit the convexity property of the barrier function to formulate the optimal control synthesis problem as a linear program. Experimental results illustrate the efficacy of the method. Namely, they show that the method can scale to multi-dimensional NNDMs with multiple layers and hundreds of neurons per layer, and that the controller can significantly improve the safety probability.
Paper Structure (21 sections, 6 theorems, 14 equations, 4 figures, 4 tables, 1 algorithm)

This paper contains 21 sections, 6 theorems, 14 equations, 4 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Problem Formulation
  4. Overall Approach
  5. Preliminaries
  6. Stochastic Barrier Functions
  7. Non-negative Polynomials
  8. Barrier Functions for Neural Network Dynamical Models
  9. Local Convex Relaxation of NNDMs
  10. Barrier Function (Certificate) Synthesis
  11. Minimally-invasive Barrier Controller Synthesis
  12. Control Synthesis Algorithm
  13. Case Studies
  14. Conclusion
  15. Additional Discussions on the Experiments
  16. ...and 6 more sections

Key Result

Proposition 1

Let $X \subset \mathbb{R}^n$ be a compact basic semi-algebraic set defined as $X = \{x \in \mathbb{R}^n \mid h_i(x) \geq 0 \;\; \forall i \in \{1, \ldots, l\}\},$ where $h_i(x)$ is a polynomial. Then, polynomial $\gamma(x)$ is non-negative on $X$ if, for some $\lambda_{0}(x), \lambda_{i}(x) \in \La

Figures (4)

  • Figure 1: Comparison of $\beta_q$ values for the Pendulum NNDM with 2 layers and 64 neurons per layer before and after applying the controller for various $|Q|$. Shade of gray correspond to the values of $\beta_q$.
  • Figure 2: Vector fields of the NNDMs for the Pendulum agent with various architectures.
  • Figure 3: State evolution of the Pendulum 3 layer NNDM model for 100 steps with and without safety feedback controller $\pi$. Blue line shows state evolution for the system starting at $\theta = 0$ and $\dot{\theta} = 0$. Black dotted line demarcates the safe space ($X_\mathrm{s}$) in $\theta$ dimension and the state space ($X$) in $\dot{\theta}$ dimension.
  • Figure 4: State evolution of the cartpole NNDM with 2 layers for 100 steps with and without safety feedback controller $\pi$ in (a) and (b), respectively. Blue line shows state evolution for the system starting at $x=0$, $\dot{x} = 0$, $\theta = 0$, and $\dot{\theta} = 0$. Black dotted line demarcates the state space ($X$) in $\dot{x}$, $\dot{\theta}$, and safe space ($X_\mathrm{s}$) in $x$ and $\theta$ dimension respectively.

Theorems & Definitions (17)

  • Remark 1
  • Remark 2
  • Remark 3
  • Definition 1: SOS Polynomial
  • Proposition 1: nie2007complexity
  • Corollary 1
  • Remark 4
  • Lemma 1
  • proof
  • Theorem 1: NNDM Barrier Certificate
  • ...and 7 more