# Polynomial-Time Reachability for LTI Systems with Two-Level Lattice Neural Network Controllers

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 14 references that are in the map.
- First posted on arXiv 20 Sep 2022.

## Builds on (most cited first, 9 of 9)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Lipschitz regularity of deep neural networks: analysis and efficient estimation](https://mlsanity.com/paper/1805.10965/) (2018)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [AReN: Assured ReLU NN Architecture for Model Predictive Control of LTI Systems](https://mlsanity.com/paper/1911.01608/) (2019)
- [Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks](https://mlsanity.com/paper/2111.09293/) (2021)
- [Bounding the Complexity of Formally Verifying Neural Networks: A Geometric Approach](https://mlsanity.com/paper/2012.11761/) (2020)
- [Safe-by-Repair: A Convex Optimization Approach for Repairing Unsafe Two-Level Lattice Neural Network Controllers](https://mlsanity.com/paper/2104.02788/) (2021)

## Abstract (arXiv)

In this paper, we consider the computational complexity of bounding the reachable set of a Linear Time-Invariant (LTI) system controlled by a Rectified Linear Unit (ReLU) Two-Level Lattice (TLL) Neural Network (NN) controller. In particular, we show that for such a system and controller, it is possible to compute the exact one-step reachable set in polynomial time in the size of the TLL NN controller (number of neurons). Additionally, we show that a tight bounding box of the reachable set is computable via two polynomial-time methods: one with polynomial complexity in the size of the TLL and the other with polynomial complexity in the Lipschitz constant of the controller and other problem parameters. Finally, we propose a pragmatic algorithm that adaptively combines the benefits of (semi-)exact reachability and approximate reachability, which we call L-TLLBox. We evaluate L-TLLBox with an empirical comparison to a state-of-the-art NN controller reachability tool. In our experiments, L-TLLBox completed reachability analysis as much as 5000x faster than this tool on the same network/system, while producing reach boxes that were from 0.08 to 1.42 times the area.