Assumption Generation for the Verification of Learning-Enabled Autonomous Systems

TL;DR

This paper introduces a compositional verification method that synthesizes assumptions on deep neural network behavior to ensure safety in autonomous systems, enabling formal guarantees despite DNN complexity and lack of formal specs.

Contribution

It presents a novel assume-guarantee approach that automatically generates weakest assumptions on DNN outputs to verify system-level safety properties.

Findings

Successfully applied to an autonomous airplane case study.

Synthesized assumptions serve as runtime monitors for DNN safety.

Assumptions can be used to guide DNN training and testing.

Abstract

Providing safety guarantees for autonomous systems is difficult as these systems operate in complex environments that require the use of learning-enabled components, such as deep neural networks (DNNs) for visual perception. DNNs are hard to analyze due to their size (they can have thousands or millions of parameters), lack of formal specifications (DNNs are typically learnt from labeled data, in the absence of any formal requirements), and sensitivity to small changes in the environment. We present an assume-guarantee style compositional approach for the formal verification of system-level safety properties of such autonomous systems. Our insight is that we can analyze the system in the absence of the DNN perception components by automatically synthesizing assumptions on the DNN behaviour that guarantee the satisfaction of the required safety properties. The synthesized assumptions are the weakest in the sense that they characterize the output sequences of all the possible DNNs that, plugged into the autonomous system, guarantee the required safety properties. The assumptions can be leveraged as run-time monitors over a deployed DNN to guarantee the safety of the overall system; they can also be mined to extract local specifications for use during training and testing of DNNs. We illustrate our approach on a case study taken from the autonomous airplanes domain that uses a complex DNN for perception.