# Reachability Analysis for Feed-Forward Neural Networks using Face Lattices

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

## Key facts

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

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

- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [Traversing the Local Polytopes of ReLU Neural Networks: A Unified Approach for Network Verification](https://mlsanity.com/paper/2111.08922/) (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)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [Reachability Analysis of Convolutional Neural Networks](https://mlsanity.com/paper/2106.12074/) (2021)
- [Dual Graphs of Polyhedral Decompositions for the Detection of Adversarial Attacks](https://mlsanity.com/paper/2211.13305/) (2022)
- [Case Studies for Computing Density of Reachable States for Safe Autonomous Motion Planning](https://mlsanity.com/paper/2209.08073/) (2022)
- [Characterizing the Discrete Geometry of ReLU Networks](https://mlsanity.com/paper/2606.07728/) (2026)

## Abstract (arXiv)

Deep neural networks have been widely applied as an effective approach to handle complex and practical problems. However, one of the most fundamental open problems is the lack of formal methods to analyze the safety of their behaviors. To address this challenge, we propose a parallelizable technique to compute exact reachable sets of a neural network to an input set. Our method currently focuses on feed-forward neural networks with ReLU activation functions. One of the primary challenges for polytope-based approaches is identifying the intersection between intermediate polytopes and hyperplanes from neurons. In this regard, we present a new approach to construct the polytopes with the face lattice, a complete combinatorial structure. The correctness and performance of our methodology are evaluated by verifying the safety of ACAS Xu networks and other benchmarks. Compared to state-of-the-art methods such as Reluplex, Marabou, and NNV, our approach exhibits a significantly higher efficiency. Additionally, our approach is capable of constructing the complete input set given an output set, so that any input that leads to safety violation can be tracked.