# Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 38 references that are in the map.
- First posted on arXiv 17 Nov 2021.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations](https://mlsanity.com/paper/1712.08163/) (2017)
- [AReN: Assured ReLU NN Architecture for Model Predictive Control of LTI Systems](https://mlsanity.com/paper/1911.01608/) (2019)
- [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)
- [Two-Level Lattice Neural Network Architectures for Control of Nonlinear Systems](https://mlsanity.com/paper/2004.09628/) (2020)

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

- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [Towards a Certified Proof Checker for Deep Neural Network Verification](https://mlsanity.com/paper/2307.06299/) (2023)
- [IoUCert: Robustness Verification for Anchor-based Object Detectors](https://mlsanity.com/paper/2603.03043/) (2026)
- [Polynomial-Time Reachability for LTI Systems with Two-Level Lattice Neural Network Controllers](https://mlsanity.com/paper/2209.09400/) (2022)
- [CGDTest: A Constrained Gradient Descent Algorithm for Testing Neural Networks](https://mlsanity.com/paper/2304.01826/) (2023)
- [Extracting Forward Invariant Sets from Neural Network-Based Control Barrier Functions](https://mlsanity.com/paper/2501.15189/) (2025)
- [NNV3: Expanding Neural Network Verification to New Architectures and Domains](https://mlsanity.com/paper/2609.30050/) (2026)

## Abstract (arXiv)

In this paper, we present the tool Fast Box Analysis of Two-Level Lattice Neural Networks (Fast BATLLNN) as a fast verifier of box-like output constraints for Two-Level Lattice (TLL) Neural Networks (NNs). In particular, Fast BATLLNN can verify whether the output of a given TLL NN always lies within a specified hyper-rectangle whenever its input constrained to a specified convex polytope (not necessarily a hyper-rectangle). Fast BATLLNN uses the unique semantics of the TLL architecture and the decoupled nature of box-like output constraints to dramatically improve verification performance relative to known polynomial-time verification algorithms for TLLs with generic polytopic output constraints. In this paper, we evaluate the performance and scalability of Fast BATLLNN, both in its own right and compared to state-of-the-art NN verifiers applied to TLL NNs. Fast BATLLNN compares very favorably to even the fastest NN verifiers, completing our synthetic TLL test bench more than 400x faster than its nearest competitor.