# Verifying Learning-Based Robotic Navigation Systems

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

## Key facts

- Cited by 33 papers in the map (data through 14 Oct 2026).
- Builds on 50 of its 97 references that are in the map.
- First posted on arXiv 26 May 2022.

## Builds on (most cited first, 30 of 50)

- [Very Deep Convolutional Networks for Large-Scale Image Recognition](https://mlsanity.com/paper/1409.1556/) (2014)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [Adversarial examples in the physical world](https://mlsanity.com/paper/1607.02533/) (2016)
- [Deep Reinforcement Learning with Double Q-learning](https://mlsanity.com/paper/1509.06461/) (2015)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Constrained Policy Optimization](https://mlsanity.com/paper/1705.10528/) (2017)
- [Universal adversarial perturbations](https://mlsanity.com/paper/1610.08401/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Safe Learning in Robotics: From Learning-Based Control to Safe Reinforcement Learning](https://mlsanity.com/paper/2108.06266/) (2021)
- [Deep Reinforcement Learning: An Overview](https://mlsanity.com/paper/1701.07274/) (2017)
- [Responsive Safety in Reinforcement Learning by PID Lagrangian Methods](https://mlsanity.com/paper/2007.03964/) (2020)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Unity: A General Platform for Intelligent Agents](https://mlsanity.com/paper/1809.02627/) (2018)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [IPO: Interior-point Policy Optimization under Constraints](https://mlsanity.com/paper/1910.09615/) (2019)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Safe Reinforcement Learning in Constrained Markov Decision Processes](https://mlsanity.com/paper/2008.06626/) (2020)
- [Virtual-to-real Deep Reinforcement Learning: Continuous Control of Mobile Robots for Mapless Navigation](https://mlsanity.com/paper/1703.00420/) (2017)
- [Sample Efficient Reinforcement Learning with REINFORCE](https://mlsanity.com/paper/2010.11364/) (2020)
- [Learning Navigation Behaviors End-to-End with AutoRL](https://mlsanity.com/paper/1809.10124/) (2018)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [Deep Reinforcement Learning with Successor Features for Navigation across Similar Environments](https://mlsanity.com/paper/1612.05533/) (2016)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)

## Built on by (most cited first, 30 of 33)

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Local vs. Global Interpretability: A Computational Complexity Perspective](https://mlsanity.com/paper/2406.02981/) (2024)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System](https://mlsanity.com/paper/2212.03287/) (2022)
- [Shield Synthesis for LTL Modulo Theories](https://mlsanity.com/paper/2406.04184/) (2024)
- [Constrained Reinforcement Learning for Robotics via Scenario-Based Programming](https://mlsanity.com/paper/2206.09603/) (2022)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation](https://mlsanity.com/paper/2408.03915/) (2024)
- [Safe Deep Reinforcement Learning by Verifying Task-Level Properties](https://mlsanity.com/paper/2302.10030/) (2023)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [Online Safety Property Collection and Refinement for Safe Deep Reinforcement Learning in Mapless Navigation](https://mlsanity.com/paper/2302.06695/) (2023)
- [Analyzing Adversarial Inputs in Deep Reinforcement Learning](https://mlsanity.com/paper/2402.05284/) (2024)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks](https://mlsanity.com/paper/2407.01639/) (2024)
- [Towards Formal Verification of Deep Neural Networks for Object Detection](https://mlsanity.com/paper/2407.01295/) (2024)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation](https://mlsanity.com/paper/2505.05235/) (2025)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [Realizable Continuous-Space Shields for Safe Reinforcement Learning](https://mlsanity.com/paper/2410.02038/) (2024)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Designing Control Barrier Function via Probabilistic Enumeration for Safe Reinforcement Learning Navigation](https://mlsanity.com/paper/2504.21643/) (2025)
- [Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification](https://mlsanity.com/paper/2507.05405/) (2025)
- [Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing](https://mlsanity.com/paper/2312.05890/) (2023)
- [Aquatic Navigation: A Challenging Benchmark for Deep Reinforcement Learning](https://mlsanity.com/paper/2405.20534/) (2024)

## Abstract (arXiv)

Deep reinforcement learning (DRL) has become a dominant deep-learning paradigm for tasks where complex policies are learned within reactive systems. Unfortunately, these policies are known to be susceptible to bugs. Despite significant progress in DNN verification, there has been little work demonstrating the use of modern verification tools on real-world, DRL-controlled systems. In this case study, we attempt to begin bridging this gap, and focus on the important task of mapless robotic navigation -- a classic robotics problem, in which a robot, usually controlled by a DRL agent, needs to efficiently and safely navigate through an unknown arena towards a target. We demonstrate how modern verification engines can be used for effective model selection, i.e., selecting the best available policy for the robot in question from a pool of candidate policies. Specifically, we use verification to detect and rule out policies that may demonstrate suboptimal behavior, such as collisions and infinite loops. We also apply verification to identify models with overly conservative behavior, thus allowing users to choose superior policies, which might be better at finding shorter paths to a target. To validate our work, we conducted extensive experiments on an actual robot, and confirmed that the suboptimal policies detected by our method were indeed flawed. We also demonstrate the superiority of our verification-driven approach over state-of-the-art, gradient attacks. Our work is the first to establish the usefulness of DNN verification in identifying and filtering out suboptimal DRL policies in real-world robots, and we believe that the methods presented here are applicable to a wide range of systems that incorporate deep-learning-based agents.