# Provably Bounding Neural Network Preimages

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

## Key facts

- Cited by 29 papers in the map (data through 14 Oct 2026).
- Builds on 36 of its 52 references that are in the map.
- First posted on arXiv 2 Feb 2023.

## Builds on (most cited first, 30 of 36)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Convex optimization](https://mlsanity.com/paper/2106.01946/) (2021)
- [YOLO9000: Better, Faster, Stronger](https://mlsanity.com/paper/1612.08242/) (2016)
- [Enhancing The Reliability of Out-of-distribution Image Detection in Neural Networks](https://mlsanity.com/paper/1706.02690/) (2017)
- [Deep Anomaly Detection with Outlier Exposure](https://mlsanity.com/paper/1812.04606/) (2018)
- [Generalized Out-of-Distribution Detection: A Survey](https://mlsanity.com/paper/2110.11334/) (2021)
- [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 Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [ViM: Out-Of-Distribution with Virtual-logit Matching](https://mlsanity.com/paper/2203.10807/) (2022)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Certified Defenses against Adversarial Examples](https://mlsanity.com/paper/1801.09344/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [A Unified Survey on Anomaly, Novelty, Open-Set, and Out-of-Distribution Detection: Solutions and Future Challenges](https://mlsanity.com/paper/2110.14051/) (2021)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [ATOM: Robustifying Out-of-distribution Detection Using Outlier Mining](https://mlsanity.com/paper/2006.15207/) (2020)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Robust Out-of-distribution Detection for Neural Networks](https://mlsanity.com/paper/2003.09711/) (2020)
- [Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming](https://mlsanity.com/paper/2004.07876/) (2020)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components](https://mlsanity.com/paper/2011.11609/) (2020)
- [Improving Neural Network Verification through Spurious Region Guided Refinement](https://mlsanity.com/paper/2010.07722/) (2020)
- [Interpreting Neural Network Judgments via Minimal, Stable, and Symbolic Corrections](https://mlsanity.com/paper/1802.07384/) (2018)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)

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

- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees](https://mlsanity.com/paper/2602.16823/) (2026)
- [PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks](https://mlsanity.com/paper/2408.09262/) (2024)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [When to Trust AI: Advances and Challenges for Certification of Neural Networks](https://mlsanity.com/paper/2309.11196/) (2023)
- [Out of the Shadows: Exploring a Latent Space for Neural Network Verification](https://mlsanity.com/paper/2505.17854/) (2025)
- [Revisiting Differential Verification: Equivalence Verification with Confidence](https://mlsanity.com/paper/2410.20207/) (2024)
- [Robust Stability Analysis of Positive Lure System with Neural Network Feedback](https://mlsanity.com/paper/2505.18912/) (2025)
- [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)
- [LEVIS: Large Exact Verifiable Input Spaces for Neural Networks](https://mlsanity.com/paper/2408.08824/) (2024)
- [Formal Verification of Markov Processes with Learned Parameters](https://mlsanity.com/paper/2501.15767/) (2025)
- [Provably Explaining Neural Additive Models](https://mlsanity.com/paper/2602.17530/) (2026)
- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [The inverse problem for neural networks](https://mlsanity.com/paper/2308.14093/) (2023)
- [Redesigning Traffic Signs to Mitigate Machine-Learning Patch Attacks](https://mlsanity.com/paper/2402.04660/) (2024)
- [Training Safe Neural Networks with Global SDP Bounds](https://mlsanity.com/paper/2409.09687/) (2024)
- [Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report](https://mlsanity.com/paper/2411.14163/) (2024)
- [A Guide to Failure in Machine Learning: Reliability and Robustness from Foundations to Practice](https://mlsanity.com/paper/2503.00563/) (2025)
- [Provable Repair of Deep Neural Network Defects by Preimage Synthesis and Property Refinement](https://mlsanity.com/paper/2511.07741/) (2025)
- [Analyzing Symbolic Properties for DRL Agents in Systems and Networking](https://mlsanity.com/paper/2604.04914/) (2026)
- [Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2605.14758/) (2026)
- [Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networks](https://mlsanity.com/paper/2605.24084/) (2026)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)
- [MLSkip: Data Skipping for ML Filters via Lightweight Metadata](https://mlsanity.com/paper/2606.03946/) (2026)
- [A Survey on the Verification of Reinforcement Learning Policies](https://mlsanity.com/paper/2607.16210/) (2026)
- [Representation Learning for Exact Preimages](https://mlsanity.com/paper/2609.32018/) (2026)
- [CLAD: Constrained Abstract Domain for Neural Network Verification](https://mlsanity.com/paper/2609.34628/) (2026)

## Abstract (arXiv)

Most work on the formal verification of neural networks has focused on bounding the set of outputs that correspond to a given set of inputs (for example, bounded perturbations of a nominal input). However, many use cases of neural network verification require solving the inverse problem, or over-approximating the set of inputs that lead to certain outputs. We present the INVPROP algorithm for verifying properties over the preimage of a linearly constrained output set, which can be combined with branch-and-bound to increase precision. Contrary to other approaches, our efficient algorithm is GPU-accelerated and does not require a linear programming solver. We demonstrate our algorithm for identifying safe control regions for a dynamical system via backward reachability analysis, verifying adversarial robustness, and detecting out-of-distribution inputs to a neural network. Our results show that in certain settings, we find over-approximations over 2500x tighter than prior work while being 2.5x faster. By strengthening robustness verification with output constraints, we consistently verify more properties than the previous state-of-the-art on multiple benchmarks, including a large model with 167k neurons in VNN-COMP 2023. Our algorithm has been incorporated into the α,!β-CROWN verifier, available at https://abcrown.org.