VeriFlow: Modeling Distributions for Neural Network Verification

## Abstract

Abstract Formal verification has emerged as a promising method to ensure the safety and reliability of neural networks.
Naively verifying a safety property amounts to ensuring the safety of a neural network for the whole input space irrespective of any training or test set.
However, this also implies that the safety of the neural network is checked even for inputs that do not occur in the real-world and have no meaning at all, often resulting in spurious errors.
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 the 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 and log-density function that are defined by our model are piece-wise affine. Therefore, the model allows the usage of verifiers based on SMT with linear arithmetic.
Second, upper density level sets (UDL) of the data distribution take the shape of an L p superscript 𝐿 𝑝 L^{p} italic_L start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT -ball in the latent space. As a consequence, representations of UDLs specified by a given probability are effectively computable in latent space. This allows for SMT and abstract interpretation approaches with fine-grained, probabilistically interpretable, control regarding on how (a)typical the inputs subject to verification are.

## 1 Introduction

The outstanding performance of neural networks in tasks such as object detection [] image classification [], anomaly detection [] and natural language processing [] made them a popular solution for many real-world-applications, including safety-critical ones.
With the increasing popularity of neural networks, defects and limitations of these systems have been witnessed by the general public. The AI incident database (^1^11[https://incidentdatabase.ai/](https://incidentdatabase.ai/)) keeps track of harms and near-harms caused by AI-Systems in the real world.

Ideally, safety and fairness properties of such inherently opaque neural networks should be formally guaranteed when used in safety-critical applications.
As a solution, formal verification can be used to check whether a neural network satisfies a given safety property for the entire input space, or whether there exists some (synthetic) input for which the desired property is violated.
This is in contrast to the statistical testing methods classically employed in Machine learning, where the output of the neural network is checked for a finite set of samples, usually from a held-out test set.

However, state-of-the-art formal verification methods only allow for verifying either global or local properties.
Global properties ensure a specific behaviour of the neural network on the whole input space.
As an example, fairness properties require the neural network to predict the same output for any two inputs that only differ in some sensitive attribute.
Local properties, on the other hand, ensure a specific behaviour of the neural network only in some part of the input space that is usually restricted using the training set.
One well-studied example for a local property is adversarial robustness which requires the neural network to classify any point from the data set as the same class as any minor perturbation of that point.
However, both global and local properties have a shortcoming: As global properties verify the property for the whole input space, we may not want or need to verify the property for noise-inputs or on regions of the input space for which there were no training samples available (epistemic uncertainty).
Local properties, on the other hand, suffer from the same problem as statistical testing, i.e., they rely on a high-quality data set that the verification property is based on.

To overcome this problem, we design a flow model tailored towards the application in neural network verification and leverage it to restrict the input space of the neural network under verification to the underlying data distribution.
In contrast to generative adversarial networks (GANs) and variational autoencoders, flow models do not only allow for efficient sampling but also provide probabilistic interpretability [, , , , ].
That is an important feature to facilitate fine-grained probabilistic control when restricting the input space to typical inputs when specifying the verification property.
This approach makes the verification property less reliant on the dataset, while still keeping the input space focused on meaningful data.

To illustrate this idea, consider a neural network trained to classify images of handwritten digits.
We want the classifier to always be confident about it’s classification of a certain digit.
More precisely, our verification property is that the neural network’s confidence is high if it classifies an image as 0 0 or $9$, respectively.
If the neural network does not satisfy the verification property, the verification tool will return an image that is classified as 0 0 or $9$ with low confidence.
Such counterexamples are illustrated in Figure 1.
The two counterexamples on the left side in Figure 1 were found with a traditional verifier without leveraging our flow model.
These counterexample are noise images without any meaning and come from a region of the input space with high epistemic uncertainty.
However, the counterexamples on the right side of Figure 1 were obtained by leveraging our flow model to restrict the input space of the verification property to typical inputs.
In the context of Figure 1, the right side restricts the input space to a UDL of given probability and therefore, the counterexamples come from within the data distribution and provide a deeper understanding of the classifiers’ weakness when used in a real-world scenario.
We refer to Section 5 for more details on this experiment.

Figure: Counterexamples without flow model.
Refer to caption: extracted/5651567/conf_9_digit_0_without_flow.png

We briefly list our main theoretical results. We design a novel flow model with $L_{1}$-radially monotonic base distributions that provides the following theoretical properties crucial for the verification domain while outperforming its normalizing counterparts in nearly all benchmarks.
Specifically, we design a flow model that:

- 1.
Maps upper/lower (log-)density level sets of the target distribution to upper/lower (log-)density level sets of the base distribution allowing for fine-grained probabilistic control during sampling.
- 2.
Allows the definition of the pre-image of a density level set in the latent space via linear constraints.
- 3.
Has a piece-wise affine log-density function for the case of a Laplacian base distribution, facilitating efficient computation and analysis.

We identify sufficient conditions for a flow layer to have the aforementioned properties and survey the literature and present a set of several layers - with its most representative members being additive coupling layers and bijective affine layers - that can be arbitrarily combined to yield a flow with the desired properties.

## 2 Verification Background

Verification of neural networks refers to checking whether a given network $f$ satisfies a given semantic property $P$ for all possible inputs $x$.
This semantic property $P$ may consist of a precondition $\phi$ and a postcondition $\psi$ usually related as an implication $\phi(x)\implies\psi(f(x))$.
There are two conceptually different approaches for verifying such properties for neural networks, namely SMT based verification and abstract interpretation.

##### SMT based Verification

An SMT based verification approach typically involves translating $f$ along with $P$ to a logical formula $\Psi_{f,P}$ that is designed to be valid if and only if the network $f$ satisfies the property $P$. For an understanding on how the neural network along with the verification condition is compiled into the formula, we refer to prior works such as the book by Albarghouthi [, ].

On a technical level, the validity of such logical formulas can be checked using off-the-shelf Satisfiability Modulo Theorem (SMT) Solvers. The runtime of such solvers depends on the pre-/post- and verification condition which in turn depends on the architecture of the neural networks that are compiled into the formula.
If the verification condition falls into a quantifier free fragment of linear arithmetic, efficient solvers such as Marabou can be used [].
This is the case if the network only used linear components, as we ensure in our case with ReLu-activation functions.
If, however, the formula contains non-linearities (e.g., due to the neural network containing non-linear activation functions such as tanh), then one may need to use more powerful but slower solvers such as dReal [].

On a conceptual level, we check the validity of $\Psi_{f,P}$ by checking the unsatisfiability of the negated verification condition $\neg\Psi_{f,P}$.
If the negated verification condition $\neg\Psi_{f,P}$ is unsatisfiable, then $\Psi_{f,P}$ is valid and by construction $f$ satisfies $P$.
If, however, $\neg\Psi_{f,P}$ is satisfiable, then $\Psi_{f,P}$ is invalid and the neural network is incorrect. In that case, the assignment $x$ for satisfying $\neg\Psi_{f,P}$ is a counterexample that shows the violation of the verification property by the neural network.
More precisely, the counterexample $x$ satisfies the precondition $\phi(x)$ but violates postcondition $\psi(f(x))$.
Such a counterexample was presented in Figure 1.
While a main advantage of SMT based verification tools is their precision and ability to provide counterexamples for when the verification property is violated by the neural network, their drawback is the computational runtime for generating positive proof certificates.
In contrast to verifying unsafe neural networks that merely require a counterexample to be found, which terminates the verification process, safe neural networks require fully rejecting the satisfiability of $\neg\Psi_{f,P}$.
This gap is closed with a less precise and conceptually different verification approach called abstract interpretation. Abstract interpretation can provide fast positive proof certificates for safe neural networks.

##### Abstract Interpretation

The main idea of abstract interpretation is to symbolically run a neural network on an abstract domain.
An abstract domain provides the basic structure of the symbolic elements that in turn represent a subspace of the input, latent or output space.
Examples for abstract domains are polytopes and widely-used zonotopes [, ].
In this paper, we exclusively consider the latter.

The zonotope in the input space of the neural network represents the set of all inputs satisfying the precondition.
This is a the geometric representation of the aforementioned logical precondition.
During the symbolic execution procedure, the input zonotope is iteratively passed through each layer of the neural network by over-approximating the behaviour of each layer.
This results in an over-approximation of all possible outputs of the neural network to the given input-level zonotope.

Until now, the aforementioned postcondition of our logical verification property has been disregarded.
However, similar to the precondition, the postcondition also induces a subspace in the output space.
Therefore, it is sufficient to check whether the output-level zonotope provided by the abstract interpretation procedure lays inside the zonotope induced by the postcondition. The latter is called safe space. If the output-level zonotope lays inside the safe space, the verification property is guaranteed by the neural network and the verification was successful.
If the output-level zonotope lays fully outside safe space, then the verification property is guaranteed to not hold.
If, however, the output-level zonotope partially lays outside the safe space, no assertion can be made due to the over-approximation of the abstract interpreter. This means, the neural network may or may not satisfy the verification property.

There exists several verification frameworks that implement abstract interpretation. [, ].
Unlike the aforementioned SMT based verifiers, abstract interpretation frameworks do not conceptually rely on piecewise affinity of the neural network, may allow more divers neural network architectures but are not able to return counterexamples if the verification condition is violated [, ].

## 3 Flow Models

Flow models provide an elegant way to define a density estimator and a generative model by a single network.
More precisely, we train a flow to transform a
simple base (or latent) distribution $B$ into the data (or target) distribution $D$ using a continuous invertible map with continuous inverse,
i.e. a diffeomorphism (^2^22Note that we define the flows in the direction from base distribution to data distribution. This is inverse to the direction suggested by the common name ”Normalizing Flow”, but better suited for our analysis. Apart from that, the two definitions are obviously equivalent.). The map $F$ is implemented by an invertible neural
network. We obtain a a density estimator and a generative model by applying the flow in both directions:

- 1.
Sampling is performed by first sampling $z\sim B$ and then computing
the map $F(z)$.
- 2.
Computing the likelihood
$p_{D}(x)$ can be done using the change of variables formula
[]:
$\displaystyle p_{D}(x)$
$\displaystyle=$
$\displaystyle\left|\textrm{det}\frac{\partial F^{-1}}{\partial x^{T}}\right|p_
{B}(F^{-1}(x)).$
(1)

While most neural networks are intrinsically differentiable, they do not represent
bijections in general. One needs to design specific architectures
that restrict the hypothesis space to diffeomorphisms. Note that the existence of an inverse does not necessarily imply
that the inverse can be easily computed. There are
flow architectures that allow only one of the above operations to be efficiently performed
[, ]. However, it is also not uncommon that both operation have the same complexity []. The major goal of this work is to design a flow architecture that does not only allow to perform both operations efficiently, but it also allows an efficient analysis of the flow in a verification context.

For the latter, it is often required to not only sample individually, but verify on a space of sampled objects.
We define the spaces containing high-density and low-density samples as upper- and lower density level sets.

###### Definition 1

Given the density of the input distribution $p_{D}:\mathbb{R}^{d}\rightarrow\mathbb{R}_{+}$. The set of points whose density exceeds a given threshold $t$ is called the upper density level set (UDL) and is defined as ${L^{\uparrow}_{D}(t)\coloneqq\{x\in\mathbb{R}^{d}\mid p_{D}(x)>t\}}$.
Respectively, the lower density level set (LDL) contains the set of points deceeding the density threshold: ${{L^{\downarrow}_{D}(t)\coloneqq\{x\in\mathbb{R}^{d}\mid p_{D}(x)\leq t\}}=
\mathbb{R}^{d}\setminus L^{\uparrow}_{D}}$. If for $q\in[0,1]$ there is a unique UDL of $D$ with probability $q$, then we denote this set by $\text{UDL}_{D}(q)$.

Upper density level sets naturally capture the center of the distribution while LDLs capture the tail.
Note that the existence and uniqueness of the UDL with given probability is guaranteed if $P_{D}(\{x\mid p(x)_{D}=t\})=0$ for all $t>0$ and the image of the density function $p_{D}$ is a (possibly infinite) initial segment of the positive reals.

###### Definition 1

##### Base Distributions

An isotropic Gaussian is the by far most common choice for the base distribution of a flow model. In this case, we refer to the model as a normalizing flow. A normal distribution might seem to be the natural choice, but it is definitely not the only option.
In fact, the Knothe-Rosenblatt Rearrangement Theorem [, ] guarantees that any two absolutely continuous distributions can be transformed into one another via a diffeomorphism between their supports.
In the next section, we will show that under certain conditions $p$-radial monotonic base distributions with $p\in\{1,\infty\}$, especially the Laplacian distributions, provide some merits that allow efficient analysis of our flow model in verification scenarios. In our case, it even turned out that changing the base distribution boosted the performance of the model and the stability of the training.

###### Definition 2

Let $X$ be random variable over $\mathbb{R}^{d}$. We say that $X$ is $p$-radially distributed if there is a function $g:\mathbb{R}_{+}\to\mathbb{R}_{+}$ such $p(x)=g(|x|_{p})$.
If $g$ is also strictly monotonically decreasing, then we say that $X$ is $p$-radial monotonic.

Moreover, $p$-radial distributions are easily definable starting from the corresponding distribution of $p$-norms.
In the following, let $V^{d}_{p}(r)$ is the hyper volume of the $L^{p}$-ball of radius $r$ in $\mathbb{R}^{d}$.

###### Definition 3

Let $\rho:\mathbb{R}_{+}\to\mathbb{R}_{+}$ be a probability density and $p\in\mathbb{N}_{>0}\cup\{\infty\}$.
Then we call $R_{\rho,p,d}$ the $p$-radial distribution with $p$-norm distribution $\rho$ in $d$-dimensional space, which is given by the probability density function
$p_{R_{\rho,p,d}}(x)=\rho(|x|_{p})\left(\frac{\partial V^{d}_{p}(r)}{\partial r
}(|x|_{p})\right)^{-1}$.

In other words, a $p$-radial distribution is completely determined by the distribution of the $p$-norm.
Note that if $X$ is radial monotonic, it does not imply that $p_{|X|_{p}}$ is monotonic. For instance, if $X$ is a $d$-dimensional standard Gaussian, then $X$ is $2$-radial monotonic but $|X|_{2}$ is $\chi(d)$ distributed and hence not monotonic for $d>1$.

The following observation is crucial for our application: The density level sets of a $p$-radial monotonic distribution are $L^{p}$-balls. By choosing $r(q)\coloneqq\textrm{quantile}_{|X|_{p}}\left(q\right)$, we obtain the following result:
{prop}[]
Let $X$ be a $p$-radial monotonic random variable on $\mathbb{R}^{d}$. Then there is a function $r:[0,1)\to\mathbb{R}_{+}$ such that for any $q\in[0,1)$, the upper density level set of probability $q$ is given by $\textrm{UDL}_{X}(q)=\mathbb{B}^{d}_{p}(r(q))$, where $\mathbb{B}^{d}_{p}(r)$ is the $L^{p}$-ball of radius $r$ with center at the origin.

###### Definition 2

###### Definition 3

### 3.1 Good Properties for Verification

As we argued earlier, piece-wise affinity is crucial for efficient SMT based verification. For the usage of our flow model this means that the transformation as well as the (log-)likelihood of the model should be piece-wise affine.
A natural approach to start off is therefore the use of piece-wise affine networks, represented e.g. by ReLU networks. If we can ensure that the defined function is bijective, then we obtain a continuous piece-wise affine bijection where
the affine regions can be represented as intersections of open and closed half-spaces []. Hence, the regions are contained in
in the Borel algebra $\mathcal{B}(\mathbb{R}^{d})$. It is straight forward to
show that the change of variables formula applies piece-wise. We include a proof for the sake of self-containedness.

[]
Let $F:\mathbb{R}^{n}\to\mathbb{R}^{n}$ be a piece-wise affine bijection with affine partition $R_{1},\ldots,R_{n}\in\mathcal{B}(\mathbb{R}^{d})$ of the input space and corresponding affine functions $f_{1},\ldots,f_{n}$.
Let $X$ be an absolutely continuous random variable. Then
$p_{F(X)}(y)=p_{X}(F^{-1}(y))\left|\det\frac{\partial F^{-1}}{\partial y}\right|$,
where the Jacobean of $F^{-1}$ is evaluated piece-wise. More precisely,
$\left|\det\frac{\partial F^{-1}}{\partial y}\right|=\sum_{i}\left|\det\frac{
\partial f_{i}^{-1}}{\partial y}\right|\cdot\mathbb{I}\left[F^{-1}(x)\in R_{i}\right]$, where $\mathbb{I}$ is the indicator function.

###### Proof

We define the random variable

$$ $C:\mathbb{R}^{d}\to\{1,\ldots,n\};x\mapsto\sum_{k=1}^{n}k\cdot\mathbb{I}\left[ x\in R_{k}\right]$ $$

and consider the conditional probability densities
$p_{X}(x\mid C=i)=P(X\in R_{i})^{-1}p_{X}(x)\cdot\mathbb{I}[x\in R_{i}]$. Since $F$ is an affine bijection on $R_{i}$,
the support of $p_{X}(\cdot|C=i)$, we can employ the change of variables formula and obtain that $p_{F(X)}(y\mid C=i)=P(X\in R_{i})^{-1}p_{X}(f_{i}^{-1}(y))\left|\det\frac{
\partial f_{i}^{-1}}{\partial y}\right|\cdot\mathbb{I}[F^{-1}(y)\in R_{i}]$. Finally, we obtain by the sum rule that

$$ $\displaystyle p_{F(X)}(y)$ $\displaystyle=\sum_{i=1}^{n}P(C=i)p_{F(X)}(y\mid C=i)$ $\displaystyle=\sum_{i=1}^{n}P_{X}(X\in R_{i})p_{F(X)}(y\mid C=i)$ $\displaystyle=\sum_{i=1}^{n}p_{X}(f_{i}^{-1}(y))\left|\det\frac{\partial f_{i} ^{-1}}{\partial y}\right|\cdot\mathbb{I}[F^{-1}(y)\in R_{i}]$ $\displaystyle\stackrel{{\scriptstyle\ast}}{{=}}\sum_{i=1}^{n}\left(\underbrace {\sum_{j=1}^{n}p_{X}(f_{i}^{-1}(y))\mathbb{I}[F^{-1}(y)\in R_{j}]}_{=p_{X}(F^{ -1}(y))}\right)\left|\det\frac{\partial f_{i}^{-1}}{\partial y}\right|\cdot \mathbb{I}[F^{-1}(y)\in R_{i}]$ $\displaystyle=p_{X}(F^{-1}(y))\sum_{i=1}^{n}\left|\det\frac{\partial f_{i}^{-1 }}{\partial y}\right|\cdot\mathbb{I}[F^{-1}(y)\in R_{i}]$ $\displaystyle=p_{X}(F^{-1}(y))\left|\det\frac{\partial F^{-1}}{\partial y} \right|,$ $$

where $(\ast)$ holds since
$\mathbb{I}[F^{-1}(y)\in R_{i}]\cdot\mathbb{I}[F^{-1}(y)\in R_{j}]=\delta_{ij}
\mathbb{I}[F^{-1}(y)\in R_{i}]$, where $\delta_{ij}=\begin{cases}1;i=j\\
0;\text{ else}\end{cases}$ is the Kronecker-Delta.∎

Next, we consider the choice of the base distribution.

[]
Let $p_{D}$ be defined by a piece-wise affine flow $F$ and a log-piece-wise affine base distribution $p_{B}$. Then $\log p_{D}$ is piece-wise affine.

###### Proof

As we have seen,

$$ $\displaystyle\log p_{D}(\mathbf{x})$ $\displaystyle=\log p_{B}(F(x))+\log\left|\textrm{det}\frac{\partial F}{ \partial x}\right|$ $$

Since $F$ and $\log p_{B}(\cdot)$ are piece-wise affine, $\log p_{B}(F(x))$ is also piece-wise affine. Similarly, $\left|\textrm{det}\frac{\partial F}{\partial x}\right|$ is piece-wise constant, which implies that $\log\left|\textrm{det}\frac{\partial F}{\partial x}\right|$ is piece-wise constant too. The claim follows immediately.∎

If restrict the flow model to further have a constant Jacobian determinant, then we obtain an even more intriguing way defining density level sets by the flow.
{prop}[]
If the determinant of the Jacobian of a flow $F$ on $\mathbb{R}^{d}$ is constant, then $F$ maps upper density level sets of the target distribution to upper density level sets of the base distribution.
Hence, if $B$ is a $p$-radial monotonic distribution over the domain of $F$, then there is a function $r:[0,1)\to\mathbb{R}_{+}$ such that $\textrm{UDL}_{F(B)}(q)=F(\mathbb{B}^{d}_{p}(r(q)))$.

###### Proof

This is a direct consequence of the change of variables formula.

$$ $\displaystyle F(\{x\mid\log p_{D}(x)>t\})$ $\displaystyle=$ $\displaystyle\{F(x)\mid\log p_{D}(x)>t\}$ $\displaystyle=$ $\displaystyle\left\{F(x)\mid\log p_{B}(F(x))>t-\underbrace{\log\left|\textrm{ det}\frac{\partial F}{\partial x}\right|}_{\text{const}}\right\}$ $\displaystyle=$ $\displaystyle\{y\mid\log p_{B}(y)>t^{\prime}\},$ $$

which is obviously an upper log-density level set w.r.t. the latent
distribution $B$. The last equation holds since $F$ is a bijection and $\log\left|\textrm{det}\frac{\partial F}{\partial x}\right|$ is constant. We combine the observation with the idea from 3 and conclude that for radial monotonic $B$ and $r(q)=\textrm{quantile}_{|B|_{p}}(q)$ the identity
$\textrm{UDL}_{F(B)}(q)=F\left(\mathbb{B}^{d}_{p}(r(q))\right)$ is indeed correct.∎

The latter proposition is especially attractive for abstract interpretation methods.
For a radial monotonic base distribution w.r.t. the $1$- or the $\infty$-norm, density level sets are definable by linear constraints.
They can therefore act as an initial
set that is propagated through the flow to obtain an approximation
of the upper density level set of the data distribution. As we can derive from Proposition 3, the function $r$ is simply the quantile function of the $p$-norm distribution of $B$. Hence, Proposition 3.1 yields an effective procedure. The approach is summarized in Figure 2. A major challenge in the application, however, will be the tightness of the approximation of the non-linearity. There is a delicate trade off to be made between tightness of approximation and complexity of the description. Interesting work in this direction has been done by Stanley Bak [].

Figure: Figure 2: Visualization of an abstract interpretation approach to in-distribution verification of a classifier using a flow model with constant Jacobian determinant and a $p$-radial monotonic base distribution. 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.

Interestingly, already the restrictions to piece-wise affine bijections leads us to classes of flows with a constant Jacobian determinant.
We provide an architectural survey in following section.

###### Proof

###### Proof

###### Proof

## 4 An Architectural Survey

We survey the literature to identify learnable components that satisfy our needs. Most prominently, additive conditioning layers, like additive coupling, turn out to yield exactly the networks that we envision. This encompasses the seminal NICE architecture [], additive auto-regressive layers [, , ], and masked additive convolutions [].

Additionally, bijective affine transformations represented by LU-decomposed affine layers (LUNets []) turn out to be equally well suitable. These layers also constitute a powerful replacement for the permutations or masks that are usually employed before a coupling-like layer. Although this addition turned out to be very beneficial, we note that the number of parameters scales quadratically with the dimension, which can be a performance bottleneck on high dimensional data.

### 4.1 Additive Transformations

As it turns out, additive transformations yield precisely the properties that we need in order to guarantee the good properties of the previous section.
The simplest such architecture is realized by so called additive coupling, which was first introduced for
the NICE architecture by Dinh et al. [].

### 4.2 Additive Coupling (NICE)

NICE belongs to the first flow architectures.
Nevertheless, it is a popular benchmark which has shown good performance on multiple data sets.

##### Additive Coupling Layers

A NICE flow is build from additive coupling layers. Each such layer $L$
consists of a partition $I_{1},I_{2}$ of $[D]$, where $D$ is the data dimension,
and a conditioning function $m:\mathbb{R}^{d}\rightarrow\mathbb{R}^{D-d}$,
where $d=|I_{1}|$. The layer $L$ maps $x$ to $y$ where

$$ $\displaystyle y_{I_{1}}$ $\displaystyle=$ $\displaystyle x_{I_{1}}$ $\displaystyle y_{I_{2}}$ $\displaystyle=$ $\displaystyle x_{I_{2}}+m(x_{I_{1}}).$ $$

It is easy to see that the Jacobean $\frac{\partial y}{\partial x}=\left(\begin{array}[]{cc}I_{d}&0\\
\frac{\partial y_{I_{2}}}{\partial x_{I_{1}}}&I_{D-d}\end{array}\right)$ is triangular and that all entries on the diagonal
are $1$. As the first $d$ components of the input remain unchanged, it is
usually necessary to employ multiple layers with varying partitions of the
input vector. It is straight forward to see that a coupling layer defines a piece-wise affine function if the conditioner $m$ is piece-wise affine.

##### Allowing Rescaling

As all additive coupling layers have Jacobean determinant $1$, the same will
hold for their composition. That means the space is never stretched or compressed through the transformation, which potentially limits the expressiveness. In order to account for this issue, NICE allows
for a final component-wise rescaling, i.e. multiplication with a matrix
$S$, where $S_{{ij}}\begin{cases}\neq 0&\text{if }i=j\\
=0&\text{else}\end{cases}$.

##### Computing log-Densities

Because of the simple additive coupling, computing log-densities is
particularly simple. Let $F$ be a NICE flow with base distribution $B$, layers
$L_{1},\ldots,L_{n}$, and scaling matrix S. Then

$$ $\displaystyle\log(p_{D}(\mathbf{x}))$ $\displaystyle=$ $\displaystyle\log\left(p_{B}(F(x))\left|\textrm{det}\frac{\partial F}{\partial x }\right|\right)$ $\displaystyle=$ $\displaystyle\log\left(p_{B}(F(x))\cdot\prod\left|\textrm{det}\frac{\partial L _{i}}{\partial x}\right|\cdot|\det S|\right)$ $\displaystyle=$ $\displaystyle\log p_{B}(F(x))+\underbrace{\sum\log\left|\textrm{det}\frac{ \partial L_{i}}{\partial x}\right|}_{=0}+\log|\det S|$ $\displaystyle=$ $\displaystyle\log p_{B}(F(x))+\sum\log S_{ii}$ $$

Computing $F^{-1}(z)$ has exactly the same complexity as computing a forward
pass $F(x)$. Because in order to invert the flow we only need to multiply
with the inverse scaling matrix and then pass the input to through the inverse
coupling layer in reverse order. Note that for an additive coupling layer $L=((I_{1},I_{2}),m)$ the inverse function can be implemented by $L^{-1}=((I_{1},I_{2}),-m)$.

#### 4.2.1 Masked Additive Coupling

It is also possible to rewrite the additive coupling equation in order to implement the NICE architecture as a fully connected neural network with masking and skip connections. An additive
coupling layer $\ell:\genfrac{(}{)}{0.0pt}{2}{x_{I_{1}}}{x_{I_{2}}}\mapsto\genfrac{(}{)}{0.0pt
}{2}{x_{I_{1}}}{x_{I_{2}}+c(x_{I_{1}})}$, whose conditioner is implemented by a neural network $c$ can equivalently be written as

$$ $\displaystyle\ell(x)=x+(1-\textrm{mask})\cdot c^{\prime}(\textrm{mask}\cdot x),$ (2) $$

where mask
is a $\{0,1\}$-vector with $\textrm{mask}_{i}=1\Leftrightarrow i\in I_{1}$ and the multiplication is computed component wise. Further, $c^{\prime}$ is a fully connected network obtained by adding dummy inputs for the components in $I_{2}$ and dummy outputs for the components of $I_{1}$ to $m$, which are effectively eliminated by the mask in Equation 2.

#### 4.2.2 Additive Auto-Regression

A general way to increase the expressiveness of the based flow models is the use of auto-regression instead of coupling [, , ]. In this case the conditioner is implemented as an RNN $c$, which couples the input component by component. More precisely, an additive auto-regressive flow layer $\ell$ computes a transformation $\ell(x)=y$ with

$$ $\displaystyle h_{1},z_{1}=0;\hskip 10.00002pt(h_{i+1},z_{i+1})=c(x_{i},h_{i})$ $\displaystyle y_{i}=x_{i}+z_{i}$ $$

Observe that the structure of the auto-regression still leads to a lower triangular shape of the Jacobean and the additive auto-regressive coupling ensures that all diagonal entries are $1$. With these properties one easily checks Proposition 3.1, 3.1 and 3.1 remain valid if additive coupling is replaced by additive auto-regression.

#### 4.2.3 Masked Additive Convolutions

The idea of masking was used in [] in order to transfer coupling to convolutional architectures where the input is a higher-order tensor. We can also employ this idea in our situation and still maintain the desired properties. In this case, Equation 2 is applied to a convolutional network, e.g. with a checker board and/or a channel-wise mask. As the reader readily verifies, the analogues of Proposition 3.1 - 3.1 hold also for this layer.

#### 4.2.4 LUNets

Recently, bijective fully-connected layers have been proposed in [] as LUNet. The idea is to ensure that that both, the affine transformation of a fully connected layer and the non-linearity are bijections. Bijectivity is ensured by representing the linear transform of the layer by an LU-factorization $A=LU$ with lower/upper triangular Matrices $L$ and $U$. Bijectivity is ensured by adding the constraints that the diagonal of $L$ contains only ones and diagonal of $U$ is always non-zero. In this case, Propositions 3.1 and 3.1 will still hold if we replace the layer architecture and use leaky ReLU instead of ReLU, but Proposition 3.1 will in general not hold anymore as the determinant of the layer Jacobean is not constant anymore.

LUNet is a very different approach to guaranteeing the bijectivity of the transformation compared to additive coupling. It has the advantage that the entire input can be transformed by a single layer.
The restriction that the affine transform needs to be bijective, however, fixes the capacity of the transformation to $d^{2}$ parameters where $d$ is the input dimension. This can be problematic, especially when working with high-dimensional data.

#### 4.2.5 Bijective Affine Layers

The bijective affine transform $T(x)=(LU)x+b$ at the heart of an LU-layer deserves special attention. Note that the determinant of the Jacobean is is constant for $T$. Since computing the inverse of an affine transform also has the complexity of computing the affine transform it follows that we can add bijective affine layers to the list of layers in Proposition 4.3 without loosing the validity of the statement. Bijective affine layers can be an interesting alternative to the intermediate permutation layers of the NICE architecture. Using an affine bijection instead of a simple fixed permutation of the dimensions allows the architecture to correlate the components of $I_{1}$ and $I_{2}$ in the subsequent coupling layer in a learnable fashion. As an example, consider the extreme case where all components of the target distribution are independent. In this case, the components $I_{1}$ and $I_{2}$ will be independent, no matter which permutation of the components we have applied beforehand. An affine bijection, however, can be capable of combining the variables in a way such that the components $I_{1}$ and $I_{2}$ become correlated.

### 4.3 The VeriFlow Architecture

We summarize the good properties of flows build from these layers in the following proposition, which also defines our proposed architecture.

[VeriFlow]
Let $F$ be a network that is purely build from the layer types (masked) additive coupling, additive autoregression, masked additive convolution, LU layers, component-wise scaling, and permutation of input dimensions. If the first three layer types only use piece-wise affine conditioning networks, then $F$ is a piece-wise affine flow with constant Jacobean determinant. In particular, any density $p_{D}$ defined by $F$ has the following properties:
(1) If $\log p_{B}(\cdot)$ is piece-wise affine, then $\log p_{D}$ is piece-wise affine.
(2) For any $p$-radial monotonic base distribution $B$ there is a function $r:[0,1)\to\mathbb{R}_{+}$ such that $\textrm{UDL}_{F(B)}(q)=F(\mathbb{B}^{d}_{p}(r(q)))$.
(3) Computing log-densities has the same computational complexity as sampling.

## 5 Experiments

The goal of our experiments is twofold.
Firstly, in Section 5.1, we show that the architecture of our flow model can be integrated with common verification frameworks for scalable verification and for obtaining more representative counterexamples when the neural network is unsafe.
Secondly, in Section 5.2.1 we show that combining LU-layers with additive coupling significantly improves over the baseline performance of the NICE architecture and that certain $1$-radial base distributions outperform their normalizing counterparts in the majority of benchmarks.

### 5.1 Verification

We train a flow model for each digit $i$ on rescaled MNIST ($\text{MNIST}^{10\times 10}_{i}$) and denote them by $g_{1},\ldots,g_{9}$.
Each flow model in our experiments has $3$ additive coupling layers with $100$ neurons and ReLu activation functions.
Furthermore, we train classifiers with varying depth $f_{\ell}$, where $\ell$ corresponds to the number of layers $1\leq\ell\leq 15$, with each layer consisting of a matrix multiplication, addition and ReLU activation, in the network.
We trained the networks with Adam-optimizer obtaining an accuracy score of around $90\%$ for all classifiers. We did not aim at making the classifiers particularly safe or unsafe w.r.t. the verification tasks at hand.
The final classification then corresponds to the respective digit with the highest score.

As verification tools, we use the Python interface of the C++ implemented verification framework Marabou 2 [] for deductive verification and ERAN, a pure Python implementation, for abstract interpretation [].
Since both verifiers only allow for one network to be parsed, we merge both networks together by piping the output of the flow model $g_{\tau}$ into the classifier $f_{\ell}$, resulting in one neural network that computes the composition $f_{\ell}\circ g_{\tau}:\mathbb{R}^{10\times 10}\rightarrow\mathbb{R}^{10}$.
We run all our verification-experiments environment on a Ubuntu 22.04 machine with an i7-1365U 1.80 GHz, 32 GB RAM and Intel Iris Xe Graphics.

#### 5.1.1 Verification within data distribution

In this section, we want to verify the (unsafe) MNIST classifier $f_{1}$. In particular, we want to show that the counterexamples obtained when leveraging our flow model for verifying the classifier is more representative of real-world inputs than the counterexamples obtained without leveraging a flow model.
As a toy property, we verify that $f_{\ell}$ always has a high confidence for all images that are classified as a specific digit $\tau$.
Counterexamples to this property contain images that are classified as $\tau$ but with a confidence lower than $\delta$. Such images are shown in Figure 3.

The top row of Figure 3 contains the precondition, assignment and postcondition that were used for the corresponding experiments.
The postcondition $\psi$ is the same for all experiments: given the output $\vec{y}$ of the neural network $f_{1}$, a digit $\tau$ and and arbitrary but fixed confidence threshold $\delta$ we want to verify whether the output of the classifier $\vec{y}\coloneqq f_{1}(x)$ satisfies the postcondition ${\psi(\vec{y})}$.
The confidence is defined as $\mathit{conf}(\vec{y},\tau)\coloneqq\nicefrac{{(|\vec{y}|\cdot\vec{y}[\tau]-
\sum_{j\neq\tau}\vec{y}[j]))}}{{|\vec{y}|}}$ with $|\vec{y}|$ denoting the number of elements in $\vec{y}$.

The results in Figures 3(a) and 3(b) mainly differ in the precondition $\phi$. In Figure 3(a) the precondition restricts the input to be any grayscale pixel image with resolution $10\times 10$. That image is then applied to the classifier $f_{1}$ to obtain the scores $\vec{y}$.
In Figure 3(b), on the other hand, the precondition restricts the input $\vec{x}$ to the UDL in the latent space. The threshold $t$ is determined such that $p_{D}(L^{\uparrow}_{D}(t_{p}))=p$ where $p=0.01$.
Applying the flow $g_{\tau}$ yields a top $1\%$ typical image which is then applied to the classifier $f_{1}$ to obtain the score $\vec{y}$.
In all experiments, the network does not satisfy the property and the images in Figure 3 correspond to the counterexamples provided by the solver.

As can be seen, the images on the left, which do not utilize a flow model, are noise and come from a region of the input space with high epistemic uncertainty.
This provides almost no insight to the weakness of the classifier when used in real world.
However, the images on the right, that do utilize a flow model, come from within the data distribution and provide a deeper insight to the classifier’s weakness as the images indeed resemble the digits $7$ and $8$.
As an alternative to using flow models, autoencoders also yield similar visual results [].
However, autoencoders lack probabilistic interpretability and fine-grained probabilistic control of the input-space, which are essential parts of our flow-model [].

Figure: (a) Counterexamples without flow model.
Refer to caption: extracted/5651567/digit_7_without_flow_in_dist.png

#### 5.1.2 Epistemic Uncertainty Verification

For the far tail of the data distribution there are usually no samples available.
Hence, any model trained purely from data has never gotten information about these areas (epistemic uncertainty).
In that context, we can verify that a classifier was trained with a vanishing inductive bias by moving away from the training data.
In this case the uncertainty estimates given by a classifier should converge towards a prior distribution, e.g., uniform, as we move further outwards in the tail [, ].
However, it is known that many deep neural network training methods produce badly calibrated networks with overconfident predictions, especially in areas of high epistemic
uncertainty [, ].
In that context, we want to verify that our classifier is not overconfident in the far tail of the data distribution.
More precisely, we leverage our flow model to restrict the input to the $9\%$ tail of the data distribution, trimming the last $1\%$ to avoid an unbounded input space and verify that the classifier has a low confidence for all atypical inputs.

Similar to the in-distribution verification task, we conduct four experiments to compare the counterexamples without and with leveraging a flow model for restricting the input space and and present them in Figure 4 along with the verification properties.

The left upper side of Figure 4 is the same as for the in-distribution verification task, except for the postcondition $\psi$, that now checks for the confidence to be low, if the image is classified as the digit $\tau$.
In the right upper side of Figure 4, the precondition $phi$ restricts the input space to the top one percent of most typical examples by first determining the threshold $t$ such that $p_{D}(L^{\uparrow}_{D}(t_{p}))=p$ where $p=0.01$ and setting the precondition $\phi\colon\{\vec{x}\in L^{\uparrow}_{D}(t)\}$.
The postcondition on the right side $\psi$ checks for the confidence to be low, if the image is classified as $\tau$.

The counterexamples on the left side of Figure 4, that do not utilize a flow model, are noise-images that do not resemble even atypical digits, despite being classified with high confidence.
The counterexamples on the right side of Figure 4, however, are atypical images of the digits that are classified with high confidence.
The latter is more useful for a user as it shows exactly the type of images where the classification itself is reasonable but the high confidence shows a wrong calibration of the neural network.

Figure: (a) Counterexamples without flow model
Refer to caption: extracted/5651567/0_conf_8_noflow.png

#### 5.1.3 Deductive Verification confidence threshold

One aspect that influences the quality of the counter examples of the verifier is the selected confidence threshold in the verification property.
More precisely, running an in-distribution verification task on the same UDL but with different confidence thresholds for the classifier may also return more atypical images as shown in Figure 5.
There, the UDL in the precondition is the same in every experiment, only the confidence threshold $\delta$ in the postcondition $argmax(y)=\tau\rightarrow\mathit{conf}(\vec{y},\tau)>\delta$ is assigned values increasing from $1$ to $15$ (with gaps in between).

Figure: Figure 5: Counterexamples for in-distribution verification tasks with increasing confidence thresholds in the postcondition.
Refer to caption: extracted/5651567/out.png

#### 5.1.4 Scalability

In this experiment, we assess the scalability of our flow model in the verification domain. To this end, we consider both the deductive verification tool Marabou 2 [] and the abstract interpretation tool ERAN [].
In order to assess the scalability reliably, we focus on verifying properties that are satisfied by the neural network. Otherwise, the deductive verifier could terminate early after finding a counterexample while barely touching the search space.
We verify for a classifier $f_{\ell}$ that for a subspace of the $1\%$ UDL, the network $f_{\ell}$ classifies the whole output space of the flow model $g_{0}$ restricted by the UDL as the digit 0 0.
We show this property only for a subspace of the UDL because the full UDL does not constitute a zonotope which is required when working on the deepzono domain [].
One could eliminate this problem by either choosing an $\infty$-radial base distribution for the flow or by using abstract interpretation algorithms that can handle more general initial sets.
However, we decided to live with this shortcoming for now, since first experiments indicated that both the above mentioned approaches bear additional challenges in terms of quality of the fit and efficiency, respectively, that we cannot fully address in this work.
For observing potential effects of the size of the neural network on the runtime, we conduct experiments with several classifiers varying in depth $f_{1},\ldots,f_{15}$ as indicated on the X-Axis of Figure 6(a) and repeat each experiment three times taking the median value. Note that the y-axes are discontinuous in Figure 6.

The results in Figure 6(a) indicate that the runtime of both tools is linear in the depth of the neural network. And even though Marabou is slower by a factor of up to $70$ compared to ERAN, both verifiers accomplish the verification tasks within seconds.
In a second experiment, we fix the neural network to $f_{1}$ and only increase the size of the input space.
We present the results of the second experiment in Figure 6(b).
Clearly, ERAN scales better than Marabou in both absolute values with a factor of around $50$ for the smallest tested input size as seen before, as well as in the overall trend when increasing the size of the input space to search in.
In particular, we can now also observe a strong non-linear increase in the runtime of Marabou, as it reaches the timeout limit of $200$ seconds for an input size that is proved by the abstract interpreter within $20$ milliseconds.
We conjecture that it is because Marabou also uses abstract interpretation methods as a preprocessing step for inferring bounds for each node in the network and use these bounds to simplifying or even trivialize the satisfiability problem. This, however, may no longer be feasible when the input space gets overly increased.
We conclude that both ERAN and Marabou scales well for deeper neural networks and ERAN also scales well for increased input sizes.

Figure: (a) Comparison increasing depth of the classifier
Refer to caption: extracted/5651567/marabou-eran-network-depth.png

### 5.2 Machine Learning

Besides the efficient applicability of our model in neuro-symbolic verification, our model needs to be versatile enough to capture the concepts of interest.
We show the effectiveness of our architecture as density estimator and generative model.

#### 5.2.1 Ablation Study

We perform several ablation studies to compare our choice of the base distribution against the most commonly used Gaussian distribution as well as our architecture against the original NICE architecture. Our most surprising finding is that $1$-radial base distributions are not only competitive but outperform their Normal counterparts in the vast majority of benchmarks. Overall, we observed that the training with an $1$-radial base distribution, especially a Laplacian, is more stable (note the bad performance and high standard deviations for some digits with the normal distribution in Figure 7 (left)).

As benchmarks, we mostly focus on tasks of moderate dimensionality and small sized networks since this scenario is approachable with the contemporary verification software on standard hardware. We pick up the example from the verification experiments and fit the models to each individual MNIST digit $i$ where the images are rescaled to $10\times 10$ pixels ($\text{MNIST}^{10\times 10}_{i}$) and we use three classic synthetic 2D datasets (circles, moons, blobs). All these experiments have been performed on a Macbook pro with M2 chip and 16GB of RAM. Additionally, we also scale our architecture to higher dimensions and more challenging datasets by performing a base distribution comparison on the full MNIST. Performance metric in all experiments is the negative log-likelihood (NLL). The scaled experiments have been performed on a DGX2 with 8 V100 GPUs. For all image datasets we used uniform dequantization and report the NLL of dequantized images.

Figure: Figure 7: (Left) Ablation study on $\text{MNIST}^{10\times 10}_{i}$. We fit our flow architecture with Normal and Laplacian base distributions and additive coupling layers, which are alternated either with random masking layers or with LU-layers. We perform a random hyperparameter optimization with $20$ samples for each configuration and report the average top-$3$ performance. The remaining experiment parametrization is fixed across all models and datasets. We use the average negative log-likelihood on the test set (lower is better) as performance measure. (Right) Negative log-likelihood (lower is better) of VeriFlow with varying base distribution on multiple benchmark datasets. The architecture is always based on alternating LU layers and additive coupling layers.The remaining experiment parametrization is fixed per dataset.
Refer to caption: extracted/5651567/mnist_digit_ablation.png

#### 5.2.2 Regularization and Advanced Training Methodology

Following the description given in [], we regularize the parameters of the LU layers. Without any form regularization, we observed exploding determinants on many tasks when working with LU layers.
Additionally, we adopt the technique of soft training []. During training, We sample a noise scale $\sigma$ from a prior distribution $P$ for each training sample and perturb the sample with noise sampled from from the base distribution (Gaussian or Laplacian) with covariance $\sigma I$. For the noise scale prior we use a Laplacian with small standard deviation. We fit a conditional flow on the perturbed data where the conditioning variable is the noise scale $\sigma$. During inference with unperturbed data, the noise scale is set to 0 0. We observed significant improvements through soft training, in terms of test likelihoods but also in terms of subjective visual quality as evaluated by the authors.

#### 5.2.3 Calibration of Density Level Sets

A major challenge that we faced when conducting verification experiments was the calibration of the density level sets. When testing for satisfiability within a given density level set, we turn the distribution of interest into an uncertainty set in the latent space without preference for more likely examples. Current solvers tend to produce counter examples from extreme points within the uncertainty set. Since the geometry of the space often enforces that little probability is centered around these areas, we found that sampling from such point in the latent space often produces OOD data, even when considering a set that is supposed to represent the top e.g. one percent of most typical examples. Following this intuition, it seems that the properties of distributions like the Laplacian and Gaussian distribution in high dimensions lead to particularly unfavorable results for our purposes. Indeed, in high dimensional spaces, the corresponding $p$-norm distributions are strongly concentrated around the relatively large values of $d$ and $\sqrt{d}$, respectively.

Figure: Figure 8: Quantiles of the $p$-norm distributions for $d$-dimensional Gaussian, Laplacian, and a custom $1$-radial distribution. While the $\infty$-norm is always relatively low, the $p$-Norm of the $p$ radial distributions Laplacian and Gaussian are relatively large. That means that even on very high density contours, there are points on contour (e.g. $\alpha e_{i}$ for a standard basis vector $e_{i}$ and suitably chosen $\alpha$) that are very far away from the data that is seen during training (assuming that the empirical latent distribution approximately follows that base distribution relatively soon during training). Hence, it is not surprising that sampling from such areas in the latent space is likely to produce poor quality samples. The custom radial distribution mitigates this effect by keeping the $p$-norm distribution constant without dependency on the dimension.
Refer to caption: extracted/5651567/high_dim_norm_quantiles.png

Therefore, we conjecture that more concentrated base distributions help to mitigate this issue to some extend, see Figure 8 for an intuition. In order to avoid that the infinity norm of vectors becomes to small by concentrating the probability mass closer to the origin, we choose a unimodal radius distribution where the density converges to 0 0 when approaching both, 0 0 and $\infty$. Among our initial trials with multiple such distributions, like e.g. scaled Normal and Laplacian or distributions based on EVT norm distributions, a log-normal distribution with $\mu=1.0$ and $\sigma=0.5$ has shown most promising results. A qualitative and quantitative comparison with the Laplace base distribution is shown in the figures 10 – 11. We remark here that, strictly speaking, the resulting distribution is not radial monotonic. However, in high dimension it holds that the corresponding function $g$ with $g(|x|_{1})=p(x)$ is unimodal with it’s mode extremely close to 0 0. In an SMT setting, it would not be very hard to correct the formulas and exclude the small $L^{p}$ ball that does not belong to the density level set, but in our experiments with a dimensionality of $100$, the additionally included area is so vanishingly small, both in probability and in volume, that we decided ignore this issue here. Based on our initial experience with more exotic radial distributions, we believe that a thorough investigation of this class of distributions is potentially interesting also in other application areas such as anomaly detection. More generally, the calibration of density level sets remains a challenge that we think has gotten too little attention in past. Therefore, we stress the need for more systematic research in that area.

Figure: Figure 9: Laplace base distribution
Refer to caption: extracted/5651567/model_laplace_udls.png

Figure: Figure 11: $QQ$-plot of the empirical latent $1$-norm distribution under the flow, $p_{\left|F^{-1}(X)\right|_{1}}$, against the theoretical $1$-norm distribution induced by the base distribution. With both base distributions, the model struggles to match the empirical with the optimal latent $1$-norm distribution in the low quantiles (although in opposite directions). However, with the log-normal distribution, the $QQ$-plot indicates approximately proportional tail behavior, while the empirical distribution is too wide in both directions with a Laplacian base distribution
Refer to caption: extracted/5651567/latent_radial_qq_logN_laplace.png

#### 5.2.4 Sample Quality and Additional Benchmarks

Figure 12 shows random samples from the MNIST digit ablation study. Additionally, we also tested our architecture on the FashionMNIST dataset. Results are depicted in table 1

Figure: Figure 12: Random samples from the ablation study on the MNIST digits. The $i$th column shows samples of the flow architectures trained on $\text{MNIST}^{10\times 10}_{i}$. Each row shows a different architecture (Top to bottom: $\text{MNIST}^{10\times 10}_{i}$ ground truth, LU $+$ Laplace distribution, LU $+$ Normal distribution, Random mask $+$ Laplace distribution, Random mask $+$ Normal distribution).
Refer to caption: extracted/5651567/digit_ablation.png

**Table 1: Additional Benchmarks comparing VeriFlow with various base distributions. For each trial, a model with 10 alternations of LU- and additive coupling layers has been trained. Each coupling layers consists of a conditioner with 3 hidden layers. Each layer consists of 300 neurons. The same setup was used for the MNIST benchmark.**
| Benchmark |  |  |
| --- | --- | --- |
| Dataset | Base Distribution | NLL |
| FashionMNIST | Normal | $-1264.539$ |
|  | Laplace | $-1341.916$ |
|  | $\mathbf{R}_{\textbf{logN(1, .5),1.784}}$ | $\mathbf{-1386.659}$ |

## 6 Related Work

In the verification domain, our paper is conceptually in-line with the recently introduced Neuro-Symbolic verification framework by Xie et al. [].
They propose verifying high-level semantics of neural network by using other specialized networks for capturing the semantics in the specification.
In our case, the specialized network is our flow model that we use for verifying another neural network, for example an MNIST-classifier.

Similar to our concern of designing a flow model such that it can be verified using existing verification infrastructure, there are recent works on automated preprocessing of neural network via pruning [] or via regularization techniques [, ] for the same goal, namely making them more suitable for verification with state-of-the-art verifiers.

Flow models are on the forefront of modern density estimation techniques and have received significant attention over the last decade []. A constant Jacobian determinant is usually observed at the time of the introduction of the respective layer in the context of the likelihood computation [, , , , ], although typically without further investigation of the induced properties. The role of the Jacobian determinant in general has been investigated in the context of the exploding determinant phenomenon [, , ]. There is also a notable application of flow architectures with constant Jacobian determinant for anomaly detection. OneFlow uses a constant Jacobian determinant to compute and minimize the volume the image of a unit hyper sphere around the origin in the latent space, drawing a connection between flows and deep one-class SVMs [].

## 7 Further Directions

We summarize the research and engineering challenges that we belief to be important for the advancement of the field:
(1) Verification tools need to provide more complete support for the capabilities of deep learning frameworks such as torch, including support for scenarios that involve more than one network.
(2) Theoretical and practical understanding of the expressivity of piece-wise affine uniformly scaling flows. To the best of our knowledge there is no known universal approximation theorem that applies to our architectures [, , , , ].
(3) Well calibrated density level sets are crucial for interpretable verification results. Improving the consistency of density level sets of deep learning models is an important challenge.

## 8 Acknowledgements

This work has been financially supported by Deutsche Forschungsgemeinschaft, DFG Project number 459419731, and the Research Center Trustworthy Data Science and Security ([https://rc-trust.ai](https://rc-trust.ai)), one of the Research Alliance centers within the UA Ruhr ([https://uaruhr.de](https://uaruhr.de)).

## Peer Reviews

confidence: 3
contribution: 4
initial_rating: 8
presentation: 4
questions: How does the flow-based approach compare with the VAE-based approach for modeling a given distribution [1]? 

[1] https://arxiv.org/pdf/2007.08450
soundness: 3
strengths: - This paper proposes a generic neuro-symbolic approach to limit the input space to a given data distribution. The specification considered here is novel and of practical interest. 
- The paper designs a novel flow model that allows the definition of the pre-image of a density level set in the latent space via linear
constraints, making the model both interpretable and compatible with existing neural network verifiers.
- The paper instantiates the proposed verification method with two verifiers, one based on bound propagation, the other based on search, and illustrates the trade-off in performance and functionality.
summary: This paper introduces a methodology to verify semantically meaning properties using a neuro-symbolic approach, in which the input to the neural network under verification is specified by a flow model trained to model a particular data distribution. The paper shows that the proposed method can be used to generate in-distribution counter-examples that violate a specified output property.
weaknesses: - The paper only considers relatively small datasets. Validating the approach on common benchmark sets considered in VNN literature such as CIFAR-10 and ACAS-Xu would better illustrate the scalability of the approach. 
- The soundness of the verification depends on the quality of the trained flow model. This is an intrinsic issue of neuro-symbolic approaches like this, but I do acknowledge that I cannot see an alternative approach to verify the specifications considered in the paper.

---

confidence: 4
contribution: 2
initial_rating: 3
presentation: 1
questions: Refer to the Weaknesses section
soundness: 2
strengths: **Strengths**

- In theory, I think coming up with sensible specifications for Neural Networks is an important problem. Unfortunately, there does not seem to be enough work in this direction.

- Using normalizing flows seems to be a reasonable choice for encoding input specification.
summary: **Outline**

The authors propose VeriFlow a normalizing flow-based method to learn more realistic input specifications for Deep Neural Network (DNN) verification which can capture more diverse inputs than existing local $L_{p}$ norm-based robustness specification while excluding noisy meaningless inputs included in global input specifications. The authors show with the help of the proposed method they can generate more sensible counter-examples that violate the property under verification.
weaknesses: **Questions and weaknesses**

I had a really hard time understanding the paper. The organization and notations and definition used in the paper are not mentioned beforehand.

**Motivation of the work**\
Q1. (Lines 52 - 53) “Local properties, on the other hand, suffer from the same problem as statistical testing, i.e., they rely on a high-quality data set that the verification property is based on.” - I completely agree with this statement. However, even networks trained with certifiably robust methods on datasets like CIFAR-10 and Tiny ImageNet [1] (excluding MNIST) still have quite low verified accuracy (percentage of verified local properties), even for small epsilon values like $\epsilon = 8/255$. Given that networks struggle to achieve robustness on this relatively "high-quality data," as the authors noted, what is the reasoning for moving to more challenging input specifications?

**Doubts regarding Proposition 2** 

Q1. I find proposition 2 hard to understand possibly due to the error/ambiguity notations and undefined terms. I list my concerns below \
a. What are affine regions $R_{1},\dots, R_{n}$? \
b. Affine regions and their relation with $F: \mathbb{R}^{n} \to \mathbb{R}^{n}$ are not defined formally. \
c. Why is the number of affine regions $R_{1},\dots, R_{n}$ the same as the input dimension of F? In the worst case, what is the number of affine regions? Is it exponential w.r.t number of activations? \
d. What is $d$ in $\mathbb{R}^{d}$ ?

Q2. Also, piecewise affine functions are not differentiable (like $ y = ReLU\(x\) $ is not differentiable ). Can you give an example of how proposition 2 holds for this case i.e. $y = ReLU(x)$?
 

**Usefulness**

Q1. I am doubtful about the usefulness of the proposed method and seems only experiments are with downsized (10x10) MNIST datasets. Can authors provide any insights into how the proposed method can generate preconditions to other scenarios MNIST (28x28), CIFAR10 (3x32x32), etc.?  It is well known that SMT-based solvers and verification w.r.t. global properties do not work with high-dimensional data, does that mean the proposed can only work for low-dimensional inputs?


**Representation & writing**

Q1. The authors should have clarified which specification the provided counterexample was violating. Let me assume it was a global property. If so, does not this counterexample substantiate why most well-known works [2, 3] focus on local properties? When violations occur, at least local properties tend to produce more sensible, human-understandable images.

Q2. (Lines ) “One well-studied example for a local property is adversarial robustness which requires the neural network to classify any point from the data set as the same class as any minor perturbation of that point.” - Correct me if I am wrong but I don’t think this is an accurate definition. Suppose an image of a 5, along with all its minor perturbations, gets classified as a 6. In this case, the predicted class remains consistent, but all labels are incorrect. Typically, in adversarial robustness, this scenario is considered a violation of the output specification. According to the authors’ definition, however, it would not be regarded as a violation.

Q3. The presentation of the paper could be clearer. Specifically in Section 3, I am unsure which contributions are original to this paper and which pre-exist in the normalizing flows literature. 

[1] “Connecting Certified and Adversarial Training”, NeurIPS, 2023.
[2] “General Cutting Planes for Bound-Propagation-Based Neural Network Verification”, NeurIPS, 2022.
[3] “Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound”, ICLR, 2022.


**Related work is obsolete** 

The works cited in this paper are outdated and have been surpassed by more recent research. I strongly recommend that the authors include references to papers from leading ML conferences (such as ICML, NeurIPS, and ICLR) and top programming languages/verification venues (such as POPL, PLDI, and CAV) from the past 3-4 years. For example,

**Abstract Domain:** The Zonotope abstract domain has been surpassed by the DeepPoly domain [1]. Subsequently, multi-neuron abstraction was introduced in [2], and more recently, the DiffPoly domain [3] was proposed for hyperproperty verification.

**Branch & Bound-Based Verifiers:** Current state-of-the-art verifiers for local properties, such as GCP-CROWN [4] and MN-BaB [5], are not mentioned.

**Input Specification:** Unlike this work, many existing studies consider weaker local specifications to model practical attack scenarios, such as robustness against geometric perturbations [1, 6] and robustness against universal adversarial perturbations (UAP) [3, 7, 8]. This work should mention these studies and justify its approach of addressing more challenging input specifications.

[1] “An Abstract Domain for Certifying Neural Networks”, POPL, 2019.\
[2] “PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations”, POPL, 2022.\
[3] “Input-Relational Verification of Deep Neural Networks”, PLDI, 2024.\
[4] “General Cutting Planes for Bound-Propagation-Based Neural Network Verification”, NeurIPS, 2022.\
[5] “Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound”, ICLR, 2022.\
[6] “Certifying Geometric Robustness of Neural Networks”, NeurIPS, 2019.\
[7] “Towards Robustness Certification Against Universal Perturbations”, ICLR, 2023.\
[8] “Relational DNN Verification With Cross Executional Bound Refinement”, ICML, 2024.

---

confidence: 4
contribution: 4
initial_rating: 6
presentation: 2
questions: 1. In Definition 2, X is a called $k$-radially distributed. However, there is no assumption on $k$. Where does $k$ come from? 

2. It is wired to have only one subsection Section 3.1 inside Section 3. Besides, why do you consider only the types of the first three types in F? In which principle one can decide the types for the first three layers and other remainder layers for different distributions? 

3. In the paper, it is not clear how the flow model is trained and how the quality of trained flow models affect the verification results. Can you provide more details regarding the the issues?
soundness: 4
strengths: 1. A novel perspective to neural network verification. Most of the existing approaches try to define tightest-possible over-approximation for DNNs to be verified to reduce over-estimation and false positives in formal verification results. This paper considers the verification from a new perspective by restricting verification approaches to meaningful input space. In literature, there are several attempts to the formal verifications of semantic perturbations such as rotations, occlusions, and geometric transformations. This paper considers the semantic perturbations from the distribution perspective. This imposes a new verification problem that is different from existing formal verification problems of DNNs. The work would inspire more solutions to the new problem. 

2. The proposed flow-based method is technically sound and practically useful. Transforming original input space into UDL sets by piecewise affine and abstracting the sets using effectively computable abstract domains are intuitively applicable and straightforward, However, the difficulty lies in finding appropriate flow models and abstractions. The authors identifies the conditions and theoretically prove the qualification of identified flow models to the verification task. 


3. The evaluations are comprehensive and the results are convincing. The results show that the counterexamples computed in the proposed way are indeed more interpretable, while it is compatible with mainstream verification approaches such as SMT-based or abstraction-based ones. The overhead caused by flow models can be ignored. The verification efficiency is mainly depended on the backend DNN verification approaches. However, this is applicable only to low-dimensioned cases.
summary: This paper proposes a novel approach to modeling input distributions for the purpose of formal verification of neural networks. In particular, the authors leverage flow models to transform input space into upper density level sets, by which existing formal verification approaches for deep neural networks are restricted to search in those data distributions of interest. In this way, one can find more meaningful counterexamples that have practical meaning or are computable under certain perturbation approaches. The authors identify two main properties that shall be satisfied by flow models suited to formal verifications. One is that the transformation by flow models must be peicewise affine. The other is that UDL sets takes the shape of L^p-ball in the latent space. Based on the two properties, the authors further analyze several existing flow models that meet the requirements and demonstrate the effectiveness when being applied to the verification of DNNs with SOTA tools such as ERAN and Marabou 2.0. The authors evaluate their proposed approach and demonstrate the effectiveness in finding more meaningful counterexamples (or adversarial examples) and the scalability to different types of verification approaches.
weaknesses: 1. The presentation shall be carefully proofread if the paper is finally accepted. There are a lot of grammatical errors that could be completely avoided. For instance, on Line 212, the sentence let XXX is the hyper volume, and on Line 480 complext problems should be complex problems. I just name a few of them. The paper seems to be written in haste. That makes me lower my score. 

2. The experiment part should provide more evidences about meaningful counterexamples generated by the proposed approach. As motivated by finding more meaning counterexamples from neural network verification, the authors should give more evidences. They shall not be placed in appendix. 

3. Section 2 (verification background) seems not necessary. The propose modeling methods are not closely related to backend verification approaches. Having section 2 or not will not affect the understanding of the paper. It provides few useful information to help readers understand the paper.

---

confidence: 3
contribution: 3
initial_rating: 3
presentation: 2
questions: - I want to know more about the enclosed set in the data space: How restrictive is the subset of the entire domain? For example, the network g_8 aims to only output images with an 8 displayed. However, are there 8s (from the training set) that cannot be constructed? Are a certain % of the 8s from the training set included in the exact / outer-approximative set in the data space if the input set in the latent space matches the same % threshold q?
- How would you address the limitation of the continuous connected set assumption on the data of each class?
- Regarding scalability of NN verifiers: Marabou regularly participates in VNN-COMP where much larger networks and also arbitrary computation graphs are considered. What specifically (e.g., types of layers) limits the scalability of your approach here? Line 390 also says that the verificaiton was done within a few seconds, which does not sound like a huge limitation.
- Many verifiers can also efficiently handle other activation functions than ReLU. Why is this limitation necessary?
soundness: 3
strengths: - Providing meaningful counterexamples is highly relevant in the safety domain, which is not necessarily the case if they are generated form the entire input domain.
- The underlying transformations are piece-wise linear and the input set in the latent space corresponds to an L_p-ball, such that existing NN verifiers can be used to formally show the (non-)existance of counterexamples.
- The quality of the counterexamples can be selected by choosing a confidence level of the underlying distribution (e.g., clearly visible in Appendix C.3).
- Modelling the approach with distributions that go beyond naive ones and perform rigorous theoretical analysis on them.
summary: The paper introduces a novel framework to extract meaningful counterexamples that a neural network missclassifies called VeriFlow.
This is realized by restricting the global input domain only to images that probabilistically match the actual data distribution via transforming an assumed base distribution from a latent space to the data space. 
The (non-)existance of counterexamples is then formally verified with existing NN verifier (Marabou/ERAN) on the generated data spaces,
where the input set for the verification query is determined by the desired confidence level on the base distribution.
The experiments show promising results and provide qualitative counterexamples.
weaknesses: Major points:

One common limitation of probabilistic approaches is that they assume a certain distribution and (in this case) transform this distribution via learning (!) to obtain desired properties (in this case, that it models the actual distribution of the data, e.g., outputs the set of "8" figures). However, if the learned (transformed) distribution in the data space actually matches the training set distribution is not adequately shown/tested.
For example, it is not said how long this has to be trained for until this property is reached (e.g., the loss is modeled in a way such that it becomes 0 once all desired properties are (formally) fulfilled). If this cannot be done, one could at least test it empirically: E.g., line 358 states that choosing a certain threshold obtains us top 1% typical images. Thus, as the paper can enclose the respective set in the data space, one could test if 1% of the training data is contained in that set and qualitatively assess if these could be classified as "typical". Doing so for different thresholds and classes would greatly strengthen that claim. If one cannot support the claim of modeling the actual data distribution in any way, there are no probabilistic guarantees even though distributions are used and I would rather categorize it as a heuristic.

The related work section does not adequately place this paper in the broader context of literature. Additionally, I found that both Sec. 2 and Sec. 5 contain stuff that are usually found in related work section and limitations/future work mentioned in Sec. 5 should be stated more clearly in a different section, e.g., Sec. 6. I propose to rework these sections: For example, a new Sec. 2 could give more background information on modeling distributions to get a better understanding of the subsequent Sec. 3. 
The new related work section should place this work into the broader context: 
- There are many more verifiers than presented in the paper. A good starting point for that literature research would be the verifiers of VNN-COMP. Also, not all optimization-based approaches are complete (i.e., either verify or provide a counterexample) but can also be incomplete and sound (i.e., if they say the property holds, it actually holds but there might be cases where they just return unknown without providing a counterexample; as is described for abstract interpretation). I think it would be better to state this, cite a broader range of NN verifiers, but you can be less detailed as currently in Sec. 2 as this is not the main focus of the paper.
- Sec. 5 also mentions "preprocessing steps" to ease verification. One should also mention adversarial training methods that incorporate NN verification into the training process, e.g.
[1] Gowal, et al., “Scalable verified training for provably robust image classification,” 2019.
[4] Zhang et al., “Theoretically principled trade-off between robustness and accuracy,” 2019.
[3] Muller, et al., “Certified training: ¨ Small boxes are all you need,” 2023.
[4] Koller et al., “End-to-end set-based training for neural network verification, 2024

Merging these sections as suggested might also leave more space for explaining the theoretical background in a new Sec. 2 on the required distributions, transformations, and terms like "constant Jacobian determinant" for the sake of self-containment. E.g. line 246 says that the constant Jacobian determinant is demanded, but it is not said how this is done.
Some propositions are also missing proofs (e.g., Prop. 1). If they are known results, they could be moved to the new Sec. 2 and cited adequately.

Minor points:
- The paper states that counterexamples generated from the global domain result in noisy, synthetic data that do not necessarily correspond to actual images. However, it is often not difficult to find counterexamples in the local neighborhood of images, which are still meaningful.
- Line 325 states that one has to learn a different transformation for each class. This could be stated more clearly.
- As the input set in the latent space corresponds to an L_p ball (a continuous connected set) and the applied transformations are continuous (piece-wise linear), also the set in the data space is continuous and connected. Thus, we implicitly assume that all our data corresponding to one class live in one connected space. This limitation should be better addressed by saying in which applications this assumption holds.
- Line 195: P_D not introduced, only probability density function p_D. Is it the respective CDF?
- Lack of intuition why a certain base distribution is chosen other than "it turned out that it boosted the performance"
- More detailed steps / motivation / intuition in Sec. 3 to make it easier for the reader to follow along. For example, one could (re-)state the desired properties of the architecture in Sec. 3.1 before saying how the components are constructed to better motivate why they are constructed like that.
- Introduce variables before they are used: e.g., line 349: What is y? Is it scores as introduced in line 356? But there, y is written in bold font and not in regular font as in line 349.
- Line 391: Which "input space" is increased? The dimension of the latent space? If not, how large is the latent space?
- Spelling/Grammar mistakes: Line 198: "Gaussian is ~the~ by far"


Other points that did not directly influence the score
- Rectified Linear Units are commonly abbreviated by ReLU, not ReLu.
- Clean figures (especially in appendix): You used titles of each image to display information. However, if something relates to an entire row / column, it's usually easier to read if you only write it as ylabel of the respective left most image / title of respective top image, respectively.

Meta-review: The submission proposes the VeriFlow architecture as a flow based density model tailored to allow any verification approach to restrict its search to the some data distribution of interest.

+ The topic is of interest as more meaningful specifications are important to showcase the usefulness of verification.
+ The proposed methodology appears to be technically sound.

- The paper is difficult to follow and requires a rewrite to improve its clarity.
- It is not clear how well the learned transformation represents the actual data distribution.

Decision: Reject