# Provable Preimage Under-Approximation for Neural Networks (Full Version)

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

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 50 references that are in the map.
- First posted on arXiv 5 May 2023.

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

- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [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)
- [End-to-end Driving via Conditional Imitation Learning](https://mlsanity.com/paper/1710.02410/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [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)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [A Statistical Approach to Assessing Neural Network Robustness](https://mlsanity.com/paper/1811.07209/) (2018)
- [Probabilistic Safety for Bayesian Neural Networks](https://mlsanity.com/paper/2004.10281/) (2020)
- [Robustness of Neural Networks: A Probabilistic and Practical Approach](https://mlsanity.com/paper/1902.05983/) (2019)
- [Abstraction based Output Range Analysis for Neural Networks](https://mlsanity.com/paper/2007.09527/) (2020)
- [Scalable Quantitative Verification For Deep Neural Networks](https://mlsanity.com/paper/2002.06864/) (2020)
- [Improving Neural Network Verification through Spurious Region Guided Refinement](https://mlsanity.com/paper/2010.07722/) (2020)
- [A Reachability Method for Verifying Dynamical Systems with Deep Neural Network Controllers](https://mlsanity.com/paper/1903.00520/) (2019)
- [SyReNN: A Tool for Analyzing Deep Neural Networks](https://mlsanity.com/paper/2101.03263/) (2021)
- [Efficient computation of the volume of a polytope in high-dimensions using Piecewise Deterministic Markov Processes](https://mlsanity.com/paper/2202.09129/) (2022)

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

- [PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks](https://mlsanity.com/paper/2408.09262/) (2024)
- [Adversarial Robustness Certification for Bayesian Neural Networks](https://mlsanity.com/paper/2306.13614/) (2023)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [Out of the Shadows: Exploring a Latent Space for Neural Network Verification](https://mlsanity.com/paper/2505.17854/) (2025)
- [Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound](https://mlsanity.com/paper/2405.17556/) (2024)
- [Efficient Preimage Approximation for Neural Network Certification](https://mlsanity.com/paper/2505.22798/) (2025)
- [Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification](https://mlsanity.com/paper/2507.05405/) (2025)
- [Formal Verification of Variational Quantum Circuits](https://mlsanity.com/paper/2507.10635/) (2025)
- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)
- [Probabilistic ML Verification via Weighted Model Integration](https://mlsanity.com/paper/2402.04892/) (2024)
- [Provable Repair of Deep Neural Network Defects by Preimage Synthesis and Property Refinement](https://mlsanity.com/paper/2511.07741/) (2025)
- [Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2605.14758/) (2026)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)
- [CLAD: Constrained Abstract Domain for Neural Network Verification](https://mlsanity.com/paper/2609.34628/) (2026)

## Abstract (arXiv)

Neural network verification mainly focuses on local robustness properties, which can be checked by bounding the image (set of outputs) of a given input set. However, often it is important to know whether a given property holds globally for the input domain, and if not then for what proportion of the input the property is true. To analyze such properties requires computing preimage abstractions of neural networks. In this work, we propose an efficient anytime algorithm for generating symbolic under-approximations of the preimage of any polyhedron output set for neural networks. Our algorithm combines a novel technique for cheaply computing polytope preimage under-approximations using linear relaxation, with a carefully-designed refinement procedure that iteratively partitions the input region into subregions using input and ReLU splitting in order to improve the approximation. Empirically, we validate the efficacy of our method across a range of domains, including a high-dimensional MNIST classification task beyond the reach of existing preimage computation methods. Finally, as use cases, we showcase the application to quantitative verification and robustness analysis. We present a sound and complete algorithm for the former, which exploits our disjoint union of polytopes representation to provide formal guarantees. For the latter, we find that our method can provide useful quantitative information even when standard verifiers cannot verify a robustness property.