Assumption Generation for the Verification of Learning-Enabled Autonomous Systems
This addresses the safety verification problem for autonomous systems with learning-enabled components, offering a method to handle DNN complexity and lack of formal specifications, though it appears incremental as it builds on existing assume-guarantee techniques.
The paper tackles the challenge of verifying safety in autonomous systems with deep neural network (DNN) perception components by proposing an assume-guarantee compositional approach that automatically synthesizes weakest assumptions on DNN behavior to guarantee system-level safety properties, enabling run-time monitoring and specification extraction for training.
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.