# Out of the Shadows: Exploring a Latent Space for Neural Network Verification

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 47 references that are in the map.
- First posted on arXiv 23 May 2025.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [Adversarial Machine Learning at Scale](https://mlsanity.com/paper/1611.01236/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Object Detection in 20 Years: A Survey](https://mlsanity.com/paper/1905.05055/) (2019)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (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)
- [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)
- [Recent Advancements in End-to-End Autonomous Driving using Deep Learning: A Survey](https://mlsanity.com/paper/2307.04370/) (2023)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Improving Neural Network Verification through Spurious Region Guided Refinement](https://mlsanity.com/paper/2010.07722/) (2020)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)
- [Neural Network Verification with PyRAT](https://mlsanity.com/paper/2410.23903/) (2024)
- [Set-Based Training for Neural Network Verification](https://mlsanity.com/paper/2401.14961/) (2024)
- [Hybrid Zonotopes Exactly Represent ReLU Neural Networks](https://mlsanity.com/paper/2304.02755/) (2023)
- [Utilizing Dependencies to Obtain Subsets of Reachable Sets](https://mlsanity.com/paper/1910.08354/) (2019)

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

- [Perception with Guarantees: Certified Pose Estimation via Reachability Analysis](https://mlsanity.com/paper/2602.10032/) (2026)
- [Lipschitz-Based Robustness Certification Under Floating-Point Execution](https://mlsanity.com/paper/2603.13334/) (2026)
- [Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems](https://mlsanity.com/paper/2605.02526/) (2026)
- [Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes](https://mlsanity.com/paper/2605.10474/) (2026)
- [The Misery of Mechanistic Interpretability: A Formal Perspective](https://mlsanity.com/paper/2609.15533/) (2026)
- [Representation Learning for Exact Preimages](https://mlsanity.com/paper/2609.32018/) (2026)

## Abstract (arXiv)

Neural networks are ubiquitous. However, they are often sensitive to small input changes. Hence, to prevent unexpected behavior in safety-critical applications, their formal verification -- a notoriously hard problem -- is necessary. Many state-of-the-art verification algorithms use reachability analysis or abstract interpretation to enclose the set of possible outputs of a neural network. Often, the verification is inconclusive due to the conservatism of the enclosure. To address this problem, we propose a novel specification-driven input refinement procedure, i.e., we iteratively enclose the preimage of a neural network for all unsafe outputs to reduce the set of possible inputs to only enclose the unsafe ones. For that, we transfer output specifications to the input space by exploiting a latent space, which is an artifact of the propagation of a projection-based set representation through a neural network. A projection-based set representation, e.g., a zonotope, is a "shadow" of a higher-dimensional set -- a latent space -- that does not change during a set propagation through a neural network. Hence, the input set and the output enclosure are "shadows" of the same latent space that we can use to transfer constraints. We present an efficient verification tool for neural networks that uses our iterative refinement to significantly reduce the number of subproblems in a branch-and-bound procedure. Using zonotopes as a set representation, unlike many other state-of-the-art approaches, our approach can be realized by only using matrix operations, which enables a significant speed-up through efficient GPU acceleration. We demonstrate that our tool achieves competitive performance compared to the top-ranking tools of the international neural network verification competition.