Risk Verification of Stochastic Systems with Neural Network Controllers

TL;DR

This paper introduces a data-driven framework for verifying the risk of stochastic systems with neural network controllers, focusing on safety specifications and risk bounds for nominal and perturbed systems.

Contribution

It presents a novel method to estimate and bound the risk of NN-controlled stochastic systems using trajectory robustness and system closeness measures.

Findings

Risk bounds for perturbed systems are derived from nominal system estimates.

The framework is demonstrated on an underwater vehicle and an autonomous car.

Quantitative risk assessment is feasible for complex stochastic systems with NN controllers.

Abstract

Motivated by the fragility of neural network (NN) controllers in safety-critical applications, we present a data-driven framework for verifying the risk of stochastic dynamical systems with NN controllers. Given a stochastic control system, an NN controller, and a specification equipped with a notion of trace robustness (e.g., constraint functions or signal temporal logic), we collect trajectories from the system that may or may not satisfy the specification. In particular, each of the trajectories produces a robustness value that indicates how well (severely) the specification is satisfied (violated). We then compute risk metrics over these robustness values to estimate the risk that the NN controller will not satisfy the specification. We are further interested in quantifying the difference in risk between two systems, and we show how the risk estimated from a nominal system can provide an upper bound the risk of a perturbed version of the system. In particular, the tightness of this bound depends on the closeness of the systems in terms of the closeness of their system trajectories. For Lipschitz continuous and incrementally input-to-state stable systems, we show how to exactly quantify system closeness with varying degrees of conservatism, while we estimate system closeness for more general systems from data in our experiments. We demonstrate our risk verification approach on two case studies, an underwater vehicle and an F1/10 autonomous car.