VeriFlow: Modeling Distributions for Neural Network Verification

TL;DR

The paper addresses the challenge of formally verifying neural networks on inputs that are meaningful in practice, rather than the entire input space. It introduces VeriFlow, a flow-based density model that is bijective and piecewise affine, preserving density level sets between the base distribution $B$ and the data distribution $D$ so verification can be confined to upper density level sets (UDLs) described by linear constraints in the latent space via $p_D(x)=p_B(F^{-1}(x))\left|\det \frac{\partial F^{-1}}{\partial x^T}\right|$. For radial base distributions, UDLs map to simple norm-based intervals, enabling straightforward latent-space descriptions and seamless integration with constraint-based verifiers and neuro-symbolic pipelines. Empirical results on MNIST and FashionMNIST demonstrate faithful latent norm distributions, competitive density estimation (vs. MACow) with a learnable radial base, and practical verification gains, with an open-source VeriFlow library and ONNX export to support broader adoption.

Abstract

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.

Figures (12)

• Figure 1: Verification of a global property
• Figure 2: Visualization of a verification pipeline for an in-distribution verification of a classifier using VeriFlow. The procedure starts by defining the UDL exactly in the latent space. The true classification range w.r.t. the UDL equals the result of pushing the set consecutively through the flow and the classifier. An over-approximation can be obtained via abstract interpretation.
• Figure 3: Comparison of PP-plots for VeriFlow on MNIST and FashionMNIST datasets. In both cases, the flexibility of the learnable norm distribution allows the model to tightly align norm distributions and the latent norms of the data.
• Figure 4: Runtime verification results and model samples.
• Figure 5: Negative log-likelihood (NLL) comparison of MACow and VeriFlow across datasets

Theorems & Definitions (12)

• definition thmcounterdefinition: Radial Distributions and Radial Profile
• definition thmcounterdefinition: $k$-Radial Distribution Construction
• definition thmcounterdefinition
• Proposition 1
• proof
• lemma thmcounterlemma
• proof
• Proposition 2: Density Level Set Preservation
• proof
• Corollary 1