Neural Network Verification in Control

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.Software– https://github.com/mit-acl/nn_robustness_analysis

I. Introduction

Data-driven (or learning-based) methods offer many compelling advantages for addressing long-standing issues in the field of controls. For instance, real environments are often highly dynamic, nonlinear, uncertain, and high-dimensional, each of which present major challenges for the design, verification and deployment of control systems. [1] identifies opportunities to reduce the costs of modeling complicated systems and improve the control of large-scale networked systems through learning: “In order to maintain verifiable high performance, future engineering systems will need to be equipped with on-line capabilities for active model learning and adaptation, and for model accuracy assessment.”