# Verifying Controllers with Convolutional Neural Network-based Perception: A Case for Intelligible, Safe, and Precise Abstractions

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

## Key facts

- Cited by 19 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Nov 2021.

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

- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [How Safe Am I Given What I See? Calibrated Prediction of Safety Chances for Image-Controlled Autonomy](https://mlsanity.com/paper/2308.12252/) (2023)
- [Bridging Dimensions: Confident Reachability for High-Dimensional Controllers](https://mlsanity.com/paper/2311.04843/) (2023)
- [Designing Latent Safety Filters using Pre-Trained Vision Models](https://mlsanity.com/paper/2509.14758/) (2025)
- [Certifying Robustness of Learning-Based Keypoint Detection and Pose Estimation Methods](https://mlsanity.com/paper/2408.00117/) (2024)
- [Scenario-based Compositional Verification of Autonomous Systems with Neural Perception](https://mlsanity.com/paper/2504.20942/) (2025)
- [Conformal Safety Shielding for Imperfect-Perception Agents](https://mlsanity.com/paper/2506.17275/) (2025)
- [Learning Ensembles of Vision-based Safety Control Filters](https://mlsanity.com/paper/2412.02029/) (2024)
- [Assumption Generation for the Verification of Learning-Enabled Autonomous Systems](https://mlsanity.com/paper/2305.18372/) (2023)
- [Refining Perception Contracts: Case Studies in Vision-based Safe Auto-landing](https://mlsanity.com/paper/2311.08652/) (2023)
- [Pre-Trained Vision Models as Perception Backbones for Safety Filters in Autonomous Driving](https://mlsanity.com/paper/2410.22585/) (2024)
- [Learning Vision-Based Neural Network Controllers with Semi-Probabilistic Safety Guarantees](https://mlsanity.com/paper/2503.00191/) (2025)
- [How Safe Will I Be Given What I Saw? Calibrated Prediction of Safety Chances for Image-Controlled Autonomy](https://mlsanity.com/paper/2508.09346/) (2025)
- [Efficient Reachability Analysis for Convolutional Neural Networks Using Hybrid Zonotopes](https://mlsanity.com/paper/2503.10840/) (2025)
- [Verification of Visual Controllers via Compositional Geometric Transformations](https://mlsanity.com/paper/2507.04523/) (2025)
- [From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications](https://mlsanity.com/paper/2603.05604/) (2026)
- [Correcting Learning-based Perception for Safety](https://mlsanity.com/paper/2609.22108/) (2026)
- [Stochastic World Models for Verifying Vision-Based Neural Feedback Systems](https://mlsanity.com/paper/2609.38120/) (2026)

## Abstract (arXiv)

Convolutional Neural Networks (CNN) for object detection, lane detection, and segmentation now sit at the head of most autonomy pipelines, and yet, their safety analysis remains an important challenge. Formal analysis of perception models is fundamentally difficult because their correctness is hard if not impossible to specify. We present a technique for inferring intelligible and safe abstractions for perception models from system-level safety requirements, data, and program analysis of the modules that are downstream from perception. The technique can help tradeoff safety, size, and precision, in creating abstractions and the subsequent verification. We apply the method to two significant case studies based on high-fidelity simulations (a) a vision-based lane keeping controller for an autonomous vehicle and (b) a controller for an agricultural robot. We show how the generated abstractions can be composed with the downstream modules and then the resulting abstract system can be verified using program analysis tools like CBMC. Detailed evaluations of the impacts of size, safety requirements, and the environmental parameters (e.g., lighting, road surface, plant type) on the precision of the generated abstractions suggest that the approach can help guide the search for corner cases and safe operating envelops.