Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound

We thank reviewer SiXd for their review.

Q3. Closed-form inference.

By "closed-form", we wanted to express that a terminating algorithm exists for computing a probability exactly, not necessarily that this algorithm has polynomial runtime. We will state this more clearly in our paper. For example, we use a Bayesian Network (BN) in our MiniACSIncome experiment, for which exact inference is NP-complete, as you also pointed out. For practical applicability, the assumption is that computing the probability of a hyperrectangle should be significantly faster than solving the overall verification problem. This is the case for our BN (inference is NP-complete) and the MiniACSIncome probabilistic verification problem (#P-hard).

Q4. Expressiveness of the supported family of distributions.

Yes, we are able to encode complex, multimodal distributions! For example, consider Figures 7 and 8 in our Appendix, which visualise the BN of our MiniACSIncome benchmark. Figure 7 shows that this distribution is multimodal. For example, the marginal distributions of "SCHL" and "AGEP" marginal distribution have several peaks. Regarding complexity, these figures also show that our BN is a reasonably good fit of real-world US census data (ACSIncome). Therefore, we believe that our MiniACSIncome experiment demonstrates that our approach is applicable to complex, multimodal distributions.

Multivariate normal distributions paragraph.

We will clarify this paragraph in the updated version of the paper. The key point here is that while general multivariate normal distributions do not admit a closed-form solution, standard multivariate normal distributions (or, more generally, multivariate normal distributions with diagonal covariance matrices) do admit a closed-form solution. Or idea is to emulate a general multivariate normal distribution through a standard multivariate normal distribution and an additional linear layer in the network we want to verify. By doing this, we can apply PV to a (general) multivariate normal distribution, although we can not use this multivariate normal distribution as an input distribution for PV directly.

Q2. How does PV compare with [1]?

We would like to point out that [1] does not provide sound coverage ratios for MNIST. The coverage ratios they report are sampling approximations. While [1] also provides sound results in the "Quantitative Verification" section, these results are for 2d and 3d input spaces. Due to the unsoundness of the MNIST results, a comparison with our approach on this case study would be unfair, but we performed a comparison with [1] on the VCAS quantitative verification case study. Our PV algorithm is faster than the algorithm from [1] by two orders of magnitude for this case study.

Both results were obtained on the hardware also used in our paper (HW1). The code for running both tools is available at https://drive.google.com/drive/folders/1KBbBwzxLvCXeufo24A-cZhuvwhGTB2MD?usp=sharing.

ReLU Splitting

The problem with ReLU splitting for probabilistic verification is that it creates branches that are non-convex in the input space. The approach of [1] to underapproximate these branches using linear relaxations is interesting. However, these underapproximations are still polytopes and computing the volume of a high-dimensional polytope is very costly. The approach in [1] to use Monte Carlo estimates of such volumes is enticing, but it entails unsoundness.

Main criticism: only low-dimensional settings.

Earlier works that consider non-uniform probability distributions (FairSquare and SpaceScanner) only scale to 2d input spaces. Although uniform input distributions significantly simplify verification, [1] and Marzari et al. (ProVe_SLR) only demonstrate sound #DNN-verification for up to 3 and 5 input dimensions, respectively. In light of this, our ability to handle 7 input variables while not assuming uniform input distributions is a major step forward. We would also like to point out that the actual input dimension of MiniACSIncome-7 is 67 (Table 7 in our Appendix).

Q1. Large networks for low-dim settings.

ACAS Xu (Julian et al., 2018) is a good example of a low-dimensional application requiring a medium-sized neural network (> 1000 parameters). Other examples are the neural network controllers in [1].

Satisfaction functions (Eq. 3)

We agree that Equation (3) is somewhat intricate. This is because of the generality of our algorithm. The satisfaction functions encapsulate, for example, the fraction in Equation (1). The full satisfaction function for Equation (1) is given in Example A.1. Our $f_{Sat}$ function roughly corresponds to the formulae $\varphi_{\mathrm{post}}$ of Albarghouthi et al. (2017) and $\Gamma$ of Morrettin et al. (2024).

We thank reviewer 8dyc for their review. We address the questions posed in the review below.

1. The updating strategy for upper and lower bounds based on probabilistics need more clearification. Why we can directly use the probabilistic to refine the interval?

We assume that this question refers to Lines 7 and 8 of Algorithm 2. Please clarify in case the question is referring to a different part of our paper. We can add the probability of $\mathcal{X}\_{\mathrm{Sat}}^{(t)}$ to the lower bound, since we know that $g\_{\mathrm{Sat}}(\mathbf{x}, \mathrm{net}(\mathbf{x}) \geq 0$ for $x \in \mathcal{X}\_{\mathrm{Sat}}^{(t)}$. This is, in turn, due to the soundness of ComputeBounds (concretely, CROWN or interval arithmetic in our paper). We can compute $\mathbb{P}[\mathcal{X}\_{\mathrm{Sat}}^{(t)}]$ directly, since $\mathcal{X}\_{\mathrm{Sat}}^{(t)}$ is a union of disjoint hyperrectangles. Because of this, we can leverage the third axiom of probabilities (i.e. the probability of a countable union of disjoint sets is the sum of the probabilities of these sets). The probability of each hyperrectangle can be computed exactly due to our assumptions on the probability distributions that are described in Section 4.2.

2. The branch-and-bound and interval propagation methods are widely used in neural network verification tools, and their properties have been explored a lot. This paper seems like merging them together, lacking of new insights.

Branch and bound and bound propagation are indeed widely used for deterministic neural network verification. However, this is not yet the case for verifying probabilistic specifications for neural networks. We use these tools and apply them to a new problem (solving probabilistic neural network verification problems). In this context, our paper provides the following new insights:

1. We apply branch and bound (BaB) and bound propagation (BP) for solving probabilistic neural network verification problems, a class of problems to which these techniques have not yet been applied to.
2. We conduct a thorough theoretical analysis of our BaB and BP-based approach. To the best of our knowledge, there are no previous results on the theoretical properties of BaB and BP for probabilistic verification problems.
3. Our experiments demonstrate that our proposed approach (based on BaB and BP) provides a substantial runtime advantage for solving probabilistic verification problems. The magnitude of this runtime advantage is a surprising novel insight.

3. As previous listed, the paper experiment needs more ellaboration. I do not understand the experiment setting of table 2. What is the meaning of the percentages in neural network verifications? Why not use the same setting for the baselines?

The percentages in Table 2 are probabilities given as percentages. We will clarify this in the table caption. The "VR" percentages in this table are the exact probabilities, that is, the verification result of quantitative verification. The probabilities for ProbabilityBounds are pairs of lower and upper bounds on these values. The percentages for $\varepsilon$-ProVe are 99.9% confidence upper bounds on these values. Overall, these percentages are results, not settings of the verifiers.

If the remark regarding using the same settings for the baselines refers to the timeout for ProbabilityBounds (10s, 1m, 1h): these settings are not applicable for ProVe_SLR and $\varepsilon$-ProVe, since these algorithms do not provide intermediate sound results. This is one of the advantages of ProbabilityBounds that we seek to demonstrate in Table 2.

[Weakness:] Lack of comparisons of non-probabilistic verification tools.

Since non-probabilistic verifiers can not be applied to probabilistic verification problems, it is not possible to compare our approach to them experimentally. For example, it is impossible to apply $\alpha$-$\beta$-CROWN to the FairSquare benchmark, since $\alpha$-$\beta$-CROWN can not handle probabilities.

To position our work more clearly in the context of other verification approaches, we provide the following table:

The rebuttal for reviewer BFqm includes an extended version of this table that we will add to our related work section. We hope that this clarifies the relation between our approach and non-probabilistic verifiers. If there remain further questions, we would be happy to address them in the second round of the author-reviewer discussion.

We thank reviewer GWj1 for their review, in particular their careful evaluation of our theoretical assumptions.

Theoretical Claims / Assumption 5.3

If the safe/unsafe region is not axis-aligned, indeed, Algorithm 2 can not compute the exact probability of safety. However, Algorithm 2 still computes a converging sequence of bounds on the unknown exact probability $p_i$. The question that motivates Assumption 5.3 is when converging bounds are sufficient for solving a probabilistic verification problem.

For illustration, assume we want to show $y \geq 0$ and have converging sequences of bounds ${(\ell\_t)}\_{t \in \mathbb{N}}$ and ${(u\_t)}\_{t \in \mathbb{N}}$ with $\ell_t \leq y \leq u_t$ for each $t \in \mathbb{N}$ and $\lim_{t \to \infty} \ell_t = \lim_{t \to \infty} u_t = y$. If the actual (exact) $y$ is zero, sequences of bounds that only converge in the limit do not suffice to prove $y \geq 0$, since there may be no $T \in \mathbb{N}$ with $\ell_T = 0$. However, if the actual value of $y$ is different from zero, knowing a finite number of iterates of ${(\ell_t)}\_{t}$ and ${(u_t)}\_{t}$ always suffices to prove or disprove $y \geq 0$. Concretely, there will be a $T \in \mathbb{N}$, such that either $\ell_T > 0$ or $u_T < 0$, that proves, respectively, disproves $y \geq 0$.

Unfortunately, the situation does not change fundamentally if we study $y > 0$ instead of $y \geq 0$. Before, if $y = 0$, our specification actually held, but we were not able to ever prove this. Now, our specification $y > 0$ is actually violated if $y = 0$, but we will never be able to disprove it. Concretely, if ${(u_t)}_{t}$ only converges in the limit, there may be no $T \in \mathbb{N}$, such that $u_T = 0$.

Our assumption that $f\_{Sat}(p_1, \ldots, p_v) \neq 0$ corresponds to assuming $y \neq 0$ in the discussion above. Note that $f\_{Sat}(p_1, \ldots, p_v)$ is a constant in Equation (3).
Our comment on studying $f\_{Sat}(...) \geq \varepsilon$ instead of $f\_{Sat}(...) \geq 0$ means solving a different verification problem with $f'\_{Sat}(...) = f\_{Sat}(...) - \varepsilon$. Practically, if you only want to show Equation (1) and PV seems not to be terminating for $\gamma = 0.8$, you can run PV again with $\gamma' = 0.81$ and find that your neural network either violates or satisfies a slightly stronger fairness specification.

The motivation for requiring $p = \mathbb{P}[g\_{Sat}(...) = 0] = 0$ is similar. However, the reason why it is not restrictive to assume $p = 0$ is different. Unlike $f\_{Sat}(...)$, $g\_{Sat}(...)$ is not a constant in Equation (3). Here, our argumentation why the assumption that $p = 0$ is not restrictive is concerned with the level sets $G\_r = \\{\mathbf{x} \in \mathbb{R}^n \mid g\_{Sat}(\mathbf{x}, \mathrm{net}(\mathbf{x})) = r\\}$ of $g$ that have positive probability ($\mathbb{P}[G\_r] > 0$). If $\mathbb{P}[G\_r] > 0$ for some $r$, $G\_r$ also needs to have positive volume in $\mathbb{R}^n$ (we assume a continuous probability distribution here; for discrete distributions we actually do not require the assumption p = 0 due to splitting differently). A set $G\_r$ having positive volume means that the plot of $g\_{Sat}(...)$ has a "flat" part where $g\_{Sat}(...) = r$. Unless $g\_{Sat}$ has a continuous range of "flat parts", we can find a small $\varepsilon > 0$, such that $\mathbb{P}[g\_{Sat}(...) = \varepsilon] = 0$. While there may be pathological functions that have continuous ranges of "flat parts", neural networks with finitely many neurons with standard activation functions can not have such continuous ranges.

We hope this discussion clarifies our assumption and why we consider it only mildly restrictive. We will use your feedback and the above discussion to improve the description of Assumption 5.3 in our paper.

Unbounded Input Spaces (Q2)

Indeed, qualitative verifiers rarely support unbounded input spaces. In practice, we use $\underline{\mathbf{y}} = -\infty$ and $\underline{\mathbf{y}} = \infty$ for unbounded branches in line 5 of Algorithm 2. With this, unbounded branches are never pruned, and LongestEdge always first selects dimensions that are unbounded in a branch. We modify BaBSB to also first select dimensions that are unbounded in a branch. Unfortunately, this was not documented in our submission, but we will add this to the last paragraph in Section 4.1.

The FairSquare benchmark (Section 6.1) features an unbounded input space (discussed in Appendix F.2.1).

Related Work: Individual Fairness (Kim et al.)

Besides what was already noted by the reviewer, Kim et al. study individual fairness, which is a non-probabilistic fairness specification. Therefore, the work of Kim et al. is more closely related to the papers of Marzari et al. (2023a, 2023b, 2024), than to our approach. Nonetheless, this paper is important related work and we will incorporate it into our discussion of #DNN-verification in Section 2.

We thank reviewer BFqm for their review. We believe there has been a misunderstanding of our definition of soundness that underlies most of the review.

The definitions of soundness [...] in this paper seem to be quite different from the commonly used ones in the neural network verification community [...]. In this sense, probabilistic verification seems to be a false proposition.

We actually use the standard definition of soundness, as expressed by Definition 3.2 in our paper. The review appears to assume that we provide what we call a "probably sound" algorithm, for which a verifier output of true means that the output specification likely holds, typically with a certain confidence level (PAC-style guarantee). We instead provide a definite guarantee for a probabilistic statement.

We agree that the term "probabilistic verification" can be misleading. Therefore, we propose to change the title of our paper to "Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound" and similarly modify our abstract and introduction to avoid this source of confusion. If there are further suggestions where our presentation can be improved in this regard, we would be happy to incorporate them.

To summarise, our paper provides a sound algorithm for solving probabilistic verification problems (PVPs), that is, proving statements involving probabilities over neural networks, such as fairness statements of the type of Equation (1). Other methods, like hypothesis testing, provide PAC-style guarantees for PVPs that only hold with a certain probability. Unlike these methods, our guarantees hold with certainty.

In Eq(3), I wonder whether each support of $P_{x^{(i)}}$ is assumed to be not overlapped.
The proof of Theorem 5.1 seems to hold with the assumption of uniform distribution and disjoint support of each single-value distribution.

We do not require these assumptions. Our assumptions are summarized in Section 4.2 If you have concerns regarding particular steps of the proofs (Appendix C), we would be happy to discuss them in the second round of the author-reviewer discussions.

In Alg 1, it is not clear if $PB_i$ is also related to $t$ on Line 5

In Algorithm 1, $PB_i$ is not dependent on $t$. However, $PB_i$ is an instantiation of Algorithm 2 rather than a fixed value. Note that Algorithm 2 also has a loop counter $t$. While some $PB_i$ may advance faster than others in our implementation, the counters $t$ in Algorithms 1 and 2 are synchronized in our paper to simplify the exposition.

In Alg 2, Line 7 and Line 8 [...] conflicted with [...] Line 220.

Our approach is not based on the union bound but rather on the third axiom of probabilities (the probability of a countable union of disjoint sets is the sum of the probabilities of these sets). The third axiom of probabilities holds with equality.

Adversarial machine learning.

We consider adversarial machine learning tasks in our ACAS Xu robustness experiment. Unlike probably sound verifiers, sound verifiers for PVPs (such as PV) do not currently scale to image datasets, but our work provides major advances in scaling to larger input spaces. We discuss this in more depth in the rebuttal to reviewer SiXd.

[...] some important baselines are missing, e.g.[...] $\alpha$-$\beta$-CROWN, NNV, etc.

Since non-probabilistic verifiers can not be applied to PVPs, it is not possible to compare our approach to these verifiers experimentally. For example, it is impossible to apply $\alpha$-$\beta$-CROWN to MiniACSIncome, since $\alpha$-$\beta$-CROWN can not handle probabilities.

To position our work more clearly in the context of other verification approaches, we will add the following table to our related work section:

We hope that this clarifies the relation between our method (PV) and other verifiers solving deterministic (non-probabilistic) verification tasks, as well as other methods mentioned in the review.

key [...] literature is missing.

Thank you for mentioning this. We will add the mentioned references to our discussion of probably sound approaches in Section 2 (third paragraph).