VeriFlow: Modeling Distributions for Neural Network Verification

TL;DR

VeriFlow introduces a flow-based density model that restricts neural network verification to relevant data distributions, improving the meaningfulness and efficiency of safety and fairness assessments.

Contribution

The paper presents VeriFlow, a novel flow-based density model enabling verification within specific data distributions using linear constraints, enhancing verification relevance and interpretability.

Findings

Model is piecewise affine, facilitating linear arithmetic verification.

Upper density level sets are definable via linear constraints.

Enables probabilistic control over input typicality during verification.

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.