# Formal Verification of End-to-End Learning in Cyber-Physical Systems: Progress and Challenges

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Jun 2020.

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

- [On Salience-Sensitive Sign Classification in Autonomous Vehicle Path Planning: Experimental Explorations with a Novel Dataset](https://mlsanity.com/paper/2112.00942/) (2021)
- [How Safe Am I Given What I See? Calibrated Prediction of Safety Chances for Image-Controlled Autonomy](https://mlsanity.com/paper/2308.12252/) (2023)

## Abstract (arXiv)

Autonomous systems -- such as self-driving cars, autonomous drones, and automated trains -- must come with strong safety guarantees. Over the past decade, techniques based on formal methods have enjoyed some success in providing strong correctness guarantees for large software systems including operating system kernels, cryptographic protocols, and control software for drones. These successes suggest it might be possible to ensure the safety of autonomous systems by constructing formal, computer-checked correctness proofs. This paper identifies three assumptions underlying existing formal verification techniques, explains how each of these assumptions limits the applicability of verification in autonomous systems, and summarizes preliminary work toward improving the strength of evidence provided by formal verification.