# VeriFlow: Modeling Distributions for Neural Network Verification

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 41 of its 76 references that are in the map.
- First posted on arXiv 20 Jun 2024.

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

- [On Calibration of Modern Neural Networks](https://mlsanity.com/paper/1706.04599/) (2017)
- [What Uncertainties Do We Need in Bayesian Deep Learning for Computer Vision?](https://mlsanity.com/paper/1703.04977/) (2017)
- [Variational Inference with Normalizing Flows](https://mlsanity.com/paper/1505.05770/) (2015)
- [Glow: Generative Flow with Invertible 1x1 Convolutions](https://mlsanity.com/paper/1807.03039/) (2018)
- [Normalizing Flows for Probabilistic Modeling and Inference](https://mlsanity.com/paper/1912.02762/) (2019)
- [NICE: Non-linear Independent Components Estimation](https://mlsanity.com/paper/1410.8516/) (2014)
- [Aleatoric and Epistemic Uncertainty in Machine Learning: An Introduction to Concepts and Methods](https://mlsanity.com/paper/1910.09457/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Masked Autoregressive Flow for Density Estimation](https://mlsanity.com/paper/1705.07057/) (2017)
- [Improving Variational Inference with Inverse Autoregressive Flow](https://mlsanity.com/paper/1606.04934/) (2016)
- [Object Detection with Deep Learning: A Review](https://mlsanity.com/paper/1807.05511/) (2018)
- [Revisiting the Calibration of Modern Neural Networks](https://mlsanity.com/paper/2106.07998/) (2021)
- [Sophia: A Scalable Stochastic Second-order Optimizer for Language Model Pre-training](https://mlsanity.com/paper/2305.14342/) (2023)
- [Flow++: Improving Flow-Based Generative Models with Variational Dequantization and Architecture Design](https://mlsanity.com/paper/1902.00275/) (2019)
- [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)
- [Neural Autoregressive Flows](https://mlsanity.com/paper/1804.00779/) (2018)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Globally-Robust Neural Networks](https://mlsanity.com/paper/2102.08452/) (2021)
- [SoftFlow: Probabilistic Framework for Normalizing Flow on Manifolds](https://mlsanity.com/paper/2006.04604/) (2020)
- [Coupling-based Invertible Neural Networks Are Universal Diffeomorphism Approximators](https://mlsanity.com/paper/2006.11469/) (2020)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [A Primer on Neural Network Models for Natural Language Processing](https://mlsanity.com/paper/1510.00726/) (2015)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [Approximation Capabilities of Neural ODEs and Invertible Residual Networks](https://mlsanity.com/paper/1907.12998/) (2019)
- [Rethinking Lipschitz Neural Networks and Certified Robustness: A Boolean Function Perspective](https://mlsanity.com/paper/2210.01787/) (2022)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [MaCow: Masked Convolutional Generative Flow](https://mlsanity.com/paper/1902.04208/) (2019)
- [Emerging Convolutions for Generative Normalizing Flows](https://mlsanity.com/paper/1901.11137/) (2019)
- [Representational aspects of depth and conditioning in normalizing flows](https://mlsanity.com/paper/2010.01155/) (2020)
- [Neuro-Symbolic Verification of Deep Neural Networks](https://mlsanity.com/paper/2203.00938/) (2022)

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

- [On Uniformly Scaling Flows: A Density-Aligned Approach to Deep One-Class Classification](https://mlsanity.com/paper/2510.09452/) (2025)

## Abstract (arXiv)

Formal verification has emerged as a promising method to ensure the safety and reliability of neural networks. However, many relevant properties, such as fairness or global robustness, pertain to the entire input space. If one applies verification techniques naively, the neural network is checked even on inputs that do not occur in the real world and have no meaning. To tackle this shortcoming, we propose the VeriFlow architecture as a flow-based density model tailored to allow any verification approach to restrict its search to some data distribution of interest. We argue that our architecture is particularly well suited for this purpose because of two major properties. First, we show that the transformation that is defined by our model is piecewise affine. Therefore, the model allows the usage of verifiers based on constraint solving with linear arithmetic. Second, upper density level sets (UDL) of the data distribution are definable via linear constraints in the latent space. As a consequence, representations of UDLs specified by a given probability are effectively computable in the latent space. This property allows for effective verification with a fine-grained, probabilistically interpretable control of how a-typical the inputs subject to verification are.