Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Model-Free Verification for Neural Network Controlled Systems

Han Wang, Zuxun Xiong, Liqun Zhao, Antonis Papachristodoulou

TL;DR

This paper proposes data-driven semi-definite programs to formally verify stability and safety for a neural network controlled linear system with unknown dynamics and performs verification directly from end-to-end without identifying the dynamics.

Abstract

Neural network controllers have shown potential in achieving superior performance in feedback control systems. Although a neural network can be trained efficiently using deep and reinforcement learning methods, providing formal guarantees for the closed-loop properties is challenging. The main difficulty comes from the nonlinear activation functions. One popular method is to use sector bounds on the activation functions resulting in a robust analysis. These methods work well under the assumption that the system dynamics are perfectly known, which is, however, impossible in practice. In this paper, we propose data-driven semi-definite programs to formally verify stability and safety for a neural network controlled linear system with unknown dynamics. The proposed method performs verification directly from end-to-end without identifying the dynamics. Through a numerical example, we validate the efficacy of our method on linear systems with controller trained by imitation learning.

Model-Free Verification for Neural Network Controlled Systems

TL;DR

This paper proposes data-driven semi-definite programs to formally verify stability and safety for a neural network controlled linear system with unknown dynamics and performs verification directly from end-to-end without identifying the dynamics.

Abstract

Neural network controllers have shown potential in achieving superior performance in feedback control systems. Although a neural network can be trained efficiently using deep and reinforcement learning methods, providing formal guarantees for the closed-loop properties is challenging. The main difficulty comes from the nonlinear activation functions. One popular method is to use sector bounds on the activation functions resulting in a robust analysis. These methods work well under the assumption that the system dynamics are perfectly known, which is, however, impossible in practice. In this paper, we propose data-driven semi-definite programs to formally verify stability and safety for a neural network controlled linear system with unknown dynamics. The proposed method performs verification directly from end-to-end without identifying the dynamics. Through a numerical example, we validate the efficacy of our method on linear systems with controller trained by imitation learning.
Paper Structure (15 sections, 4 theorems, 50 equations, 1 figure)

This paper contains 15 sections, 4 theorems, 50 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Problem Formulation
  3. Data-Driven Open Loop Representation
  4. Neural Network Representation
  5. Sector Constraints
  6. Neural Network Verification
  7. Stability Verification
  8. Safety Verification
  9. Invariance Verification
  10. Simulation Results
  11. Vehicle Cruise Control
  12. Stability Verification
  13. Safety Verification
  14. Pendulum
  15. Conclusion

Key Result

lemma 1

Let $\alpha_\phi$, $\beta_{\phi}\in\mathbb{R}^{n_\phi}$ be given with $\alpha_{\phi}\le \beta_{\phi}$, and $w_*:=\phi(v_*)$. Assume $\phi$ element-wisely satisfies the offset sector $[\alpha_{\phi},\beta_{\phi}]$ around the point $(v_*,w_*)$ for all $v_\phi\in\mathbb{R}^{n_\phi}$. Then, for any $\la where $A_\phi$ = diag($\alpha_\phi$), $B_\phi$ = diag($\beta_\phi$), and $\Lambda$ = diag($\lambda$

Figures (1)

  • Figure 1: The ROAs of NN controller.

Theorems & Definitions (9)

  • definition 1
  • definition 2
  • lemma 1: yin2021stability
  • theorem 1
  • proof
  • theorem 2
  • proof
  • theorem 3
  • proof