# Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components

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

## Key facts

- Cited by 36 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Nov 2020.

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

- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Efficient Neural Network Analysis with Sum-of-Infeasibilities](https://mlsanity.com/paper/2203.11201/) (2022)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Neural Network Verification in Control](https://mlsanity.com/paper/2110.01388/) (2021)
- [Traversing the Local Polytopes of ReLU Neural Networks: A Unified Approach for Network Verification](https://mlsanity.com/paper/2111.08922/) (2021)
- [A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis](https://mlsanity.com/paper/2112.05745/) (2021)
- [Learning Density Distribution of Reachable States for Autonomous Systems](https://mlsanity.com/paper/2109.06728/) (2021)
- [ReLU Neural Networks, Polyhedral Decompositions, and Persistent Homolog](https://mlsanity.com/paper/2306.17418/) (2023)
- [Backward Reachability Analysis for Neural Feedback Loops](https://mlsanity.com/paper/2204.08319/) (2022)
- [PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks](https://mlsanity.com/paper/2408.09262/) (2024)
- [A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops](https://mlsanity.com/paper/2210.07918/) (2022)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [DRIP: Domain Refinement Iteration with Polytopes for Backward Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2212.04646/) (2022)
- [Provable Fairness for Neural Network Models using Formal Verification](https://mlsanity.com/paper/2212.08578/) (2022)
- [Constrained Feedforward Neural Network Training via Reachability Analysis](https://mlsanity.com/paper/2107.07696/) (2021)
- [Probabilistic Verification of ReLU Neural Networks via Characteristic Functions](https://mlsanity.com/paper/2212.01544/) (2022)
- [Chordal Sparsity for SDP-based Neural Network Verification](https://mlsanity.com/paper/2206.03482/) (2022)
- [Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq](https://mlsanity.com/paper/2301.12893/) (2023)
- [Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis](https://mlsanity.com/paper/2406.04476/) (2024)
- [Predictive Uncertainty for Runtime Assurance of a Real-Time Computer Vision-Based Landing System](https://mlsanity.com/paper/2508.09732/) (2025)
- [Marching Neurons: Accurate Surface Extraction for Neural Implicit Shapes](https://mlsanity.com/paper/2509.21007/) (2025)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems](https://mlsanity.com/paper/2505.03643/) (2025)

## Abstract (arXiv)

We present a method for computing exact reachable sets for deep neural networks with rectified linear unit (ReLU) activation. Our method is well-suited for use in rigorous safety analysis of robotic perception and control systems with deep neural network components. Our algorithm can compute both forward and backward reachable sets for a ReLU network iterated over multiple time steps, as would be found in a perception-action loop in a robotic system. Our algorithm is unique in that it builds the reachable sets by incrementally enumerating polyhedral cells in the input space, rather than iterating layer-by-layer through the network as in other methods. If an unsafe cell is found, our algorithm can return this result without completing the full reachability computation, thus giving an anytime property that accelerates safety verification. In addition, our method requires less memory during execution compared to existing methods where memory can be a limiting factor. We demonstrate our algorithm on safety verification of the ACAS Xu aircraft advisory system. We find unsafe actions many times faster than the fastest existing method and certify no unsafe actions exist in about twice the time of the existing method. We also compute forward and backward reachable sets for a learned model of pendulum dynamics over a 50 time step horizon in 87s on a laptop computer. Algorithm source code: https://github.com/StanfordMSL/Neural-Network-Reach.