Neural Network Verification in Control

TL;DR

This paper reviews recent methods for verifying the safety and robustness of neural networks in control systems, focusing on formal guarantees for neural feedback loops and applications in reachability analysis and reinforcement learning.

Contribution

It unifies recent verification techniques from machine learning and control, extending them to provide formal safety guarantees for neural feedback systems.

Findings

Enables formal verification of neural feedback loops.

Supports closed-loop reachability analysis.

Facilitates robust deep reinforcement learning.

Abstract

Learning-based methods could provide solutions to many of the long-standing challenges in control. However, the neural networks (NNs) commonly used in modern learning approaches present substantial challenges for analyzing the resulting control systems' safety properties. Fortunately, a new body of literature could provide tractable methods for analysis and verification of these high dimensional, highly nonlinear representations. This tutorial first introduces and unifies recent techniques (many of which originated in the computer vision and machine learning communities) for verifying robustness properties of NNs. The techniques are then extended to provide formal guarantees of neural feedback loops (e.g., closed-loop system with NN control policy). The provided tools are shown to enable closed-loop reachability analysis and robust deep reinforcement learning.