# A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural Network Controlled Systems

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 16 references that are in the map.
- First posted on arXiv 27 Jun 2023.

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

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach](https://mlsanity.com/paper/2004.12273/) (2020)
- [TIRA: Toolbox for Interval Reachability Analysis](https://mlsanity.com/paper/1902.05204/) (2019)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [Tight Decomposition Functions for Continuous-Time Mixed-Monotone Systems with Disturbances](https://mlsanity.com/paper/2003.07975/) (2020)
- [Computing Robustly Forward Invariant Sets for Mixed-Monotone Systems](https://mlsanity.com/paper/2003.05912/) (2020)

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

- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [textttimmrax: A Parallelizable and Differentiable Toolbox for Interval Analysis and Mixed Monotone Reachability in JAX](https://mlsanity.com/paper/2401.11608/) (2024)
- [Forward Invariance in Neural Network Controlled Systems](https://mlsanity.com/paper/2309.09043/) (2023)
- [Mixed Monotonicity Reachability Analysis of Neural ODE: A Trade-Off Between Tightness and Efficiency](https://mlsanity.com/paper/2510.17859/) (2025)
- [Verifying Closed-Loop Contractivity of Learning-Based Controllers via Partitioning](https://mlsanity.com/paper/2512.02262/) (2025)
- [Beyond Prediction: Interval Neural Networks for Uncertainty-Aware System Identification](https://mlsanity.com/paper/2605.11460/) (2026)

## Abstract (arXiv)

In this paper, we present a toolbox for interval analysis in numpy, with an application to formal verification of neural network controlled systems. Using the notion of natural inclusion functions, we systematically construct interval bounds for a general class of mappings. The toolbox offers efficient computation of natural inclusion functions using compiled C code, as well as a familiar interface in numpy with its canonical features, such as n-dimensional arrays, matrix/vector operations, and vectorization. We then use this toolbox in formal verification of dynamical systems with neural network controllers, through the composition of their inclusion functions.