Verifying Global Neural Network Specifications using Hyperproperties
Current approaches to neural network verification focus on specifications
that target small regions around known input data points, such as local
robustness. Thus, using these approaches, we can not obtain guarantees for
inputs that are not close to known inputs. Yet, it is highly likely that a
neural network will encounter such truly unseen inputs during its application.
We study global specifications that - when satisfied - provide guarantees for
all potential inputs. We introduce a hyperproperty formalism that allows for
expressing global specifications such as monotonicity, Lipschitz continuity,
global robustness, and dependency fairness. Our formalism enables verifying
global specifications using existing neural network verification approaches by
leveraging capabilities for verifying general computational graphs. Thereby, we
extend the scope of guarantees that can be provided using existing methods.
Recent success in verifying specific global specifications shows that attaining
strong guarantees for all potential data points is feasible.
David Boetius, Stefan Leue
# Verifying Global Neural Network Specifications using Hyperproperties

###### Abstract

Current approaches to neural network verification focus on specifications that target small regions around known input data points, such as local robustness. Thus, using these approaches, we can not obtain guarantees for inputs that are not close to known inputs. Yet, it is highly likely that a neural network will encounter such truly unseen inputs during its application. We study global specifications that -- when satisfied -- provide guarantees for all potential inputs. We introduce a hyperproperty formalism that allows for expressing global specifications such as monotonicity, Lipschitz continuity, global robustness, and dependency fairness. Our formalism enables verifying global specifications using existing neural network verification approaches by leveraging capabilities for verifying general computational graphs. Thereby, we extend the scope of guarantees that can be provided using existing methods. Recent success in verifying specific global specifications shows that attaining strong guarantees for all potential data points is feasible.

Keywords:Neural Network Verification Safe Deep Learning Hyperproperties General Computational Graphs.

## 1 Introduction

Deep learning is a game changer for research, education, business and beyond [9, 11]. Yet, we remain unable to provide strong guarantees on the behaviour of neural networks. In particular, while neural network verification in principle can provide strong guarantees, current approaches almost exclusively consider _local_ specifications [1, 14, 20, 25, 32, 38] that only apply to small regions around known input data points. This means that the currently widely-used specifications only sparsely cover the input space, providing no guarantees for inputs that are not close to known inputs. In contrast, _global_ specifications cover the entire input space.

We propose a specification formalism for neural networks that encompasses a rich class of global specifications while enabling verification using existing verifier technology. In particular, we show how monotonicity, Lipschitz continuity, two notions of global robustness [21, 24], and dependency fairness [15, 35] can be expressed using our formalism.

As noted in [30], global specifications such as monotonicity and global robustness are hyperproperties [8]. In difference to regular properties that only
consider one network execution at a time, hyperproperties relate executions for several inputs of the same neural network to each other. This allows us, for example, to express a naive notion of global robustness stating that an arbitrary input and a second input that lies close need to receive the same classification.

A central aspect of our formalism is that we use auxiliary neural networks to define input sets and output sets. By leveraging capabilities for verifying general computational graphs [37], the auxiliary networks, together with _self-composition_[8], allow for verifying hyperproperties using existing neural network verification approaches. Here, the role of the auxiliary neural networks is to make complex hyperproperty input and output sets accessible to existing verification approaches. Concretely, we design an auxiliary neural network to generate the tuples of inputs that need to be compared to determine whether a hyperproperty is satisfied. Another auxiliary neural network detects whether the outputs a network produces for these inputs satisfy the output constraint. For the naive notion of global robustness, this means that we derive a neural network that generates arbitrary pairs of inputs that are close to each other and another neural network that detects whether two outputs represent the same classification. Importantly, these auxiliary neural networks _exactly_ capture the targeted input and output constraints using standard neural network components.

Recent success in verifying global robustness [36] and global individual fairness [35] demonstrates that verifying global specifications is feasible. Our formalism is a general framework for global specifications targeting existing verifiers [14, 22, 32, 38]. While our formalism does not alleviate the need for specialised techniques, such as the Interleaving Twin Encoding [36], it allows for

1. Comparing general-purpose verifiers with specialised verifiers for specific global specifications and
2. Applying general-purpose verifiers to global specifications for which no specialised verifier exists.

## 2 Preliminaries

We consider verifying whether a neural network conforms to a global specification. Neural networks are computational graphs [16]. Global specifications are formalised using hyperproperties [8, 30].

Definition 1 (Computational Graph): A _computational graph_ is a directed acyclic graph with computations \((V,E,h)\), where \(V=\{1,\ldots,L\}\) with \(L\in\mathbb{N}\) is the set of nodes, \(E\subseteq V\times V\) is the edge relation and \(h=(h_{1},\ldots,h_{L})\) is the computations tuple. Let \(\mathrm{degin}:V\rightarrow\mathbb{N}\) denote the in-degree. The computation of node \(i\in V\) is \(h_{i}:\mathbb{R}^{m_{k_{1}}}\times\cdots\times\mathbb{R}^{m_{k_{\mathrm{degin}( i)}}}\rightarrow\mathbb{R}^{m_{i}}\), where \(m_{i}\in\mathbb{N}\) is the output dimension of node \(i\) and \(k_{1},\ldots,k_{\mathrm{degin}(i)}\in\{i\mid(k,i)\in E\}\) with \(k_{1}\leq\cdots\leq k_{\mathrm{degin}(i)}\) are the direct predecessors of \(i\).

Definition 2 (Neural Network): A _neural network \(\mathrm{net}_{\boldsymbol{\theta}}:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}\)_, \(n,m\in\mathbb{N}\) is a composition of affine transformations and non-affine activation functions
represented by a computational graph \((V,E,h)\) with a source \(i\) and a single sink \(j\), such that \(h_{i}:\{\emptyset\}\to\mathbb{R}^{n}\) and \(h_{j}:\mathbb{R}^{m_{k_{1}}}\times\cdots\times\mathbb{R}^{m_{k_{\mathrm{design} (j)}}}\to\mathbb{R}^{m}\). The source \(i\) is the _input_ of \(\mathrm{net}_{\boldsymbol{\theta}}\). The remaining sources of the computational graph together form the _parameters_\(\boldsymbol{\theta}\) of \(\mathrm{net}_{\boldsymbol{\theta}}\). The sink \(j\) is the _output_ of \(\mathrm{net}_{\boldsymbol{\theta}}\). For classification tasks, \(\arg\max_{j=1}^{m}\mathrm{net}_{\boldsymbol{\theta}}(\boldsymbol{x})\) is the class \(\mathrm{net}_{\boldsymbol{\theta}}\) assigns to an input \(\boldsymbol{x}\in\mathbb{R}^{n}\)._

Figure 1 contains the computational graph of a residual unit [19] as an example. This graph defines the steps necessary for computing the output of a residual unit, given an input. It also allows for computing gradients and verifying a residual unit. Assume we want to compute the outputs of a neural network for an input \(\boldsymbol{x}\in\mathbb{R}^{n}\). Also, assume we have a parameter assignment \(\boldsymbol{\theta}\). We assign \(\boldsymbol{x}\) to the network input node \(i\) and the corresponding parameter values to the remaining sources. Now, computing the outputs corresponds to a forward walk over the computational graph, propagating the computation results of each node to its direct successors. Similarly, a backwards walk from sinks to sources allows for computing the gradients of the sink with respect to each source (backpropagation). Forward and backwards walks also allow for computing certified lower and upper bounds on the network output that can be used for verifying the neural network [37].

Verifying a neural network means that we want to automatically prove or disprove whether the neural network satisfies a _specification_. A specification is a set of properties.

Definition 3 (Property): A _property_\(\varphi=(\mathcal{X}_{\varphi},\mathcal{Y}_{\varphi})\) is a tuple of an _input set_\(\mathcal{X}_{\varphi}\subseteq\mathbb{R}^{n}\) and an _output set_\(\mathcal{Y}_{\varphi}\subseteq\mathbb{R}^{m}\), \(n,m\in\mathbb{N}\). We write \(\mathrm{net}_{\boldsymbol{\theta}}\vDash\varphi\) when a neural network \(\mathrm{net}_{\boldsymbol{\theta}}:\mathbb{R}^{n}\to\mathbb{R}^{m}\)_satisfies the property \(\varphi\). Specifically,

\[\mathrm{net}_{\boldsymbol{\theta}}\vDash\varphi\Leftrightarrow\forall \boldsymbol{x}\in\mathcal{X}_{\varphi}:\mathrm{net}_{\boldsymbol{\theta}}( \boldsymbol{x})\in\mathcal{Y}_{\varphi}.\]

We call an input \(\boldsymbol{x}\in\mathcal{X}_{\varphi}\) for which \(\mathrm{net}_{\boldsymbol{\theta}}(\boldsymbol{x})\notin\mathcal{Y}_{\varphi}\) a _counterexample.

A verifier determines whether a neural network \(\mathrm{net}_{\boldsymbol{\theta}}\) satisfies a property \(\varphi\). We require verifiers to **1.** report property satisfaction if and only if the property

Figure 1: **The computational graph of a residual unit [19].** In this figure, \(*\) denotes convolution, / denotes batch normalisation, \([\bullet]^{+}\) denotes ReLU, and \(+\) denotes addition. We use pink nodes \(\boxed\) for inputs, yellow \(\boxed\) for parameters, and blue \(\boxed\) for outputs.
is indeed satisfied (_soundness_) and **2.** to terminate (_completeness_). In this paper, we only require verifiers to support bounded hyperrectangles as property input sets and the non-negative real numbers as output set. Practically, verifiers can also handle more complicated input and output sets.

For formalising global specifications, we make use of _hyperproperties_. Hyperproperties extend properties by considering multiple input variables and input-dependent output sets.

Definition 4 (Hyperproperty): A _hyperproperty_\(\psi=(\mathcal{X}_{\psi},\mathcal{Y}_{\psi})\) is a tuple of a _multi-variable input set_\(\mathcal{X}_{\psi}\subseteq\left(\mathbb{R}^{n}\right)^{v}\) and an _input-dependent output set

\[\mathcal{Y}_{\psi}\subseteq\underbrace{\mathbb{R}^{n}\times\cdots\times \mathbb{R}^{n}}_{v\ times}\times\underbrace{\mathbb{R}^{m}\times\cdots\times \mathbb{R}^{m}}_{v\ times},\]

where \(n,m,v\in\mathbb{N}\). For a neural network \(\mathrm{net}_{\boldsymbol{\theta}}:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}\), we write \(\mathrm{net}_{\boldsymbol{\theta}}\vDash\psi\) if

\[\forall\boldsymbol{x}^{(1)},\ldots,\boldsymbol{x}^{(v)}\in\mathcal{X}_{\psi}: \Big{(}\boldsymbol{x}^{(1)},\ldots,\boldsymbol{x}^{(v)},\mathrm{net}_{ \boldsymbol{\theta}}\Big{(}\boldsymbol{x}^{(1)}\Big{)},\ldots,\mathrm{net}_{ \boldsymbol{\theta}}\Big{(}\boldsymbol{x}^{(v)}\Big{)}\Big{)}\in\mathcal{Y}_{ \psi}.\]

## 3 Formalising Global Specifications using Hyperproperties

Global specifications allow for expressing desired behaviour for the entire input domain of a neural network while local specifications only apply to small regions around known inputs. This property of local specifications brings with it that we have a fixed reference point for each property in a local specification. We typically do not have such a fixed reference point for global specifications, since they apply to the entire input domain.

For example, a local robustness property expresses that a classifier assigns the same class to all inputs that lie within a small \(L_{p}\)-ball \(\mathcal{B}_{p}(\boldsymbol{x})\) around a fixed input point \(\boldsymbol{x}\). Because we have this fixed input \(\boldsymbol{x}\) as a reference point, we know the class that should be assigned to all the inputs in \(\mathcal{B}_{p}(\boldsymbol{x})\). Knowing this class allows for judging whether an input \(\boldsymbol{x}^{\prime}\in\mathcal{B}_{p}(\boldsymbol{x})\) is a counterexample to the local robustness property by executing the network once for \(\boldsymbol{x}^{\prime}\).

If we now look at global robustness, we find that it does not suffice to consider a single execution of a network to check for specification violations. As the inputs now are arbitrary inputs from the entire input domain, we can not determine whether robustness is violated by looking only at the output for one input \(\boldsymbol{x}^{(1)}\). Instead, we need to find another input \(\boldsymbol{x}^{(2)}\in\mathcal{B}_{p}\big{(}\boldsymbol{x}^{(1)}\big{)}\) such that the classes that a network assigns to \(\boldsymbol{x}^{(1)}\) and \(\boldsymbol{x}^{(2)}\) do not match. Only in pair, these inputs form a counterexample. The necessity to compare outputs for multiple inputs requires us to adopt hyperproperties for formalising global specifications.

If we look more closely at our example of global robustness, we find that requiring the points in all \(L_{p}\)-balls to have the same output forces the network to produce the same output for all inputs. This means that we also have to consider more complicated output sets for global specifications. In this case, we either need to allow small changes in class scores (Example 2) or devise special
rules for points close to the decision boundary (Example 3). Furthermore, if we express global robustness as Lipschitz continuity [7] (Example 4), our output set needs to be _input-dependent_. This means that it does not suffice to only compare network outputs with network outputs to determine whether a specification is violated. Instead, we also need to take the inputs that lead to the observed outputs into account.

For the reasons outlined above, we consider hyperproperties with multi-variable input sets and input-dependent output sets as in Definition 4 for formalising global specifications. To leverage existing neural network verification approaches for verifying these hyperproperties, we express the multi-variable input set and the input-dependent output set using auxiliary neural networks.

Definition 5 (Neural-Network-Defined Hyperproperty): Let \(n,m,v,w\in\mathbb{N}\). A _Neural-Network-Defined Hyperproperty (NNDH)_ is a hyperproperty \(\psi=(\mathcal{X}_{\psi},\mathcal{Y}_{\psi})\), where \(\mathcal{X}_{\psi}=\{\mathrm{net}_{\mathrm{In}}(\mathbf{w})\mid\mathbf{w}\in\mathcal{ W}\}\) and

\[\mathcal{Y}_{\psi}=\left\{\mathbf{x}^{(1)},\ldots,\mathbf{x}^{(v)},\mathbf{y}^{(1)},\ldots,\mathbf{y}^{(v)}\ \Big{|}\,\mathrm{net}_{\mathrm{Sat}}\Big{(}\mathbf{x}^{(1)},\ldots,\mathbf{x}^{(v)}, \mathbf{y}^{(1)},\ldots,\mathbf{y}^{(v)}\Big{)}\geq 0\right.\right\},\]

where \(\mathcal{W}\subset\mathbb{R}^{w}\) is a bounded hyperrectangle and \(\mathrm{net}_{\mathrm{In}}:\mathbb{R}^{w}\to\left(\mathbb{R}^{n}\right)^{v}\) and \(\mathrm{net}_{\mathrm{Sat}}:\underbrace{\mathbb{R}^{n}\times\cdots\times \mathbb{R}^{n}}_{v\ times}\times\underbrace{\mathbb{R}^{m}\times\cdots\times \mathbb{R}^{m}}_{v\ times}\to\mathbb{R}\) are neural networks.

We can think of the neural network \(\mathrm{net}_{\mathrm{In}}\) as generating the multi-variable input set from a single-variable hyperrectangular input space. The neural network \(\mathrm{net}_{\mathrm{Sat}}\) serves as a _satisfaction function_[4] for the output set. A satisfaction function is non-negative if and only if an output -- or, in this case, a tuple of inputs and outputs -- lies within the output set or a property or hyperproperty.

It is central to Definition 5 that \(\mathrm{net}_{\mathrm{In}}\) and \(\mathrm{net}_{\mathrm{Sat}}\) do not _approximate_ our desired input and output set, but express them _exactly_. Usually, we train neural networks to approximate a potentially unknown relationship between inputs and outputs. The neural networks \(\mathrm{net}_{\mathrm{In}}\) and \(\mathrm{net}_{\mathrm{Sat}}\), however, are not trained but carefully constructed to generate our desired input and output set. As such, these auxiliary neural networks are relatively simple structures in this paper. Their main purpose is to make hyperproperties accessible for existing neural network verification approaches.

We now provide several concrete examples of NNDHs including concrete \(\mathrm{net}_{\mathrm{In}}\) and \(\mathrm{net}_{\mathrm{Sat}}\) networks. We formalise global monotonicity, two notions of global robustness [21, 24], Lipschitz continuity, and dependency fairness [15, 35] as NNDHs. Afterwards, we show how NNDHs can be verified using existing neural network verifiers that can handle general computational graphs.

In the following, let \(\mathcal{X}\subset\mathbb{R}^{n}\) be the bounded hyperrectangular input domain of the neural network under consideration. This domain is determined by the target application. In the case of image classification, for example, \(\mathcal{X}\) would be the (normalised) pixel space.

Example 1 (Global Monotonicity): Monotonicity is a desired behaviour of a neural network in applications from medicine to aviation [33]. Here, we formalise
that the output \(j\in\{1,\ldots,m\}\) may not _increase_ when input \(i\in\{1,\ldots,n\}\) increases. Non-decreasing monotonicity can be formalised analogously. We formalise global monotonicity as a hyperproperty \(\psi_{M}=(\mathcal{X}_{\psi_{M}},\mathcal{Y}_{\psi_{M}})\), where the input set \(\mathcal{X}_{\psi_{M}}\subseteq\mathcal{X}\times\mathcal{X}\) and output set \(\mathcal{Y}_{\psi_{M}}\subset\mathbb{R}^{n}\times\mathbb{R}^{n}\times\mathbb{ R}^{m}\times\mathbb{R}^{m}\) are

\[\mathcal{X}_{\psi_{M}} =\left\{\boldsymbol{x}^{(1)},\boldsymbol{x}^{(2)}\;\left|\; \boldsymbol{x}^{(2)}_{i}\geq\boldsymbol{x}^{(1)}_{i}\right.\right\}\] \[\mathcal{Y}_{\psi_{M}} =\left\{\boldsymbol{x}^{(1)},\boldsymbol{x}^{(2)},\boldsymbol{y} ^{(1)},\boldsymbol{y}^{(2)}\;\left|\;\boldsymbol{y}^{(2)}_{j}\leq\boldsymbol{y }^{(1)}_{j}\right.\right\}.\]

To generate these sets using neural networks to obtain an NNDH, we define

\[\mathcal{W}_{M}=\left\{\boldsymbol{x}^{(1)}_{1},\ldots,\boldsymbol{x}^{(1)}_ {n},\boldsymbol{x}^{(2)}_{1},\ldots,\boldsymbol{x}^{(2)}_{n}\;\left|\; \boldsymbol{x}^{(1)},\boldsymbol{x}^{(2)}\in\mathcal{X}\right.\right\},\]

\[\text{net}_{\text{In}_{M}}\Big{(}\boldsymbol{x}^{(1)}_{1},\ldots, \boldsymbol{x}^{(1)}_{n},\boldsymbol{x}^{(2)}_{1},\ldots,\boldsymbol{x}^{(2)} _{n}\Big{)}=\Big{(}\boldsymbol{x}^{\prime(1)},\boldsymbol{x}^{\prime(2)} \Big{)}\,,\]

\[\text{where }\boldsymbol{x}^{\prime(1)}=\Big{(}\boldsymbol{x}^{(1)}_{1}, \ldots,\min\Big{(}\boldsymbol{x}^{(1)}_{i},\boldsymbol{x}^{(2)}_{i}\Big{)}, \ldots,\boldsymbol{x}^{(1)}_{n}\Big{)}\]

\[\boldsymbol{x}^{\prime(2)}=\Big{(}\boldsymbol{x}^{(2)}_{1},\ldots,\max\Big{(} \boldsymbol{x}^{(1)}_{i},\boldsymbol{x}^{(2)}_{i}\Big{)},\ldots,\boldsymbol{x }^{(2)}_{n}\Big{)}\,,\]

and

\[\text{net}_{\text{Sat}_{M}}\Big{(}\boldsymbol{x}^{(1)},\boldsymbol{x}^{(2)}, \boldsymbol{y}^{(1)},\boldsymbol{y}^{(2)}\Big{)}=\boldsymbol{y}^{(1)}_{j}- \boldsymbol{y}^{(2)}_{j}.\]

The function \(\text{net}_{\text{Sat}_{M}}\) is a neural network with a single affine layer. Concerning \(\text{net}_{\text{In}_{M}}\), we can compute max either using a maxpooling layer or by leveraging \(\forall a,b\in\mathbb{R}:\max(a,b)=\left[a-b\right]^{+}+b\) where \(\left[\bullet\right]^{+}=\max(\bullet,0)\) is ReLU. Furthermore, since \(\forall a,b\in\mathbb{R}:\min(a,b)=-\max(-a,-b)\), we can also compute min in a neural network. Therefore, \(\mathcal{W}_{M}\), \(\text{net}_{\text{In}_{M}}\) and \(\text{net}_{\text{Sat}_{M}}\) together form an NNDH having \(\mathcal{X}_{\psi_{M}}\) as its input set and \(\mathcal{Y}_{\psi_{M}}\) as its output set.

Example 2: (Global \(L_{\infty}\) Robustness following [21]).: Neural networks are susceptible to adversarial attacks where slightly modifying the input allows an attacker to control the output produced by a neural network [34]. This is a safety concern, for example, for traffic sign recognition [12] and biometric authentication using face recognition [31]. In this example, we express \(L_{\infty}\) global robustness according to [21] as an NNDH. This specification limits how much the output of a neural network may change for inputs that lie within an \(L_{\infty}\)-ball of a certain size. Let \(\delta,\varepsilon\in\mathbb{R}_{>0}\) be the radius of the \(L_{\infty}\)-ball and the permitted magnitude of change, respectively. Let

\[\mathcal{W}_{R} =\{\boldsymbol{x}_{1},\ldots,\boldsymbol{x}_{n},\boldsymbol{ \tau}_{1},\ldots,\boldsymbol{\tau}_{n}\mid\boldsymbol{x}\in\mathcal{X}, \boldsymbol{\tau}\in\left[-\delta,\delta\right]^{n}\}\] \[\text{net}_{\text{In}_{R}}(\boldsymbol{x}_{1},\ldots,\boldsymbol {x}_{n},\boldsymbol{\tau}_{1},\ldots,\boldsymbol{\tau}_{n}) =(\boldsymbol{x},\text{project}_{\mathcal{X}}(\boldsymbol{x}+ \boldsymbol{\tau}))\] \[\text{net}_{\text{Sat}_{R1}}\Big{(}\boldsymbol{x}^{(1)}, \boldsymbol{x}^{(2)},\boldsymbol{y}^{(1)},\boldsymbol{y}^{(2)}\Big{)} =\varepsilon-\left\|\boldsymbol{y}^{(1)}-\boldsymbol{y}^{(2)} \right\|_{\infty}=\varepsilon-\max_{j=1}^{m}\left|\boldsymbol{y}^{(1)}_{j}- \boldsymbol{y}^{(2)}_{j}\right|,\]

where \(\text{project}_{\mathcal{X}}\) computes the projection into the hyperrectangle \(\mathcal{X}\). Projecting a point \(\boldsymbol{x}\) into a hyperrectangle corresponds to computing the minimum between each coordinate and the lower boundary of the hyperrectangle and the
maximum between each coordinate and the upper boundary of the hyperrectangle. As we show in Example 1, we can compute minima and maxima in a neural network. Similarly, \(\mathrm{net}_{\mathrm{Sat}}R1\) computes a maximum and absolute values, which we can compute by leveraging \(\forall a\in\mathbb{R}:|a|=\max(a,-a)\). Overall, \(\mathcal{W}_{R}\), \(\mathrm{net}_{\mathrm{In}_{R}}\), and \(\mathrm{net}_{\mathrm{Sat}_{R1}}\) define an NNDH \(\psi_{R1}=(\mathcal{X}_{\psi_{R}},\mathcal{Y}_{\psi_{R1}})\), where \(\mathcal{X}_{\psi_{R}}\subset\mathcal{X}\times\mathcal{X}\) and \(\mathcal{Y}_{\psi_{R1}}\subset\mathbb{R}^{n}\times\mathbb{R}^{n}\times\mathbb{ R}^{m}\times\mathbb{R}^{m}\), with

\[\mathcal{X}_{\psi_{R}} =\left\{\mathbf{x}^{(1)},\mathbf{x}^{(2)}\ \Big{|}\ \Big{\|}\mathbf{x}^{(1)}-\mathbf{x}^{(2)}\Big{\|}_{\infty}\leq\delta\right\}\] \[\mathcal{Y}_{\psi_{R1}} =\left\{\mathbf{x}^{(1)},\mathbf{x}^{(2)},\mathbf{y}^{(1)},\mathbf{y}^{(2)}\ \Big{|}\ \Big{\|}\mathbf{y}^{(1)}-\mathbf{y}^{(2)}\Big{\|}_{\infty}\leq\varepsilon\right\}.\]

This captures that a network is globally robust as defined in [21].

Example 3 (Global \(L_{\infty}\) Robustness following [24]): We also present an alternative definition of global robustness using an extra class representing non-robustness at an input point [24]. This definition may be more desirable in some applications, as it still permits non-robustness for noise-only _rubbish class_ inputs [17] that lie off the data manifold. Let \(\delta\in\mathbb{R}_{>0}\) be as in Example 2. Assume the classifier network we are studying produces an additional output \(\bot=m+1\) that shall indicate non-robustness. We reuse \(\mathcal{X}_{\psi_{R}}\) from Example 2 and define \(\psi_{R2}=(\mathcal{X}_{\psi_{R}},\mathcal{Y}_{\psi_{R2}})\), where \(\mathcal{Y}_{\psi_{R2}}\subset\mathbb{R}^{n}\times\mathbb{R}^{n}\times\mathbb{ R}^{m+1}\times\mathbb{R}^{m+1}\) and, concretely,

\[\mathcal{Y}_{\psi_{R2}}=\left\{\mathbf{x}^{(1)},\mathbf{x}^{(2)},\mathbf{y}^{(1)},\mathbf{y}^{ (1)}\ \Big{|}\ N\!R\!\left(\mathbf{y}^{(1)}\right)\lor N\!R\!\left(\mathbf{y}^{(2)}\right) \lor Same\!\left(\mathbf{y}^{(1)},\mathbf{y}^{(2)}\right)\Big{\}}\,,\]

where

\[N\!R\!\left(\mathbf{y}\right) =\bigwedge_{j=1}^{m}\mathbf{y}_{\bot}^{(k)}\geq\mathbf{y}_{j}^{(k)}\] \[Same\!\left(\mathbf{y}^{(1)},\mathbf{y}^{(2)}\right) =\bigvee_{j_{1}=1}^{m}\bigwedge_{k=1}^{2}\bigwedge_{j_{2}=1}^{m} \mathbf{y}_{j_{1}}^{(k)}\geq\mathbf{y}_{j_{2}}^{(k)}.\]

Intuitively, \(N\!R\) captures that the extra class \(\bot\) is assigned to an input, while \(Same\) captures that the same class is assigned to \(\mathbf{y}^{(1)}\) and \(\mathbf{y}^{(2)}\)1. To construct a neural network \(\mathrm{net}_{\mathrm{Sat}_{R2}}\) that serves as a satisfaction function for \(\psi_{R2}\), we note that for an arbitrary vector \(\mathbf{u}\in\mathbb{R}^{u}\), \(u\in\mathbb{N}\)

Footnote 1: Strictly speaking, \(Same\) only requires that there is an intersection between the largest elements of \(\mathbf{y}^{(1)}\) and \(\mathbf{y}^{(2)}\). This comes into play when the assigned class is ambiguous due to an output having several largest elements.

\[\bigvee_{a\in\mathcal{A}}\bigwedge_{b\in B(a)}\mathbf{u}_{k_{1}(a,b) }\geq\mathbf{u}_{k_{2}(a,b)} \tag{1}\] \[\Leftrightarrow \left(\max_{a\in\mathcal{A}}\min_{b\in B(a)}\mathbf{u}_{k_{1}(a,b)}- \mathbf{u}_{k_{2}(a,b)}\right)\geq 0, \tag{2}\]

where \(\mathcal{A}\) and \(\mathcal{B}\) are finite sets, \(B:\mathcal{A}\to 2^{\mathcal{B}}\), and \(k_{1},k_{2}:\mathcal{A}\times\mathcal{B}\to\mathbb{N}\). As we can transform any formula in propositional logic into Disjunctive Normal Form, we
can bring the formula defining \(\mathcal{Y}_{\psi_{R2}}\) into the form of Equation (1). Therefore, since we can compute \(\min\) and \(\max\) using a neural network (Example 1), we can define a neural network \(\mathrm{net}_{\mathrm{Sat}_{R2}}\) serving as a satisfaction function for \(\psi_{R2}\). Together with \(\mathcal{W}\) and \(\mathrm{net}_{\mathrm{In}_{R}}\) from Example 2, \(\mathrm{net}_{\mathrm{Sat}_{R2}}\) defines an NNDH with the same input and output set as \(\psi_{R2}\).

Example 4 (Lipschitz Continuity): The Lipschitz continuity of a neural network is linked not only to robustness [34] but also to fairness [10], generalisation [3], and explainability [13]. While many neural network architectures are always Lipschitz continuous [7; 34; 29], it is the magnitude of the Lipschitz constant that matters [7]. Let \(K\in\mathbb{R}_{\geq 0}\) be the desired global Lipschitz constant. Define \(\mathcal{W}_{C}=\left\{\left.\mathbf{x}_{1}^{(1)},\ldots,\mathbf{x}_{n}^{(1)},\mathbf{x}_ {1}^{(2)},\ldots,\mathbf{x}_{n}^{(2)}\ \right|\ \mathbf{x}^{(1)},\mathbf{x}^{(2)}\in\mathcal{X}\right\}\) and

\[\mathrm{net}_{\mathrm{In}_{C}}\Big{(}\mathbf{x}_{1}^{(1)},\ldots,\mathbf{ x}_{n}^{(1)},\mathbf{x}_{1}^{(2)},\ldots,\mathbf{x}_{n}^{(2)}\Big{)} =\Big{(}\mathbf{x}^{(1)},\mathbf{x}^{(2)}\Big{)}\] \[\mathrm{net}_{\mathrm{Sat}_{C}}\Big{(}\mathbf{x}^{(1)},\mathbf{x}^{(2)}, \mathbf{y}^{(1)},\mathbf{y}^{(2)}\Big{)} =K\Big{\|}\mathbf{x}^{(1)}-\mathbf{x}^{(2)}\Big{\|}_{\infty}-\Big{\|}\mathbf{ y}^{(1)}-\mathbf{y}^{(2)}\Big{\|}_{\infty}.\]

First, \(\mathrm{net}_{\mathrm{In}_{C}}\) is an identity function and, thus, a trivial neural network. Then, by computing \(\|\bullet\|_{\infty}\) as in Example 2 in a neural network, we obtain an NNDH \(\psi_{C}=(\mathcal{X}_{\psi_{C}},\mathcal{Y}_{\psi_{C}})\) with

\[\mathcal{X}_{\psi_{C}} =\mathcal{X}\times\mathcal{X}\] \[\mathcal{Y}_{\psi_{C}} =\left\{\mathbf{x}^{(1)},\mathbf{x}^{(2)},\mathbf{y}^{(1)},\mathbf{y}^{(2)}\ \Big{|}\ \Big{\|}\mathbf{y}^{(1)}-\mathbf{y}^{(2)}\Big{\|}_{\infty}\leq K\left\|\mathbf{x}^{(1)}- \mathbf{x}^{(2)}\right\|_{\infty}\right\},\]

which corresponds to Lipschitz continuity with Lipschitz constant \(K\).

Example 5 (Dependency Fairness): Machine learning applications from automated hiring [6] to image classification [28] bear the danger of producing unfair machine-learning models. However, in some applications, ensuring fairness may be legally required [27]. One fairness requirement that we may pose is that "similar individuals are treated similarly" [10]. _Dependency fairness_[15; 35] is a fairness criterion based on this idea2. Assume the first dimension of the input space is a categorical sensitive attribute with \(A\in\mathbb{N}\) disjoint values. We consider two inputs to be _similar_ if they are equal except for the sensitive attribute. Dependency fairness specifies that all similar inputs are assigned to the same class. Let \(\psi_{F}=(\mathcal{X}_{\psi_{F}},\mathcal{Y}_{\psi_{F}})\), with \(\mathcal{X}_{\psi_{F}}\subset\mathcal{X}^{A}\), \(\mathcal{Y}_{\psi_{F}}\subset\left(\mathbb{R}^{n}\right)^{A}\times\left( \mathbb{R}^{m}\right)^{A}\), where

Footnote 2: We believe dependency fairness is an overly simplistic fairness criterion as it can be trivially satisfied by withholding sensitive attributes from the neural network, which is known to be insufficient for real-world fairness [2]. However, we still think that dependency fairness is suitable as an example for experimenting with verifying global specifications.

Let \(\psi_{F}=(\mathcal{X}_{\psi_{F}},\mathcal{Y}_{\psi_{F}})\), with \(\mathcal{X}_{\psi_{F}}\subset\mathcal{X}^{A}\), \(\mathcal{Y}_{\psi_{F}}\subset\left(\mathbb{R}^{n}\right)^{A}\times\left( \mathbb{R}^{m}\right)^{A}\), where

\[\mathcal{X}_{\psi_{F}} =\left\{\mathbf{x}^{(1)},\ldots,\mathbf{x}^{(A)}\ \left|\begin{array}{c}\forall k\in\{1,\ldots,A\}:\\ \Big{(}\mathbf{x}_{1}^{(k)}=k\wedge\forall i\in\{2,\ldots,n\}:\mathbf{x}_{i}^{(1)}=\bm {x}_{i}^{(k)}\Big{)}\end{array}\right.\right\}\] \[\mathcal{Y}_{\psi_{F}} =\left\{\mathbf{x}^{(1)},\ldots,\mathbf{x}^{(A)},\mathbf{y}^{(1)},\ldots,\mathbf{ y}^{(A)}\ \left|\begin{array}{c}\bigvee_{j_{1}=1}^{m}\bigwedge_{k=1}^{A}\bigwedge_{j_{2}=1}^{m} \mathbf{y}_{j_{1}}^{(k)}\geq\mathbf{y}_{j_{2}}^{(k)}\end{array}\right.\right\}.\]
We can construct a neural network satisfaction function \(\mathrm{net}_{\mathrm{Sat}_{F}}\) for this property analogously to Example 3. The input set \(\mathcal{X}_{\psi_{F}}\) consists of tuples of similar inputs which contain each value of the sensitive attribute in a fixed order. Let \(\mathbf{A}\in\mathbb{R}^{n\times n}\) be the diagonal matrix with \(0,1,\ldots,1\) on its diagonal. Let \(\mathrm{assign}:\mathbb{N}\times\mathbb{R}\rightarrow\mathbb{R}\) be an affine function with \(\mathrm{assign}(k,\mathbf{x})=\mathbf{A}\mathbf{x}+(k,0,\ldots,0)^{T}\). Define \(\mathcal{W}=\mathcal{X}\) and \(\mathrm{net}_{\mathrm{In}_{F}}(\mathbf{x})=(\mathrm{assign}(1,\mathbf{x}),\ldots, \mathrm{assign}(A,\mathbf{x}))\). Since assign is affine, \(\mathrm{net}_{\mathrm{In}_{F}}\) is a neural network. Overall, \(\mathcal{W}\), \(\mathrm{net}_{\mathrm{In}_{F}}\), and \(\mathrm{net}_{\mathrm{Sat}_{F}}\) define an NNDH with the same input and output set as \(\psi_{F}\).

These examples demonstrate that Definition 5 is an expressive specification formalism, despite restricting input and output sets to be defined by neural networks. It remains to show that we can indeed verify NNDHs using existing neural network verification approaches. This builds upon the ability to verify general computational graphs. In [37], the Linear Relaxation-based Perturbation Analysis (LiRPA) framework is extended to general computational graphs. LiRPA underlies verifiers such as \(\alpha\),\(\beta\)-CROWN [38] and ERAN [32], and is used in Marabou [22] and MN-BaB [14], among others. Among these verifiers, \(\alpha\),\(\beta\)-CROWN already supports verifying general computational graphs.

The central idea in verifying an NNDH \(\psi\) is to compose the network to verify \(\mathrm{net}_{\mathbf{\theta}}\) with itself and the networks \(\mathrm{net}_{\mathrm{In}_{\psi}}\) and \(\mathrm{net}_{\mathrm{Sat}_{\psi}}\) that define the input and output set of \(\psi\).

Theorem 3.1 (NNDH Verification): _Let \(\psi=(\mathcal{X}_{\psi},\mathcal{Y}_{\psi})\) with \(\mathcal{W}\subseteq\mathbb{R}^{w}\), \(\mathrm{net}_{\mathrm{In}}:\mathbb{R}^{w}\rightarrow(\mathbb{R}^{n})^{v}\) and \(\mathrm{net}_{\mathrm{Sat}}:(\mathbb{R}^{m})^{v}\rightarrow\mathbb{R}\) be an NNDH. Let \(\mathrm{net}_{\mathbf{\theta}}:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}\) be a neural network. Define \(\mathrm{net}^{\prime}_{\mathbf{\theta}}:\mathbb{R}^{w}\rightarrow\mathbb{R}\) as_

\[\mathrm{net}^{\prime}_{\mathbf{\theta}}(\mathbf{w}) =\mathrm{net}_{\mathrm{Sat}}\Big{(}\mathbf{x}^{(1)},\ldots,\mathbf{x}^{(v )},\mathrm{net}_{\mathbf{\theta}}\Big{(}\mathbf{x}^{(1)}\Big{)},\ldots,\mathrm{net}_{ \mathbf{\theta}}\Big{(}\mathbf{x}^{(v)}\Big{)}\Big{)}\] \[\text{where }\mathbf{x}^{(1)},\ldots,\mathbf{x}^{(v)}=\mathrm{net}_{ \mathrm{In}}(\mathbf{w}).\]

_Further, let \(\varphi=(\mathcal{W},\mathbb{R}_{\geq 0})\). It holds that \(\mathrm{net}^{\prime}_{\mathbf{\theta}}\models\varphi\Leftrightarrow\mathrm{net}_{ \mathbf{\theta}}\models\psi\)._

Proof: Theorem 3.1 follows from applying Definitions 3 and 5. 

Figure 2 visualises \(\mathrm{net}^{\prime}_{\mathbf{\theta}}\) from Theorem 3.1. We construct a new computational graph by generating several inputs using \(\mathrm{net}_{\mathrm{In}}\) and feeding each input to a separate copy of \(\mathrm{net}_{\mathbf{\theta}}\). Finally, \(\mathrm{net}_{\mathrm{Sat}}\) takes the generated inputs and the output of each copy of \(\mathrm{net}_{\mathbf{\theta}}\) and computes the satisfaction function value. Considering several copies of the same artefact is known as _self-composition_[8]. As Theorem 3.1 shows, verifying an NNDH \(\psi\) corresponds to verifying a property \(\varphi\) of the new computational graph \(\mathrm{net}^{\prime}_{\mathbf{\theta}}\). Overall, \(\mathrm{net}^{\prime}_{\mathbf{\theta}}\) has a more complicated graph structure than \(\mathrm{net}_{\mathbf{\theta}}\), but it only contains computations that also appear in \(\mathrm{net}_{\mathbf{\theta}}\), \(\mathrm{net}_{\mathrm{In}}\) or \(\mathrm{net}_{\mathrm{Sat}}\). Therefore, \(\psi\) can be verified using verifiers that can verify \(\mathrm{net}_{\mathbf{\theta}}\), \(\mathrm{net}_{\mathrm{In}}\) and \(\mathrm{net}_{\mathrm{Sat}}\) and support general computational graphs.

## 4 Related Work

Using self-composition for verifying specific global specifications was explored previously [21, 23]. We use self-composition for verifying a range of global speci
fications. Improved encodings of self-composition [36] and approaches from differential verification of neural networks [26] are interesting directions for improving the verification of NNDHs.

In 2017, verifying global robustness was found to be infeasible using the then-available verifiers [21]. Recent approaches to global robustness [36] and global fairness specifications [35] have demonstrated that verifying global specifications is feasible today. The reason behind this could be that practically, neural networks appear not to realise their full combinatorial potential [18], in a way that allows for efficient branch-and-bound verification [35].

## 5 Conclusion

We present a versatile formalism for expressing global specifications while maintaining compatibility with existing verification approaches. Evaluating this approach empirically remains future work. A promising verifier for this approach is \(\alpha\),\(\beta\)-CROWN [38], as it already supports verifying arbitrary computational graphs. An interesting direction is comparing our generally applicable approach with approaches specialised to individual global specifications, such as, global robustness [36], dependency fairness [35] and Lipschitz continuity [5].

Figure 2: **Computational Graph for Verifying NNDHs.** Verifying an NNDH (Definition 5) reduces to verifying an input-output property of the computational graph in this figure. The boxes enclose sub-graphs of the computational graph. The contents of each box are placeholders. Pink nodes represent inputs, yellow nodes represent parameters, and blue nodes represent outputs. The input and output nodes in each sub-graph are repetitions of their direct predecessors or direct successors outside of the subgraph. The inputs of \(\mathrm{net}_{\mathrm{Sat}}\) were rearranged for better legibility.