# Assumption Generation for the Verification of Learning-Enabled Autonomous Systems

arXiv: https://arxiv.org/abs/2305.18372 · HTML: https://mlsanity.com/paper/2305.18372/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 30 references that are in the map.
- First posted on arXiv 27 May 2023.

## Builds on (most cited first, 15 of 15)

- [Fast and Accurate Deep Network Learning by Exponential Linear Units (ELUs)](https://mlsanity.com/paper/1511.07289/) (2015)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Learning Safe, Generalizable Perception-based Hybrid Control with Certificates](https://mlsanity.com/paper/2201.00932/) (2022)
- [DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks](https://mlsanity.com/paper/1710.00486/) (2017)
- [Verifying Controllers with Convolutional Neural Network-based Perception: A Case for Intelligible, Safe, and Precise Abstractions](https://mlsanity.com/paper/2111.05534/) (2021)
- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [Compositional Verification for Autonomous Systems with Deep Learning Components](https://mlsanity.com/paper/1810.08303/) (2018)
- [Counterexample-Guided Synthesis of Perception Models and Control](https://mlsanity.com/paper/1911.01523/) (2019)
- [Abstraction and Learning for Infinite-State Compositional Verification](https://mlsanity.com/paper/1309.5140/) (2013)
- [Real-time System Modeling and Verification through Labeled Transition System Analyser (LTSA)](https://mlsanity.com/paper/1803.05362/) (2018)
- [Pacti: Scaling Assume-Guarantee Reasoning for System Analysis and Design](https://mlsanity.com/paper/2303.17751/) (2023)

## Built on by (most cited first, 1 of 1)

- [Refining Perception Contracts: Case Studies in Vision-based Safe Auto-landing](https://mlsanity.com/paper/2311.08652/) (2023)

## Abstract (arXiv)

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.