# Compositional Verification for Autonomous Systems with Deep Learning Components

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Oct 2018.

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

- [ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems](https://mlsanity.com/paper/2511.02164/) (2025)
- [Incremental Neural Network Verification via Learned Conflicts](https://mlsanity.com/paper/2603.12232/) (2026)
- [Assumption Generation for the Verification of Learning-Enabled Autonomous Systems](https://mlsanity.com/paper/2305.18372/) (2023)
- [Safe AI -- How is this Possible?](https://mlsanity.com/paper/2201.10436/) (2022)
- [Certified Multi-Turn Robustness for LLM Safety via Compositional Bounds and Safety Persistence](https://mlsanity.com/paper/2608.20820/) (2026)
- [Marginal Calibration Does Not Compose: Hidden Dependence in Modular Robot Navigation](https://mlsanity.com/paper/2609.23731/) (2026)

## Abstract (arXiv)

As autonomy becomes prevalent in many applications, ranging from recommendation systems to fully autonomous vehicles, there is an increased need to provide safety guarantees for such systems. The problem is difficult, as these are large, complex systems which operate in uncertain environments, requiring data-driven machine-learning components. However, learning techniques such as Deep Neural Networks, widely used today, are inherently unpredictable and lack the theoretical foundations to provide strong assurance guarantees. We present a compositional approach for the scalable, formal verification of autonomous systems that contain Deep Neural Network components. The approach uses assume-guarantee reasoning whereby em contracts, encoding the input-output behavior of individual components, allow the designer to model and incorporate the behavior of the learning-enabled components working side-by-side with the other components. We illustrate the approach on an example taken from the autonomous vehicles domain.