Formal Control Synthesis for Stochastic Neural Network Dynamic Models

TL;DR

This paper presents a control synthesis framework for stochastic neural network dynamic models that guarantees performance by abstracting NNs into interval Markov decision processes and optimizing strategies accordingly.

Contribution

It introduces a novel method combining convex relaxation and finite abstraction to synthesize controllers with guarantees for complex neural network models.

Findings

Successfully applied to models with up to 5 hidden layers and hundreds of neurons.

Provides formal guarantees of correctness for stochastic neural network models.

Efficient convex optimization approach enables scalable control synthesis.

Abstract

Neural networks (NNs) are emerging as powerful tools to represent the dynamics of control systems with complicated physics or black-box components. Due to complexity of NNs, however, existing methods are unable to synthesize complex behaviors with guarantees for NN dynamic models (NNDMs). This work introduces a control synthesis framework for stochastic NNDMs with performance guarantees. The focus is on specifications expressed in linear temporal logic interpreted over finite traces (LTLf), and the approach is based on finite abstraction. Specifically, we leverage recent techniques for convex relaxation of NNs to formally abstract a NNDM into an interval Markov decision process (IMDP). Then, a strategy that maximizes the probability of satisfying a given specification is synthesized over the IMDP and mapped back to the underlying NNDM. We show that the process of abstracting NNDMs to IMDPs reduces to a set of convex optimization problems, hence guaranteeing efficiency. We also present an adaptive refinement procedure that makes the framework scalable. On several case studies, we illustrate the our framework is able to provide non-trivial guarantees of correctness for NNDMs with architectures of up to 5 hidden layers and hundreds of neurons per layer.