Enumerating Safe Regions in Deep Neural Networks with Provable
  Probabilistic Guarantees
Identifying safe areas is a key point to guarantee trust for systems that are
based on Deep Neural Networks (DNNs). To this end, we introduce the
AllDNN-Verification problem: given a safety property and a DNN, enumerate the
set of all the regions of the property input domain which are safe, i.e., where
the property does hold. Due to the #P-hardness of the problem, we propose an
efficient approximation method called epsilon-ProVe. Our approach exploits a
controllable underestimation of the output reachable sets obtained via
statistical prediction of tolerance limits, and can provide a tight (with
provable probabilistic guarantees) lower estimate of the safe areas. Our
empirical evaluation on different standard benchmarks shows the scalability and
effectiveness of our method, offering valuable insights for this new type of
verification of DNNs.
Luca Marzari, Davide Corsi, Enrico Marchesini, Alessandro Farinelli, Ferdinando Cicalese
# Enumerating Safe Regions in Deep Neural Networks

###### Abstract

Identifying safe areas is a key point to guarantee trust for systems that are based on Deep Neural Networks (DNNs). To this end, we introduce the _AllDNN-Verification_ problem: given a safety property and a DNN, enumerate the set of all the regions of the property input domain which are safe, i.e., where the property does hold. Due to the #P-hardness of the problem, we propose an efficient approximation method called \(\epsilon\)-ProVe. Our approach exploits a controllable underestimation of the output reachable sets obtained via statistical prediction of tolerance limits, and can provide a tight --with provable probabilistic guarantees-- lower estimate of the safe areas. Our empirical evaluation on different standard benchmarks shows the scalability and effectiveness of our method, offering valuable insights for this new type of verification of DNNs.

## Introduction

Deep Neural Networks (DNNs) have emerged as a groundbreaking technology revolutionizing various fields ranging from autonomous navigation [12, 13] to image classification [14] and robotics for medical applications [15]. However, while DNNs can perform remarkably well in different scenarios, their reliance on massive data for training can lead to unexpected behaviors and vulnerabilities in real-world applications. In particular, DNNs are often considered "black-box" systems, meaning their internal representation is not fully transparent. A crucial DNNs weakness is the vulnerability to adversarial attacks [16, 1], wherein small, imperceptible modifications to input data can lead to wrong and potentially catastrophic decisions when deployed.

To this end, Formal Verification (FV) of DNNs [12, 13] holds great promise to provide assurances on the safety aspect of these functions before the actual deployment in real scenarios. In detail, the decision version of the _DNN-Verification_ problem takes as input a trained DNN \(\mathcal{N}\) and a safety property, typically expressed as an input-output relationship for \(\mathcal{N}\), and aims at determining whether there exists at least an input configuration which results in a violation of the safety property. It is crucial to point out that due to the fact that the DNN's input is typically defined in a continuous domain any empirical evaluation of a safety property cannot rely on testing all the (infinitely many) possible input configurations.

In contrast, FV can provide provable assurances on the DNNs' safety aspect. However, despite the considerable advancements made by DNN-verifiers over the years [17, 18, 19], the binary result (_safe_ or _unsafe_) provided by these tools is generally not sufficient to gain a comprehensive understanding of these functions. For instance, when comparing two neural networks and employing a FV tool that yields a _unsafe_ answer for both (i.e., indicating the existence of at least one violation point) we cannot distinguish whether one model exhibits only a small area of violation around the identified counterexample, while the other may have multiple and widespread violation areas.

To overcome this limitation, a quantitative variant of FV, asking for the number of violation points, has been proposed and analyzed, first in [1] for the restricted class of Binarized Neural Networks (BNNs) and more recently in [11] for general DNNs. Following [11] we will henceforth refer to such counting problem as _#DNN-Verification_. Due to the #P-Completeness of the _#DNN-Verification_, both studies in [1, 12], focus on efficient approximate solutions, which allow the resolution of large-scale real-world problems while providing provable (probabilistic) guarantees regarding the computed count.

Solutions to the _#DNN-Verification_ problem allow to estimate the probability that a DNN violates a given property but they do not provide information on the actual input configurations that are safe or violations for the property of interest.

On the other hand, knowledge of the distribution of safe and unsafe areas in the input space is a key element to devise approaches that can enhance the safety of DNNs, e.g., by patching unsafe areas through re-training.

To this aim, we introduce the _AllDNN-Verification_ problem, which corresponds to computing the set of all the areas that do not result in a violation for a given DNN and a safety property (i.e., enumerating all the safe areas of a property's input domain). The _AllDNN-Verification_ is at least as hard as _#DNN-Verification_, i.e., it is easily shown to be #P-Hard.

Hence, we propose \(\epsilon\)-ProVe, an approximation ap
proach that provides provable (probabilistic) guarantees on the returned areas. \(\epsilon\)-ProVe is built upon interval analysis of the DNN output reachable set and the iterative refinement approach [22], enabling efficient and reliable enumeration of safe areas.1

Footnote 1: We point out that the _AllDNN-Verification_ can also be defined to compute the set of unsafe regions. For better readability, in this work, we will only focus on safe regions. The definition and the solution proposed are directly derivable also when applied to unsafe areas.

Notice that state-of-the-art FV methods typically propose an over-approximated output reachable set, thereby ensuring the soundness of the result. Nonetheless, the relaxation of the nonlinear activation functions employed to compute the over-approximate reachable set has non-negligible computational demands. In contrast, \(\epsilon\)-ProVe provides a scalable solution based on an underestimation of the output reachable set that exploits the _Statistical Prediction of Tolerance Limits_[13]. In particular, we demonstrate how, with a confidence \(\alpha\), our underestimation of the reachable set computed with \(n\) random input configurations sampled from the initial property's domain \(A\) is a correct output reachable set for at least a fraction \(R\) of an indefinitely large further sample of points. Broadly speaking, this result tells us that if all the input configurations obtained in a random sample produce an output reachable set that does not violate the safety property (i.e., a _safe_ output reachable set) then, with probability \(\alpha\), at least a subset of \(A\) of size \(R\cdot|A|\) is safe (i.e., \(R\) is a lower bound on the safe rate in \(A\) with confidence \(\alpha\)).

In summary, the main contributions of this paper are the following:

* We initiate the study of the _AllDNN-verification_ problem, the enumeration version of the DNN-Verification
* Due to the #P-hardness of the problem, we propose \(\epsilon\)-ProVe a novel polynomial approximation method to obtain a provable (probabilistic) lower bound of the safe zones within a given property's domain.
* We evaluate our approach on FV standard benchmarks, showing that \(\epsilon\)-ProVe is scalable and effective for real-world scenarios.

## Preliminaries

In this section, we discuss existing FV approaches and related key concepts on which our approach is based. In contrast to the standard robustness and adversarial attack literature [16, 15, 14], FV of DNNs seeks formal guarantees on the safety aspect of the neural network given a specific input domain of interest. Broadly speaking, if a DNN-Verification tool states that the region is provably verified, this implies that there are no adversarial examples - violation points - in that region. We recall in the next section the formal definition of the satisfiability problem for _DNN-Verification_[16].

### DNN-Verification

In the _DNN-Verification_, we have as input a tuple \(\mathcal{T}=\langle\mathcal{N},\mathcal{P},\mathcal{Q}\rangle\), where \(\mathcal{N}\) is a DNN, \(\mathcal{P}\) is precondition on the input, and \(\mathcal{Q}\) a postcondition on the output. In particular, \(\mathcal{P}\) denotes a particular input domain or region for which we require a particular postcondition \(\mathcal{Q}\) to hold on the output of \(\mathcal{N}\). Since we are interested in discovering a possible counterexample, \(\mathcal{Q}\) typically encodes the negation of the desired behavior for \(\mathcal{N}\). Hence, the possible outcomes are SAT if there exists an input configuration that lies in the input domain of interest, satisfying the predicate \(\mathcal{P}\), and for which the DNN satisfies the postcondition \(\mathcal{Q}\), i.e., at least one violation exists in the considered area, UNSAT otherwise.

To provide the reader with a better intuition on the _DNN-Verification_ problem, we discuss a toy example.

**Example 1**.: _(DNN-Verification) Suppose we want to verify that for the toy DNN \(\mathcal{N}\) depicted in Fig. 1 given an input vector \(x=(x_{1},x_{2})\in[0,1]\times[0,1]\), the resulting output should always be \(y\geq 0\). We define \(\mathcal{P}\) as the predicate on the input vector \(x=(x_{1},x_{2})\) which is true iff \(x\in[0,1]\times[0,1]\), and \(\mathcal{Q}\) as the predicate on the output \(y\) which is true iff \(y=\mathcal{N}(x)<0\), that is, we set \(\mathcal{Q}\) to be the negation of our desired property. As reported in Fig. 1, given the vector \(x=(1,0)\) we obtain \(y<0\), hence the verification tool returns a SAT answer, meaning that a specific counterexample exists and thus the original safety property does not hold._

### #DNN-Verification

Despite the provable guarantees and the advancement that formal verification tools have shown in recent years [15, 16, 14, 22], the binary nature of the result of the _DNN-Verification_ problem may hide additional information about the safety aspect of the DNNs. To address this limitation in [16] the authors introduce the _#DNN-Verification_, i.e., the extension of the decision problem to its counting version. In this problem, the input is the same as the decision version, but we denote as \(\Gamma(\mathcal{T})\) the set of _all_ the input configurations for \(\mathcal{N}\) satisfying the property defined by \(\mathcal{P}\) and \(\mathcal{Q}\), i.e.

\[\Gamma(\mathcal{T})=\left\{x\;\big{|}\;\mathcal{P}(x)\wedge\mathcal{Q}( \mathcal{N}(x))\right\} \tag{1}\]

Then, the _#DNN-Verification_ consists of computing \(|\Gamma(\mathcal{T})|\).

The approach (reported in Fig.2) solves the problem in a sound and complete fashion where any state-of-the-art FV tool for the decision problem can be employed to check each

Figure 1: A counterexample for a toy _DNN-Verification_ problem.
node of the Branch-and-Bound (Bunel et al. 2018) tree recursively. In detail, each node produces a partition of the input space into two equal parts as long as it contains both a point that violates the property and a point that satisfies it. The leaves of this recursion tree procedure correspond to partitioning the input space into parts where we have either complete violations or safety. Hence, the provable count of the safe areas is easily computable by summing up the cardinality of the subinput spaces in the leaves that present complete safety.

Clearly, by using this method, it is possible to exactly count (and even to enumerate) the safe points. However, due to the necessity of solving a _DNN-Verification_ instance at each node (an intractable problem that might require exponential time), this approach becomes soon unfeasible and struggles to scale on real-world scenarios. In fact, it turns out that under standard complexity assumption, no efficient and scalable approach can return the exact set of areas in which a DNN is provably safe (as detailed in the next section).

To address this concern, after formally defining the _AllDNN-Verification_ problem and its complexity, we propose first of all a relaxation of the problem, and subsequently, an approximate method that exploits the analysis of underestimated output reachable sets obtained using statistical prediction of tolerance limits (Wilks 1942) and provides a tight underapproximation of the safe areas with strong probabilistic guarantees.

## The AllDNN-Verification Problem

The _AllDNN-Verification_ problem asks for the set of all the safe points for a particular tuple \(\langle\mathcal{N},\mathcal{P},\mathcal{Q}\rangle\).

Formally:

**Definition 1** (_AllDNN-Verification Problem_).:

**Input**: _A tuple \(\mathcal{T}=\langle\mathcal{N},\mathcal{P},\mathcal{Q}\rangle\)._

**Output**: _the set of safe points \(\Gamma(\mathcal{T})\), as given in (1)._

Considering the example of Fig. 2 solving the _AllDNN-Verification_ problem for the safe areas consists in returning the set: \(\Gamma=\Bigg{\{}\big{[}[0.5,1],[0,1]\big{]}\cup\big{[}[0,0.24],[0,0.49]\big{]} \Bigg{\}}\).

### Hardness of _AllDNN-Verification_

From the #P-completeness of the _#DNN-Verification_ problem proved in (Marzari et al. 2023) and the fact that exact enumeration also provides exact counting it immediately follows that the _AllDNN-Verification_ is _#P-hard_, which essentially states that no polynomial algorithm is expected to exists for the _AllDNN-Verification_ problem.

#### \(\epsilon\)-ProVe: a Provable (Probabilistic) Approach

In view of the structural scalability issue of any solution to the _AllDNN-Verification_ problem, due to its #P-hardness, we propose to resort to an approximate solution. More precisely, we define the following approximate version of the _AllDNN-Verification_ problem:

**Definition 2** (\(\epsilon\)-_Rectilinear Under-Approximation of safe areas for DNN (\(\epsilon\)-Rua-Dnn)_).:

**Input**: _A tuple \(\mathcal{T}=\langle\mathcal{N},\mathcal{P},\mathcal{Q}\rangle\)._

**Output**: _a family \(\mathcal{R}=\{r_{1},\ldots,r_{m}\}\) of disjoint rectilinear \(\epsilon\)-bounded hyperrectangles such that \(\bigcup_{i}r_{i}\subseteq\Gamma(\mathcal{T})\) and \(|\Gamma(\mathcal{T})\setminus\bigcup_{i}r_{i}|\) is minimum._

A _rectilinear \(\epsilon\)-bounded hyperrectangle_ is defined as the cartesian product of intervals of size at least \(\epsilon\). Moreover, for \(\epsilon>0,\) we say that a rectilinear hyperrectangle \(r=\times_{i}[\ell_{i},u_{i}]\) is \(\epsilon\)_-aligned_ if for each \(i,\) both extremes \(\ell_{i}\) and \(u_{i}\) are a multiple of \(\epsilon\).

The rational behind this new formulation of the problem is twofold: on the one hand, we are relaxing the request for the exact enumeration of safe points; on the other hand, we are requiring that the output is more concisely representable by means of hyperrectangles of _some significant_ size.

Note that for \(\epsilon\to 0\), \(\epsilon\)-_RUA-DNN_ and _AllDNN-Verification_ become the same problem. More generally, whenever the solution \(\Gamma(\mathcal{T})\) to an instance \(\mathcal{T}\) of _AllDNN-Verification_ can be partitioned into a collection of rectilinear \(\epsilon\)-bounded hyperrectangles, \(\Gamma(\mathcal{T})\) can be attained by an optimal solution for the \(\epsilon\)-_RUA-DNN_. This allows as to tackle the _AllDNN-Verification_ problem via an efficient approach with strong probabilistic approximation guarantee to solve the \(\epsilon\)-_RUA-DNN_ problem.

Our method is based on two main concepts: the analysis of an underestimated output reachable set with probabilistic guarantees and the _iterative refinement_ approach (Wang et al. 2018b). In particular, in Fig. 3 we report a schematic representation of the approach that can be set up through reachable set analysis. Let us consider a possible domain for the safety property, i.e., the polygon highlighted in light blue in the upper left corner of Fig. 3.

Suppose that the undesired output reachable set is the one highlighted in red called \(\mathcal{R}^{*}\) in the bottom left part of the image, i.e., this set describes all the unsafe outcomes the DNN should never output starting from \(\mathcal{X}\). Hence, in order to formally verify that the network respects the desired safety property, the output reachable set computed from the domain of the property (i.e., the green \(\mathcal{R}\) area of the left side of the image) should have an empty intersection with the undesired reachable set (the red one). If this condition is not respected, as, e.g., in the left part of the figure, then there

Figure 2: Explanatory image execution of exact count for a particular \(\mathcal{N}\) and safety property.
exists at least an input configuration for which the property is not respected.

To find all the portions of the property's domain where either the undesired reachable set and the output reachable set are disjoint, i.e., \(\mathcal{R}^{*}\bigcap\mathcal{R}=\emptyset\), or, dually, discover the unsafe areas where the condition \(\mathcal{R}\subseteq\mathcal{R}^{*}\) holds (as shown in the right part of Fig. 3) we can exploit the _iterative refinement_ approach [22]. However, given the nonlinear nature of DNNs, computing the exact output reachable set is infeasible. To address this issue, the reachable set is typically over-approximated, thereby ensuring the soundness of the result. Still, the relaxation of the nonlinear activation functions used to compute the over-approximated reachable set is computationally demanding.

In contrast, we propose a computationally efficient solution that uses underestimation of the reachable set and construct approximate solutions for the \(\epsilon\)-_RUA-DNN_ problem with strong probabilistic guarantees.

### Probabilistic Reachable Set

Given the complexity of computing the exact minimum and maximum of the function computed by a DNN, we propose to approximate the output reachable set using a statistical approach known as _Statistical Prediction of Tolerance Limits_[23].

We use a Monte Carlo sampling approach: for an appropriately chosen \(n\), we sample \(n\) input points and take the smallest and the greatest value achieved in the output node as the lower and the upper extreme of our probabilistic estimate of the reachable set. The choice of the sample size is based on the results of [23] that allow us to choose \(n\) in order to achieve a given desired guarantee on the probability \(\alpha\) that our estimate of the output reachable set holds for at least a fixed (chosen) fraction \(R\) of a further possibly infinitely large sample of inputs. Crucially, this statistical result is independent of the probability function that describes the distribution of values in our function of interest and thus also applies to general DNNs. Stated in terms more directly applicable to our setting, the main result of [23] is as follows.

**Lemma 1**.: _For any \(R\in(0,1)\) and integer \(n\), given a sample of \(n\) values from a (continuous) set \(X\) the probability that for at least a fraction \(R\) of the values in a further possibly infinite sequence of samples from \(X\) are all not smaller (respectively larger) than the minimum value (resp. maximum value) estimated with the first \(n\) samples is given by the \(\alpha\) satisfying the following equation_

\[n\cdot\int_{R}^{1}x^{n-1}\ dx=\alpha \tag{2}\]

### Computation of Safe Regions

We are now ready to give a detailed account of our algorithm \(\epsilon\)-ProVe.

Our approximation is based on the analysis of an under-estimated output reachable set obtained by sampling a set of \(n\) points \(P_{A}\) from a domain of interest \(A\). We start by observing that, it is possible to assume without loss of generality that the network has a single output node on whose reachable set we can verify the desired property [10]. For networks not satisfying this assumption, we can enforce it by adding one layer. For example, consider the network in the example of Fig. 4 and suppose we are interested in knowing if, for a given input configuration in a domain \(A=[0,1]\times[0,1]\), the output \(y_{1}\) is always less than \(y_{2}\). By adding a new output layer with a single node \(y^{*}\) connected to \(y_{1}\) by weight \(-1\) and to \(y_{2}\) with weight \(1\) the condition required reduces to check that all the values in the reachable set for \(y^{*}\) are positive.

In general, from the analysis of the underestimated reachable set of the output node computed as \(\mathcal{R}=[min(y_{i}),max(y_{i})]\ \forall i=1,\ldots,n\) we can obtain one of these three conditions:

\[\begin{cases}A\text{ is unsafe}&\text{upper bound of }\mathcal{R}<0\\ A\text{ is safe}&\text{lower bound of }\mathcal{R}\geq 0\\ unknown&\text{otherwise}\end{cases} \tag{3}\]

With reference to the toy example in Figure 4, assuming we sample only \(n=2\) input configurations, \((1,0)\) and \((0,1)\) which when propagated through \(\mathcal{N}\) produce as a result in the new output layer the vector \(y^{*}=[8,5]\). This results in the estimated reachable set \(\mathcal{R}=[5,8]\). Since the lower bound of this interval is positive, we conclude that the region \(A\), under consideration, is completely safe.

To confirm the correctness of our construction, we can check the partial values of the original output layer and notice that no input generates \(y_{1}\geq y_{2}\). Specifically, if all inputs

Figure 4: Example of computation single reachable set for a DNN with two outputs.

Figure 3: Explanatory image of how to exploit reachable set result for solving the _AllDNN-Verification_ problem.
result in \(y_{1}\geq y_{2}\) (violating the specification we are trying to verify), then the reachable set must have, by construction, a negative upper bound, leading to the correct conclusion that the area is unsafe. On the other hand, if only some inputs produce \(y_{1}\geq y_{2}\), then we obtain a reachable set with a negative lower bound and a positive upper bound, thus we cannot state whether the area is unsafe or not, and we should proceed with an interval refinement process. Hence, this approach allows us to obtain the situations shown to the right of Fig. 3, that is, a situation in which the reachable set is either completely positive (\(A\) safe) or completely negative (\(A\) unsafe).

We present the complete pipeline of \(\epsilon\)-ProVe in Algorithm 1. Our approach receives as input a standard tuple for the _DNN-Verification_ and creates the augmented DNN \(\mathcal{N}^{\prime}\) (line 3) following the intuitions provided above. Moreover, we initialize respectively the set of safe regions as an empty set and the unchecked regions as the entire domain of the safety specification encoded in \(\mathcal{P}\) (line 5). Inside the loop (line 6), our approximation iteratively considers one area \(A\) at the time and begins computing the reachable set, as shown above. We proceed with the analysis of the interval computed, where in case we obtain a positive reachable set, i.e., the lower bound is positive (lines 9-10), then the area under consideration is deemed as safe and stored in the set of safe regions we are enumerating. On the other hand, if the interval is negative, that is, the upper bound is negative, then we ignore the area and proceed (lines 11-12). Finally, if we are not in any of these cases, we cannot assert any conclusions about the nature of the region we are checking, and therefore we must proceed with splitting the area according to the heuristic we prefer (lines 13-14).

The loop ends when either we have checked all areas of the domain of interest, or we have reached the \(\epsilon-precision\) on the iterative refinement. In detail, given the continuous nature of the domain, it is always possible to split an interval into two subparts, that is, the process could continue indefinitely in the worst case. For this reason, as is the case of other state-of-the-art FV methods that are based on this approach, we use a parameter to decide when to stop the process. This does not affect the correctness of the output since our goal is to (tightly) underapproximate the safe regions, and thus in case the \(\epsilon-precision\) is reached, the area under consideration would not be considered in the set that the algorithm returns, thus preserving the correctness of the result. Although the level of precision can be set arbitrarily, it does have an effect on the performance of the method. In the supplementary material, we discuss the impact that different heuristics and different setting of hyper-parameters have on the resulting approximation.

### Theoretical Guarantees

In this section, we analyze the theoretical guarantees that our approach can provide. We assume that the IntervalRefinement procedure consists of iteratively choosing one of the dimensions of the input domain and splitting the area into two halves of equal size as in [22]. The theoretical guarantee easily extends to any other heuristic provided that each split produces two parts both at least a fixed constant fraction \(\beta\) of the subdivided area. Moreover, we assume that reaching the \(\epsilon\) precision is implemented as testing that the area has reached size \(\epsilon^{d}\), i.e., it is the cartesian product of \(d\) intervals of size \(\epsilon\). It follows that, by definition, the areas output by \(\epsilon\)-ProVe are \(\epsilon\)-bounded and \(\epsilon\)-aligned.

The following proposition is the basis of the approximation guarantee (in terms of the size of the safe area returned) on the solution output by \(\epsilon\)-ProVe on an instance of the \(\epsilon\)-_RUA-DNN_ problem.

**Proposition 2**.: _Fix a real number \(\epsilon>0\), an integer \(k\geq 3\), and a real \(\gamma>k\epsilon\). Let \(\mathcal{T}\) be an instance of the \(\epsilon\)-RUA-DNN problem. Then for any solution \(\mathcal{R}=\{r_{1},\ldots,r_{m}\}\) such that for each \(i=1,\ldots,m\), \(r_{i}\) is \(\gamma\)-bounded, there is a solution \(\mathcal{R}^{(\epsilon)}=\{r_{1}^{(\epsilon)},\ldots,r_{m}^{(\epsilon)}\}\) such that each \(r_{i}^{(\epsilon)}\) is \(\epsilon\)-aligned and \(||\mathcal{R}^{(\epsilon)}||\geq\left(\frac{k-2}{k}\right)^{d}||\mathcal{R}||\), where \(d\) is the number of dimensions of the input space, and for every solution \(\mathcal{R}^{\prime}\), \(||\mathcal{R}^{\prime}||=|\cup_{i}r_{i}|\) is the total area covered by the hyperrectangles in \(\mathcal{R}^{\prime}\)._

The result is obtained by applying the following lemma to each hyperrectangle of the solution \(\mathcal{R}\).

**Lemma 3**.: _Fix a real number \(\epsilon>0\) and an integer \(k\geq 3\). For any \(\gamma>k\epsilon\) and any \(\gamma\)-bounded rectilinear hyperrectangle \(r\subseteq\mathbb{R}^{d},\) there is a \(\epsilon\)-aligned rectilinear hyperrectangle \(r^{(\epsilon)}\) such that: (i) \(r^{(\epsilon)}\subseteq r\); and (ii) \(|r^{(\epsilon)}|\geq\left(\frac{k-2}{k}\right)^{d}|r|\)._

Figure 5: An Example of applying Lemma 3 with \(k=3\).
Fig. 5 gives a pictorial explanation of the lemma. In the example shown, \(k=3\) and the parameter \(\epsilon\) is the unit of the grid, which we can imagine superimposed to the bidimensional (\(d=2\)) space in which the hyperrectangles live. Hence \(\gamma=3\epsilon\). The non-\(\epsilon\)-aligned \(r_{i}\) (depicted in blue) is \(\gamma\)-bounded, since its width \(w=(b_{1}-a_{1})=4\epsilon\) and its height \(h=(b_{2}-a_{2})=3\epsilon\) are both \(\geq 3\epsilon\). Hence, it covers completely at least \(w-2\) columns and \(h-2\) rows of the grid. These rows and columns define the green \(\epsilon\)-aligned hyperrectangle \(r_{i}^{(\epsilon)},\) of dimension

\[\geq(w-2)\cdot(h-2)\geq\frac{k-2}{k}w\cdot\frac{k-2}{k}h=\left(\frac{k-2}{k} \right)^{d}|r_{i}|.\]

The following theorem summarizes the coverage approximation guarantee and the confidence guarantee on the safety nature of the areas returned by \(\epsilon\)-ProVe.

**Theorem 4**.: _Fix a positive integer \(d\) and real values \(\epsilon,\alpha,R\in(0,1),\) with \(R>1-\epsilon^{d}.\) Let \(\mathcal{T}\) be an instance of the AllDNN-Verification with input in2\([0,1]^{d},\) and let \(k\) be the largest integer such that \(\Gamma(\mathcal{T})\) can be partitioned into \(k\epsilon\)-bounded rectilinear hyperrectangle. Let \(\mathcal{R}^{(\epsilon)}=\{r_{i}^{(\epsilon)}\mid i=1,\ldots,m\}\) be the set of areas returned by \(\epsilon\)-ProVe using \(n\) samples at each iteration, with \(n\geq\log_{R}(1-\alpha^{1/m})\). Then,_

Footnote 2: This assumption is w.l.o.g. modulo some normalization.

1. _(coverage guarantee) with probability_ \(1-R^{n}\) _the solution_ \(\mathcal{R}^{(\epsilon)}\) _is a_ \(\left(\frac{k-2}{k}\right)^{d}\) _approximation of_ \(\Gamma(\mathcal{T}),\) _i.e.,_ \(||\mathcal{R}^{(\epsilon)}||\geq\left(\frac{k-2}{k}\right)^{d}|\Gamma(\mathcal{ T})|\)_;_
2. _(safety guarantee) with probability at least_ \(\alpha\)_, in each hyperrectangle_ \(r\in\mathcal{R}^{(\epsilon)}\) _at most_ \((1-R)\cdot|r|\) _points are not safe._

This theorem gives two types of guarantees on the solution returned by \(\epsilon\)-ProVe. Specifically, point 2. states that for any \(R<1\) and \(\alpha<1\), \(\epsilon\)-ProVe can guarantee that with probability \(\alpha\) no more than \((1-R)\) of the points classified as safe can, in fact, be violations. Moreover, point 1. guarantees that, provided the space of safety points is not too scattered--formalized by the existence of some representation in \(k\epsilon\)-bounded hyperrectangles-- the total area returned by \(\epsilon\)-ProVe is guaranteed to be close to the actual \(\Gamma(\mathcal{T})\).

Finally, the theorem shows that the two guarantees are attainable in an efficient way, providing a quantification of the size \(n\) of the sample needed at each iteration. Note that the value of \(m\) needed in defining \(n\) can be either estimated, e.g., by a standard doubling technique, or it could be set using the upper limit \(2^{d\log(1/\epsilon)}\), which is the maximum number of possible split operations performed before reaching the \(\epsilon\) precision limit.

Proof.: (Sketch) The safety guarantee (item 2.) is a direct consequence of Lemma 1. In fact, an hyperrectangle \(r\) is returned as safe if all the \(n\) sampled points from \(r\) are not violations, i.e., their output is \(\geq 0\) (see (3)). By Lemma 1, at most \((1-R)\) of the points in \(r\) can give an output \(<0\), i.e., can be a violation, where, from the solution of (2),

\[\hat{\alpha}=(1-R^{n}). \tag{4}\]

Since samples are chosen independently in different hyperrectangles, this bound on the number of violations in a hyperrectangle of \(\mathcal{R}^{(\epsilon)}\) holds simultaneously for all \(m\) of them with probability \(\hat{\alpha}^{m}\). Taking \(\alpha=\hat{\alpha}^{m}\), and solving (4) for \(n\) we get \(n\geq\log_{R}(1-\alpha^{1/m})\) as desired.

For the coverage guarantee, we start by noticing that under the hypotheses on \(k\), Proposition 2 guarantees the existence of a solution \(\mathcal{R}^{*}_{1}\) made of \(\epsilon\)-bounded and \(\epsilon\)-aligned rectilinear hyperrectangles. Let \(\mathcal{R}^{*}_{2}\) be a solution obtained from \(\mathcal{R}^{*}_{1}\) by partitioning each hyperrectangle into pieces of minimum possible size \(\epsilon^{d}\), each one \(\epsilon\)-aligned.

The first observation is that, being the solution produced by \(\epsilon\)-ProVe made of \(\epsilon\)-bounded and \(\epsilon\)-aligned rectilinear hyperrectangles, also \(\mathcal{R}^{*}_{2}\) is among the solutions possibly returned by the algorithm.

We now observe that with probability \(1-R^{n}\) each hyperrectangle \(r^{\prime}\) in \(\mathcal{R}^{*}_{2}\) must be contained in some hyperrectangle \(r\) in the solution \(\mathcal{R}^{(\epsilon)}\) returned by \(\epsilon\)-ProVe.

First note that if in the iterations of the execution of \(\epsilon\)-ProVe, \(r^{\prime}\) keeps on being contained in an area where both safe and violation points are sampled, then eventually \(r^{\prime}\) will become itself an area to analyze. At such a step, clearly every sample in \(r^{\prime}\) will be safe and \(r^{\prime}\) will be included in \(\mathcal{R}^{(\epsilon)},\) as desired.

Therefore, the only possibility for \(r^{\prime}\) not to be contained in any \(r\in\mathcal{R}^{(\epsilon)}\) is that at some iteration an area \(A\supseteq r^{\prime}\) is analyzed and all the \(n\) points sampled in \(A\) are violation points, so that the whole \(A\) (including \(r^{\prime}\)) is discarded (as unsafe) by \(\epsilon\)-ProVe. However, by Lemma 1 with probability \((1-R^{n})\) this can happen only if \(\epsilon^{d}=|r^{\prime}|<(1-R)|A|,\) which contradicts the hypotheses. Hence, with probability \((1-R^{n})\), the \(r^{\prime}\) must be contained in a hyperrectangle of \(\mathcal{R}^{(\epsilon)}\), concluding the argument. 

Fig. 6 (left) shows the correlation between the number of points to be sampled based on the number of areas obtained by \(\epsilon\)-ProVe if we want to obtain a total confidence of \(\alpha=99.9\%\) and a lower bound \(R=99.5\%\). As we can notice from the plot, if we compute our output reachable set sampling \(n=3250\) points, we are able to obtain the desired confidence and lower bound if the number of regions is in \([1,10000]\). For this reason, in all our empirical evaluations, we use \(n=3500\) to compute \(\mathcal{R}\). An explanatory example of

Figure 6: Left: Correlation point to sample and # of (un)safe areas using \(\epsilon\)-ProVe to obtain a confidence \(\alpha=99.9\%\) and a lower bound \(R=99.5\%\). Right: example of a set of safe regions (in green) returned by \(\epsilon\)-ProVe (scaled x100).
the possible result achievable using our approach is depicted in Fig. 6 (right).

## Empirical Evaluation

In this section, we evaluate the scalability of our approach, and we validate the theoretical guarantees discussed in the previous section. Our analysis considers both simple DNNs to analyze in detail the theoretical guarantees and two real-world scenarios to evaluate scalability. The first scenario is the ACAS xu [16], an airborne collision avoidance system for aircraft, which is a well-known standard benchmark for formal verification of DNNs [16, 17, 18]. The second scenario considers DNN trained and employed for autonomous mapless navigation tasks in a Deep Reinforcement Learning (DRL) context [16, 15, 14].

All the data are collected on a commercial PC equipped with an M2 Apple silicon. The code used to collect the results and several additional experiments and discussions on the impact of different heuristics for our approximation are available in the supplementary material.

### Correctness and Scalability Experiments

These experiments aim to estimate the correctness and scalability of our approach. Specifically for each model tested, we used \(\epsilon\)-ProVe to return the set of safe regions in the domain of the property under consideration3. All data are collected with parameters \(\alpha_{TOT}=99.9\%\) and \(R=99.5\%\) and \(n=3500\) points to compute the reachable set used for the analysis. The results are presented in Table 1. For all experiments, we report the number of safe regions returned by \(\epsilon\)-ProVe (for which we also know the hyperrectangles position in the property domain), the percentage of safe areas relative to the total starting area (i.e., the safe rate), and the computation time. Moreover, we include a comparison, measured as percentage distance, of the safe rate computed with alternative methods, such as an exact enumeration method (whenever feasible due to the scalability issue discussed above) and a Monte Carlo (MC) Sampling approach using a large number of samples (i.e., 1 million). It's important to note that the MC sampling only provides a probabilistic estimate of the safe rate, lacking information about the location of safe regions in the input domain.

Footnote 3: we recall that similarly can be done with the set of unsafe areas

The first block of Table 1 involves two-dimensional models with two hidden layers of 32 nodes activated with ReLU. The safety property consists of all the intervals of \(\mathcal{P}\) in the range \([0,1]\) and a postcondition \(\mathcal{Q}\) that encodes a strictly positive output. Notably, \(\epsilon\)-ProVe is able to return the set of safe regions in a fraction of a second, and the safe rate returned by our approximation deviates at most a \(1.75\%\) from the one computed by an exact count, which shows the tightness of the bound returned by our approach. In the second block of Tab. 1, the Mapless Navigation (MN) DNNs are composed of 22 inputs, two hidden layers of 64 nodes activated with \(ReLU\), and finally, an output space composed of five nodes, which encode the possible actions of the robot. We test a behavioral safety property where \(\mathcal{P}\) encodes a potentially unsafe situation (e.g., _there is an obstacle in front_), and the postcondition \(\mathcal{Q}\) specifies the unsafe action that should not be selected (\(\bigvee_{i=2,3}y_{1}<y_{i}\) if \(y_{1}\) encodes a forward movement). The table illustrates how increasing input space and complexity affects computation time. Nevertheless, the proposed approximation remains efficient even for ACAS xu tests, returning results within seconds. Crucially, focusing on \(Model\_MN\_2\) and \(\phi_{2}\) ACAS Xu_3.3, \(\epsilon\)-ProVe states that all the property's domain is safe (i.e., no violation points). The correctness of the results was verified by employing VeriNet [1], a state-of-the-art FV tool.

## Discussion

We studied the _AllDNN-Verification_, a novel problem in the area of FV of DNNs asking for the set of all the safe regions for a given safety property. Due to the #P-hardness of the problem, we proposed an approximation approach, \(\epsilon\)-ProVe, which is, to the best of our knowledge, the first method able to efficiently approximate the safe regions with some guarantees on the tightness of the solution returned. We believe \(\epsilon\)-ProVe is an important step to provide consistent and effective tools for analyzing safety in DNNs.

An interesting future direction could be testing the enumeration of the unsafe regions for subsequent patching or a safe retrain on the areas discovered by our approach.

\begin{table}
\begin{tabular}{|c||c c c||c c||c|} \hline
**Instance** & \multicolumn{2}{c||}{\(\epsilon\)**-ProVe** (\(\alpha_{TOT}=99.9\%\))} & \multicolumn{2}{c||}{**Exact count** or _MC sampling_} & \multicolumn{2}{c||}{**Und-estimation (\% distance)**} \\  & \# Safe regions & Safe rate & Time & Safe rate & Time & \\ \hline Model\_2\_20 & 335 & 78.50\% & 0.4s & 79.1\% & 234min & 0.74\% \\ Model\_2\_56 & 251 & 43.69\% & 0.3s & 44.46\% & 196min & 1.75\% \\ \hline Model\_MN\_1 & 545 & 64.72\% & 60.6s & _67.59\%_ & _0.6s_ & 4.24\% \\ Model\_MN\_2 & 1 & 100\% & 0.4s & _100\%_ & _0.4s_ & - \\ \hline \(\phi_{2}\) ACAS Xu\_2\_1 & 2462 & 97.47\% & 26.9s & 99.25\% & _0.6s_ & 1.81\% \\ \(\phi_{2}\) ACAS Xu\_3.3 & 1 & 100\% & 0.4s & _100\%_ & _0.5s_ & - \\ \hline \end{tabular}
\end{table}
Table 1: Comparison of \(\epsilon\)–ProVe and Exact count or Monte Carlo (MC) sampling approach on different benchmark setups. Full results and other different experiments are reported in the supplementary material.