# LEVIS: Large Exact Verifiable Input Spaces for Neural Networks

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 32 references that are in the map.
- First posted on arXiv 16 Aug 2024.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Trustworthy LLMs: a Survey and Guideline for Evaluating Large Language Models' Alignment](https://mlsanity.com/paper/2308.05374/) (2023)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [OMLT: Optimization & Machine Learning Toolkit](https://mlsanity.com/paper/2202.02414/) (2022)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [On The Verification of Neural ODEs with Stochastic Guarantees](https://mlsanity.com/paper/2012.08863/) (2020)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)
- [Reinforcement Learning for Optimal Primary Frequency Control: A Lyapunov Approach](https://mlsanity.com/paper/2009.05654/) (2020)
- [Modeling Design and Control Problems Involving Neural Network Surrogates](https://mlsanity.com/paper/2111.10489/) (2021)
- [Optimization-Based Bound Tightening using a Strengthened QC-Relaxation of the Optimal Power Flow Problem](https://mlsanity.com/paper/1809.04565/) (2018)
- [Persistent Classification: A New Approach to Stability of Data and Adversarial Examples](https://mlsanity.com/paper/2404.08069/) (2024)

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

- [CLAD: Constrained Abstract Domain for Neural Network Verification](https://mlsanity.com/paper/2609.34628/) (2026)

## Abstract (arXiv)

The robustness of neural networks is crucial in safety-critical applications, where identifying a reliable input space is essential for effective model selection, robustness evaluation, and the development of reliable control strategies. Most existing robustness verification methods assess the worst-case output under the assumption that the input space is known. However, precisely identifying a verifiable input space (C), where no adversarial examples exist, is challenging due to the possible high dimensionality, discontinuity, and non-convex nature of the input space. To address this challenge, we propose a novel framework, **LEVIS**, consisting of **LEVIS-α** and **LEVIS-beta**. **LEVIS-α** identifies a single, large verifiable ball that intersects at least two boundaries of a bounded region (C), while **LEVIS-beta** systematically captures the entirety of the verifiable space by integrating multiple verifiable balls. Our contributions include: (1) introducing a verification framework that uses mixed-integer programming (MIP) to compute nearest and directional adversarial points, (2) integrating complementarity-constrained (CC) optimization with a reduced MIP formulation for scalability, achieving up to a 6 times runtime reduction, (3) theoretically characterizing the properties of the verifiable balls obtained by **LEVIS-α**, and (4) validating the approach across applications including electrical power flow regression and image classification, with demonstrated performance gains and geometric insights into the verifiable region.