Safety Verification of Neural Network Control Systems Using Guaranteed Neural Network Model Reduction

TL;DR

This paper introduces a neural network model reduction technique that guarantees output bounds, enabling more efficient safety verification of neural network control systems through reachability analysis.

Contribution

It proposes a novel guaranteed model reduction method with a reachability-based algorithm, improving the computational efficiency of safety verification for neural network control systems.

Findings

Significantly reduces safety verification computational time.

Provides a guaranteed output distance between original and reduced neural networks.

Successfully applied to an adaptive cruise control system case study.

Abstract

This paper aims to enhance the computational efficiency of safety verification of neural network control systems by developing a guaranteed neural network model reduction method. First, a concept of model reduction precision is proposed to describe the guaranteed distance between the outputs of a neural network and its reduced-size version. A reachability-based algorithm is proposed to accurately compute the model reduction precision. Then, by substituting a reduced-size neural network controller into the closed-loop system, an algorithm to compute the reachable set of the original system is developed, which is able to support much more computationally efficient safety verification processes. Finally, the developed methods are applied to a case study of the Adaptive Cruise Control system with a neural network controller, which is shown to significantly reduce the computational time of safety verification and thus validate the effectiveness of the method.