# Polyhedral Enclosures: An Efficient Combinatorial Abstraction for Nonlinear Neural Feedback Systems

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Mar 2025.

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

- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)
- [A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems](https://mlsanity.com/paper/2601.08065/) (2026)
- [Stochastic World Models for Verifying Vision-Based Neural Feedback Systems](https://mlsanity.com/paper/2609.38120/) (2026)

## Abstract (arXiv)

As dynamical systems equipped with neural network controllers (neural feedback systems) become increasingly prevalent, it is critical to develop methods to ensure their safe operation. Verifying safety requires extending control theoretic analysis methods to these systems. Although existing techniques can efficiently handle linear neural feedback systems, relatively few scalable methods address the nonlinear case. We propose a novel algorithm for forward reachability analysis of nonlinear neural feedback systems. The approach leverages the structure of the nonlinear transition functions of the systems to compute tight polyhedral enclosures (i.e., abstractions). These enclosures, combined with the neural controller, are then encoded as a mixed-integer linear program (MILP). Optimizing this MILP yields a sound over-approximation of the forward-reachable set. Beyond the conference version of this work, we perform more extensive ablations, and introduce further optimizations to the algorithm. We evaluate our algorithm on representative benchmarks, and demonstrate significant improvements over the current state of the art.