Abstract

In this work we present a rigorous theoretical framework to a foundational problem of AI safety, namely adversarial robustness. In particular, we show that the adversarial robustness problem can be reduced to a lattice traversal problem. Each element of this lattice corresponds to an interval, i.e., an axis-aligned hyper-rectangle, containing an input point $\mathbf{x}$. Consider a multilayered perceptron classifier (MLP). An interval $I$ constitutes a sound certification if $\mathbf{x} \in I$ and $\mathbf{x}$ can be freely perturbed in $I$ without changing the MLP’s prediction. Complementarily, an interval $I$ constitutes a complete certification if $\mathbf{x} \in I$ and when $\mathbf{x}$ moves outside of $I$ the MLP’s prediction is guaranteed to change. While the sound certification problem corresponds to the well-studied adversarial robustness, complete certifications have not been examined in the literature. We develop lattice traversal operators, which we apply in a refine & verify iterative scheme. Using formal MLP verifiers, sound maximality and complete minimality are guaranteed. Moreover, we examine objective optimization problems. There we discover some interesting asymmetries. For complete certifications, the minimum solution is obtained in polynomial oracle calls. This does not hold for sound certifications, where we prove strong intractability results. Additionally, we examine optimization problems in symmetric intervals (i.e., $\ell_\infty$-spheres), where we provide logarithmic algorithms. Finally, we present an empirical evaluation, using the novel ParallelepipedoNN¹ system.

1 Introduction↩︎

Artificial Intelligence, mostly driven by deep neural networks (NN), is rapidly becoming part of our everyday life, from recommendation systems in media platforms [1] to large language models chat-bots [2]. Despite these achievements, NNs promise even greater accomplishments by replacing humans in critical, decision-making areas, from driving [3] to healthcare [4] or government administration [5]. However, NNs are brittle, meaning that small, often imperceptible input perturbations can flip their predictions. These inputs are commonly referred to as adversarial examples [6]–[8].

Ensuring a NN’s robustness to adversarial attacks remains a persisting problem for AI safety. The first works on the field focused on exploiting the gradient information to produce adversarial examples, subsequently incorporating them into the learning process, e.g., [6], [9]. Nevertheless, these initial attempts fail to solve the problem in its generality [10]. More sophisticated methods utilized the convex relaxation of a NN [11], reducing adversarial robustness to a convex optimization problem. This problem was either solved directly [12]–[14], or in its dual form [15]. Even so, this family of works suffers from low precision, since they rely on a relaxation of the original problem [16], [17].

The hardness of adversarial robustness stems from the NN representation and seems to be deeply rooted in its computational properties. NN’s activation functions introduce nonlinearities that can only be studied using integer constraints. Therefore, NN can only be accurately described as mixed integer linear programs (MILPs) [18]. The MILP description of a NN made it possible to construct sound and complete NN verifiers (e.g., Marabou [19], [20]), improving upon earlier Satisfiability Modulo Theory (SMT) techniques, e.g., Reluplex [21]. Formal NN Verifiers prove if $\sigma(X) = Y$, for a pair of I/O-sets $X, Y$, and a given NN $\sigma(\cdot)$. If the property does not hold, they provide a counterexample, namely some $\mathbf{x} \in X$, s.t. $\sigma(\mathbf{x}) \notin Y$. However, this precision comes at a cost. Verifying a property on NN is NP-hard [21]. Moreover, verifying that a given area is free of adversarial examples does not admit an approximate algorithm [22].

This work aspires to provide a detailed formal analysis on robustness certification. Our work differs from previous attempts [12]–[15] in considering the underlying problem in its generality. We consider the family of interval certifications, i.e., axis-aligned hyper-rectangles, containing a given input $\mathbf{x}$. To our knowledge, this is the most general family of certification considered in the literature [12], [13]. Utilizing Sunaga’s Interval Algebra [23], we show that the space of interval certifications is organized as an innumerable, complete lattice. We introduce a set of lattice traversal operators that enable systematic exploration of this space. These operators are then applied to refine-and-verify iterative schemes for computing maximally sound and minimally complete interval certifications. An interval $I$ constitutes sound certification, if $\mathbf{x} \in I$ and $\mathbf{x}$ can vary arbitrarily within $I$ without changing model’s prediction. Dually, $I$ is a complete certification, if $\mathbf{x} \in I$ and any movement of $\mathbf{x}$ outside $I$ is guaranteed to change the prediction. Minimality and maximality are defined, w.r.t. set inclusion. Existing approaches [12]–[15] compute sound certifications, without guaranteeing maximality. Moreover, complete certifications have not, to the best of our knowledge, been considered in the literature.

Further we examine optimization problems over interval certifications, focusing on the minimum edge length objective, which is widely used in prior work [13]–[15]. In contrast to existing methods, our approach provides non-triviality guarantees for our certifications. Namely, our algorithms can decide if a non-trivial solution exists to a given optimization problem, under certain assumptions. This core functionality is lacking in existing methods, due to their reliance on relaxation. We provide a qualitative comparison between existing work and ours in Tbl. ¿tbl:tab:compare?. Finally, we strengthen known intractability results, showing that computing optimal sound interval certifications cannot be achieved in polynomial time, w.r.t. the input dimension, the number of verification calls, and the time of each verification call.

width=

Outline. In Sec. 2, we introduce the necessary preliminaries. Sec. 3 develops the interval algebra required for our analysis, while Sec. 4 explores the structure of the space of interval certifications. In Sec. 5 we review optimization problems. Finally, Sec. 6 presents the ParallelepipedoNN system and discusses the practical implications of our work.

2 Preliminaries↩︎

In this section, we review some elementary notions and definitions that will be needed in the rest of this work. For any natural number $d \in \mathbb{N}$, we denote with $[d]$ the set $\{1, 2, \dots, d\}$. Vectors will be denoted by bold, e.g., $\mathbf{x}$, while scalar values by light, e.g., $x$. For a $d$-dimensional vector $\mathbf{x}$ we denote with $x_i$ its $i$-th coordinate. Moreover, let $f\colon \mathbb{R} \to \mathbb{R}$ be a real function that takes as input some $x \in \mathbb{R}$. For a vector input $\mathbf{x} \in \mathbb{R}^d$, we denote with $\mathbf{f}(\mathbf{x}) \in \mathbb{R}^d$ the vector function induced by $f$, i.e., $\mathbf{f}(\mathbf{x}) = (f(x_1), \dots, f(x_d))$. The $d$-dimensional vectors $\mathbf{0}$ and $\mathbf{1}$ denote the zero and the all-ones vectors. For each $i \in [d]$, we denote with $\mathbf{e}^i$ a vector, s.t. $e^i_j = 0$, when $i \neq j$, and $e^i_i = 1$. Finally, matrices $A \in \mathbb{R}^{d_1 \times d_2}$ are denoted with capital letters.

2.0.0.1 Normed Vector Spaces.

In this work, we are interested in $d$-dimensional normed vector spaces on the real field $\mathbb{R}$. We will use $\ell_p$-norms, denoted $\|\mathbf{x}\|_p$ and defined as $\|\mathbf{x}\|_p = \sqrt[p]{\sum_{i \in [d]} \vert x_i \vert^p}$. In the limit $p \to \infty$ this reduces to the infinity norm $\|\mathbf{x}\|_\infty = \max_{i \in [d]} \vert x_i \vert$.

With $\mathcal{B}^p(\mathbf{x}^\star, \rho) \subset \mathbb{R}^d, \rho > 0$ we denote the $d$-dimensional sphere around $\mathbf{x}$ with radius $\rho$ w.r.t.the $\|\cdot\|_p$ norm, i.e., $\mathcal{B}^p(\mathbf{x}^\star, \rho) = \{\mathbf{x} \in \mathbb{R}^d \mid \|\mathbf{x} - \mathbf{x}^\star\|_p \leq \rho\}$. Consider a set $S \subseteq \mathbb{R}^d$. With $\partial S$ we denote the boundary of $S$ w.r.t.the measure $\|\cdot\|_p$, i.e., $\partial S = \{\mathbf{x} \in S \mid \forall \rho > 0,~~ \mathcal{B}^p(\mathbf{x}, \rho) \cap (\mathbb{R}^d \setminus S) \neq \emptyset\}$. The interior of $S$, denoted by $S^\circ$, is composed of the points of $S$ not belonging to the boundary, i.e., $S^\circ = S \setminus \partial S$. A set $S \subseteq \mathbb{R}^d$ is open w.r.t.the measure $\|\cdot\|_p$ if for every $\mathbf{x} \in S$, there is a $\rho > 0$ such that $\mathcal{B}^p(\mathbf{x}, \rho) \subseteq S$. A set $S \subseteq \mathbb{R}^d$ is closed if $\mathbb{R}^d \setminus S$ is open. A set $S \subseteq \mathbb{R}^d$ is called bounded if there is some finite $\rho > 0$ s.t.$\mathcal{B}^{\infty}(\mathbf{0}, \rho) \supseteq S$. Finally, a closed and bounded set is compact.

2.0.0.2 Multilayered Perceptrons.

A MLP is a function $\sigma\colon \mathbb{F} \to \mathbb{S}$, with $\mathbb{F} \subset \mathbb{R}^{{d_{\text{in}}}}$, $\mathbb{S} \subset \mathbb{R}^{d_{\text{out}}}$ denoting the features (input) and scores (output) spaces, respectively. We focus on MLPs, with rectified linear units (ReLU) [24] as activation functions. For $x \in \mathbb{R}$ the ReLU function $r(x)$ is given as $r(x) = \max(0, x)$. In higher dimensions, we have $\mathbf{r}(\mathbf{x}) = (r(x_1), \dots, r(x_d))$. We give the following formal definition.

Definition 1 (Multilayered Perceptron). A multilayered perceptron $\sigma \colon \mathbb{F} \to \mathbb{S}$, with $\mathbb{F} \subset \mathbb{R}^{{d_{\text{in}}}}, \mathbb{S} \subset \mathbb{R}^{d_{\text{out}}}$. is described as the tuple $\sigma = \langle L, D, W, Q \rangle$. With $L \in \mathbb{N}$, we denote the number of layers. With $D$, we denote a sequence of $L + 1$ natural numbers, where ${d_{\text{in}}}= d_0, d_1, \dots, d_{L-1}, d_L = d_{\text{out}}$. With $W$, we denote a sequence of $L$ real matrices, s.t. $W^{(i)} \in \mathbb{R}^{d_i \times d_{i-1}}$, for each $i \in [L]$. Finally, with $Q$ we denote a sequence of $L$ real vectors, s.t. $\mathbf{q}^{(i)} \in \mathbb{R}^{d_i}$, for each $i \in [L]$. For an input $\mathbf{x} \in \mathbb{F}$, the value of $\sigma(\mathbf{x})$ is given as the value $\sigma^{(L)}$ in the system of recursive equations below. \[\label{eq:mlp} \left. \begin{array}{ll} \sigma^{(0)} &= \mathbf{x} \\ \sigma^{(i)} &= \mathbf{r}[W^{(i)}\sigma^{(i-1)} + \mathbf{q}^{(i)}],\quad \forall i \in [L] \end{array} \right\}\qquad{(1)}\]

For classification problems, let $\mathcal{C} \subset \mathbb{N}$ be a finite set of classes, with $\vert \mathcal{C} \vert = d_{\text{out}}$. A classifier $\kappa \colon \mathbb{F} \to \mathcal{C}$ is constructed, with respect to the MLP $\sigma(\cdot)$, as $\kappa(\mathbf{x}) = \arg \max_{i \in [d_{\text{out}}]} \sigma_i(\mathbf{x})$. For a class $c \in \mathcal{C}$, we denote with $\mathcal{D}_c$ the decision surface of the class $c$. Namely, $\mathcal{D}_c$ is the pre-image of $\kappa(c)$; consisting of all the inputs in $\mathbb{F}$ that are classified to $c$, by $\kappa(\cdot)$.

2.0.0.3 Formal MLP Verification.

The MLP of Def. 1 can be expressed as a set of linear inequalities, with real and integer variables. This formalization is known in the literature as Mixed Integer Linear Programming (MILP). \[\label{eq:milp} \left. \begin{array}{l l l} \multicolumn{2}{l}{\widehat{\mathbf{z}}^{(0)} = \mathbf{x}, ~\mathbf{y} = \widehat{\mathbf{z}}^{(L)}}\\ \mathbf{z}^{(i)} &= W^{(i)}\widehat{\mathbf{z}}^{(i-1)} + \mathbf{q}^{(i)}, &\forall i \in [L]\\ \multicolumn{2}{l}{\widehat{\mathbf{z}}^{(i)} \geq \mathbf{z}^{(i)}, ~\widehat{\mathbf{z}}^{(i)} \geq \mathbf{0},} &\forall i \in [L]\\ \widehat{\mathbf{z}}^{(i)} &\leq \mathbf{z}^{(i)} + M\mathbf{t}^{(i)}, &\forall i \in [L]\\ \widehat{\mathbf{z}}^{(i)} & \leq M(\mathbf{1} - \mathbf{t}^{(i)}), &\forall i \in [L]\\ \\ \multicolumn{2}{l}{\mathbf{x} \in \mathbb{R}^{d_\text{in}}, ~\mathbf{y} \in \mathbb{R}^{d_\text{out}}}\\ \multicolumn{2}{l}{\mathbf{t}^{(i)} \in \{0, 1\}^{d^i_\text{out}}, ~\mathbf{z}^{(i)} \in \mathbb{R}^{d^i_\text{out}}} &\forall i \in [L]\\ \end{array} \right\}\tag{1}\] In eq. 1 , we denote with $\mathbf{z}$ the value of the neuron before the ReLU activation, while with $\widehat{\mathbf{z}}$ the value of the neuron after the activation is applied. We use the constant $M$² representing a high value, practically treated as infinity. The variables $\mathbf{t}$ model ReLU’s behaviour. For the $j$-th neuron of the $i$-th layer, $t^{(i+1)}_j = 0$ iff $\widehat{z}^{(i+1)}_j = z^{(i+1)}_j$, i.e., ReLU is activated; otherwise, $t^{(i+1)}_j = 1$.

The MILP formalization allows us to rigorously reason about the MLP’s behaviour. In particular, eq. 1 formally defines a relation $\mathcal{N} \subseteq \mathbb{F} \times \mathbb{S}$, s.t. for an I/O-pair $\langle \mathbf{x}, \mathbf{y} \rangle \in \mathbb{F} \times \mathbb{S}$, we have $\langle \mathbf{x}, \mathbf{y} \rangle \in \mathcal{N}$, iff $\sigma(\mathbf{x}) = \mathbf{y}$. A verifier is essentially another relation $\mathcal{V} \subseteq \mathbb{F} \times \mathbb{S}$. We call the verifier $\mathcal{V}$ sound if $\mathcal{V} \subseteq \mathcal{N}$. We call the verifier $\mathcal{V}$ complete if $\mathcal{N} \subseteq \mathcal{V}$. Sound and complete verifiers such as Marabou [19] make heavy use of cutting-edge MILP solvers, e.g., Gurobi³, while utilizing sophisticated heuristics tailored for MILPs modeling MLPs. This allows them to analyse much larger networks, whose size would be otherwise prohibiting. Still, note that verifying a MLP is an NP-complete problem [18].

3 Intervals in Higher Dimensions↩︎

In this section, we present some foundational results from Interval Algebra [23], [26]. Firstly, we generalize the $\leq ~\subseteq \mathbb{R} \times \mathbb{R}$ relation to high-dimensional spaces. For two vectors $\boldsymbol{\ell}, \boldsymbol{u}\in \mathbb{R}^d$ we write $\boldsymbol{\ell}\leq \boldsymbol{u}$ iff $\ell_i \leq u_i$ for all $i \in [d]$. Similarly, we write $\boldsymbol{\ell}< \boldsymbol{u}$ iff $\ell_i < u_i$ for each $i \in [d]$⁴. Below, we describe a generalization of real intervals for high-dimensional spaces.

Definition 2 (High Dimensional Intervals). Let $\boldsymbol{\ell}, \boldsymbol{u}\in \mathbb{R}^d$, with $\boldsymbol{\ell}\leq \boldsymbol{u}$. A closed interval $[\boldsymbol{\ell}, \boldsymbol{u}] \subset \mathbb{R}^d$ is the set of points $\mathbf{x} \in \mathbb{R}^d$ such that $\boldsymbol{\ell}\leq \mathbf{x} \leq \boldsymbol{u}$. An open interval* $(\boldsymbol{\ell}, \boldsymbol{u})$ is the interior of the respective closed interval, i.e., $(\boldsymbol{\ell}, \boldsymbol{u}) = [\boldsymbol{\ell}, \boldsymbol{u}]^\circ$. We denote with $\mathbb{I}(d)$ the space of the $d$–dimensional closed intervals, i.e. $\mathbb{I}(d) = \{S \subset \mathbb{R}^d \mid \exists \;\boldsymbol{\ell}, \boldsymbol{u}\in \mathbb{R}^d, \;\boldsymbol{\ell}\leq \boldsymbol{u}, \;S = [\boldsymbol{\ell}, \boldsymbol{u}]\}$.*

From the above definition, it is easy to see that $\mathbf{x} \in (\boldsymbol{\ell}, \boldsymbol{u})$ iff $\boldsymbol{\ell}< \mathbf{x} < \boldsymbol{u}$. Note that for any $\mathbf{x} \in \mathbb{R}^d$ the closed interval $[\mathbf{x}, \mathbf{x}]$ is a trivial interval, corresponding to the singleton $\{\mathbf{x}\}$. Additionally, the trivial open interval $(\mathbf{x}, \mathbf{x})$ corresponds to the empty set $\varnothing$. Observe that the sphere $\mathcal{B}^\infty(\mathbf{x}, \rho)$ corresponds to the uniform interval $[\mathbf{x} - \rho\mathbf{1}, \mathbf{x} + \rho\mathbf{1}]$. Geometrically, an interval $[\boldsymbol{\ell}, \boldsymbol{u}]$ corresponds to a hyper-rectangle in $\mathbb{R}^d$. In particular, a uniform interval centered at $\mathbf{x}$ corresponds to a hyper-cube with $\mathbf{x}$ as its barycenter. We extend the notation of Definition 2, denoting with $\mathbb{I}(d)\vert_{\mathbf{x}}\subseteq \mathbb{I}(d)$ the set of all intervals including the point $\mathbf{x} \in \mathbb{R}^d$. Naturally, for every $\mathbf{x} \in \mathbb{R}^d$, and every $\rho > 0$, $\mathcal{B}^{\infty}(\mathbf{x}, \rho) \in \mathbb{I}(d)\vert_{\mathbf{x}}$. We often consider an interval universe $\mathbb{F}= [\underline{\mathbf{U}}, \overline{\mathbf{U}}]$, for specific $\underline{\mathbf{U}}, \overline{\mathbf{U}}$. We denote with $\mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}\subseteq \mathbb{I}(d)\vert_{\mathbf{x}}$ all the intervals that include the point $\mathbf{x}$ and are included in $\mathbb{F}$.

3.1 Operations on Intervals & the Interval Lattice↩︎

Below we give some elementary operations on the interval space $\mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$.

propositionintervalops Let $[\boldsymbol{\ell}, \boldsymbol{u}], [\boldsymbol{m}, \boldsymbol{n}] \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$ two $d$–dimensional intervals, and the operations:

$[\boldsymbol{\ell}, \boldsymbol{u}] + [\boldsymbol{m}, \boldsymbol{n}] \overset{\Delta}{=} [\boldsymbol{\ell}+ \boldsymbol{m}, \boldsymbol{u}+ \boldsymbol{n}]$
$[\boldsymbol{\ell}, \boldsymbol{u}] \sqcup [\boldsymbol{m}, \boldsymbol{n}] \overset{\Delta}{=} [\min\{\boldsymbol{\ell},\boldsymbol{m}\}, \max\{\boldsymbol{u}, \boldsymbol{n}\}]$
$[\boldsymbol{\ell}, \boldsymbol{u}] \sqcap [\boldsymbol{m}, \boldsymbol{n}] \overset{\Delta}{=} [\max\{\boldsymbol{\ell},\boldsymbol{m}\}, \min\{\boldsymbol{u}, \boldsymbol{n}\}]$

For any $\square \in \{+, \sqcup, \sqcap\}$ and $I, J \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$, $I ~\square~ J \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$.

Observe that the $\sqcap$ operator coincides with the set-theoretic intersection $\cap$. However, it holds that $I ~\sqcup~ J \supsetneq I \cup J$. In general, the union of two intervals is not an interval. Below, we review how the $\sqcup, \sqcap$ operations reveal the underlying structure of the interval space $\mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$.

Theorem 1 (Interval Lattice, [23]). The interval space $\mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$, organized under $\subseteq$ constitutes a complete lattice* with $\sqcup, \sqcap$ as the meet and join operations, respectively.*

Note that the set-theoretic exclusion of a point from an interval ($I \setminus \mathbf{x}$) does not yield an interval. We therefore define an alternative exclusion operator that removes a point $\mathbf{x}$ from an interval $I= [\boldsymbol{\ell}, \boldsymbol{u}]$. The operator selects a coordinate along which the induced modification to $I$ is minimal, and then adjusts either $\ell_i$ or $u_i$–which results in the smaller change–by setting it to a value infinitesimally smaller or larger than $x_i$. This infinitesimal offset is formalized using a parameter $\delta>0$.

Definition 3. Let $I = [\boldsymbol{\ell}, \boldsymbol{u}] \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$ be an interval and $\mathbf{x}^\prime \in I$ a point included in the interval $I$. Let $k = \arg\max\{\vert x_i - x^\prime_i \vert \mid i \in [d] \wedge \mathbf{x} \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}\}$⁵. If $x_i - x^\prime_i > 0$, then $I \!\sideset{}{_\delta}{\mathop{\scalebox{1}[1.3]{/}}} \mathbf{x}^\prime = [\boldsymbol{\ell}^\prime, \boldsymbol{u}]$, where $\ell^\prime_i = \ell_i$, for every $i \neq k$ and $\ell_k = x^\prime_k + \delta$, for some $\delta > 0$. If $x_i - x^\prime_i < 0$, then $I \!\sideset{}{_\delta}{\mathop{\scalebox{1}[1.3]{/}}} \mathbf{x}^\prime = [\boldsymbol{\ell}, \boldsymbol{u}^\prime]$, where $u^\prime_i = u_i$, for every $i \neq k$ and $u_k = x^\prime_k - \delta$, for some $\delta > 0$.

Despite its subtleties, we will see in Sec. 4 that operator $ !$ is natural. $I \!\sideset{}{_\delta}{\mathop{\scalebox{1}[1.3]{/}}}\mathbf{x}^\prime$ chooses a maximum refinement of $I$ that excludes $\mathbf{x}^\prime$. Further, to simplify notation, we will drop the $\delta$ from the notation of $ !$ when it’s clear from the context.

3.2 Interval Objectives↩︎

To formulate our methodology, we examine the following family of measures on intervals. We call these quantities objectives, since they are optimized in the computation of maximal sound or minimal complete intervals.

Definition 4 (Interval Objectives). Consider an interval $I = [\boldsymbol{\ell}, \boldsymbol{u}] \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$, with $\boldsymbol{\ell}\leq \boldsymbol{u}$. Then we define the following measures:

Minimum Edge Length:	$\alpha(I)$	$= \min_{i \in [d]} u_i - \ell_i$
Perimeter:	$\pi(I)$	$= \sum_{i \in [d]} u_i - \ell_i$
Volume:	$v(I)$	$= \prod_{i \in [d]} u_i - \ell_i$.
Diameter:	$\mathcal{A}(I)$	$= \max_{i \in [d]} u_i - \ell_i = \\|u_i - \ell_i\\|_\infty$

These objectives are related through the arithmetic-geometric means inequality.

propositionnumericalgeometricmean For an interval $I \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$ and the measures of Def. 4 we have, \[\label{eq:numerical-geometric-mean} \mathcal{A}(I) \geq \frac{1}{d}\cdot\pi(I) \geq \sqrt[d]{v(I)}\geq \alpha(I)\tag{2}\]

Eq. 2 highlights the significance of the minimum edge length measure within the family of interval measures defined in Def. 4, since it provides an explicit lower bound on all other measures. Thus, it suffices to ensure the non-triviality, i.e., strict positivity, of $\alpha(I)$, to ensure the non-triviality of all the remaining objectives. This fact supports the choice of the exclusion operation of Def. 3, since it computes the optimal exclusion w.r.t. the minimum edge length objective.

theoremintervalexclusion Consider an interval $I \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$ and a point $\mathbf{x}^\prime \in I$. For any interval $J \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$, with $\mathbf{x}^\prime \notin J$ and $J \subseteq I$, we have $\alpha(J) \leq \alpha(I/\mathbf{x}^\prime)$.

4 Sound & Complete Interval Certifications↩︎

Figure 1: A sound interval certification $[\mathbf{lb}, \mathbf{ub}]$, and a complete interval certification $[\mathbf{LB}, \mathbf{UB}]$, for a MNIST image of “7”. The sound interval certification has been computed using the Algorithm [algo:generic-traversal] , while its complete counterpart was computed by Algorithm [algo:non-det-expand] in $\ell_\infty$-spheres..

Definition 5. Consider a classifier $\kappa \colon \mathbb{F} \to \mathcal{C}$, with $\mathbb{F} \subset \mathbb{R}^{d}$, and $\mathbf{x} \in \mathbb{F}$ an input, s.t. $\kappa(\mathbf{x}) = c$. Moreover, let $I, J \in \mathbb{I}(d)$ two intervals, s.t. \[\label{eq:interval-sound-complete} {!}{\mathbf{x} \in I \land \left[\forall \mathbf{x}^\prime \in \mathbb{F}\colon \;\mathbf{x}^\prime \in I \to \kappa(\mathbf{x}^\prime) = c \right], \enspace \mathbf{x} \in J \land \left[\forall \mathbf{x}^\prime \in \mathbb{F}\colon \;\mathbf{x}^\prime \notin J \to \kappa(\mathbf{x}^\prime) \neq c \right],}\qquad{(2)}\] then we call $I$ a sound* and $J$ a complete certification.*

Intuitively, a sound certification $I$ assures that any perturbation of the input $\mathbf{x}$ inside $I$ will not change its prediction. On the other hand, a complete certification $J$ asserts that if $\mathbf{x}$ is moved outside of $J$, then its prediction is guaranteed to change (see Fig. 1). Naturally, a trivial sound certification is the input itself, expressed as an interval, i.e., $I = [\mathbf{x}, \mathbf{x}]$. Similarly, a trivial complete certification will be the entire input space $\mathbb{F}$ itself. Therefore, we are interested in maximally sound and minimally complete certifications. Since $I, J$ are subsets of $\mathbb{F}$, maximality and minimality are considered w.r.t.set inclusion.

4.1 Verification Oracles↩︎

In our algorithms, we will utilize two oracles that either verify the truth of a property on a given interval, or return a counterexample, witnessing its falsehood. In particular, we are interested in soundness and completeness oracles, verifying an interval’s respective property. These oracles can be constructed using a sound and complete MLP verifier⁶. Indeed, we make use of the Marabou verifier [19], where we extend the set of constraints fed to the verifier. To that end, let $\mathcal{N}(\mathbf{x}, \mathbf{y})$ be the I/O-relation describing a MLP, as in eq. 1 .

For a given MLP, described by the relation $\mathcal{N}(\cdot, \cdot)$ and an interval $I = [\boldsymbol{\ell}, \boldsymbol{u}] \subseteq \mathbb{F}$, the soundness oracle is given by the predicate $\mathscr{S}_{I, \mathcal{N}}$, where, \[\label{eq:sound-oracle} {!}{\mathscr{S}_{I, \mathcal{N}}(\mathbf{x}^\prime) \equiv \exists\mathbf{y}. ~(\boldsymbol{\ell}\leq \mathbf{x}^\prime \leq \boldsymbol{u})~ \land ~\mathcal{N}(\mathbf{x}^\prime, \mathbf{y})~ \land ~\left( \bigvee_{j \in [d_{\text{out}}] \setminus c} y_j - y_{c} > \epsilon \right).}\tag{3}\] If the predicate $\mathscr{S}_{I, \mathcal{N}}(\mathbf{x}^\prime)$ is a contradiction, i.e., $\models \lnot \mathscr{S}_{I, \mathcal{N}}(\mathbf{x}^\prime)$, the interval $I$ is a sound certification. However, any $\mathbf{x} \in \mathbb{F}$, s.t. $\mathbf{x}^\prime \models \mathscr{S}_{I, \mathcal{N}}(\mathbf{x}^\prime)$ is a counterexample. In the literature, such an input is also called adversarial example or adversarial attack. Such a counterexample $\mathbf{x}^\prime$ can “fool” the MLP, since it will be relatively close to a given input $\mathbf{x}$, but is classified to a different class from $c = \kappa(\mathbf{x})$. The latter is ensured by the last clause in eq. 3 , by asserting that a score different than $c$ is the highest in the output scores vector, w.r.t. a constant $\epsilon > 0$.

Conversely, the completeness oracle is provided by predicate $\mathscr{C}_{I, \mathcal{N}}$, where, \[\label{eq:complete-oracle} {!}{\mathscr{C}_{I, \mathcal{N}}(\mathbf{x}^\prime) \equiv \left( \bigvee_{i \in [{d_{\text{in}}}]} x_i^\prime < \ell_i \lor u_i < x_i^\prime \right)~ \land ~\mathcal{N}(\mathbf{x}^\prime, \mathbf{y})~ \land ~\left( \bigwedge_{j \in [d_{\text{out}}] \setminus c} y_{c} - y_j > \epsilon \right).}\tag{4}\] If the predicate $\mathscr{C}_{I, \mathcal{N}}(\mathbf{x}^\prime)$ is a contradiction, i.e., $\models \lnot \mathscr{C}_{I, \mathcal{N}}(\mathbf{x}^\prime)$, then the interval $I$ is a complete certification. However, any $\mathbf{x} \in \mathbb{F}$, s.t.$\mathbf{x}^\prime \models \mathscr{C}_{I, \mathcal{N}}(\mathbf{x}^\prime)$ is a counterexample. Essentially, the completeness predicate is the dual of $\mathscr{S}_{I, \mathcal{N}}$. Notably, since we use a sound and complete verification system, invoking both the oracles $\mathscr{S}_{I, \mathcal{N}}$ and $\mathscr{C}_{I, \mathcal{N}}$ inherits the computational hardness of MLP verification [18].

Finally, observe that the formulas in eq. 3 and 4 can be use to “locally” describe the MLP. Consider a sound certification $I$ and a complete verification $J$, then it holds $\lnot \mathscr{I}_{I, \mathcal{N}}(\mathbf{x}) \models \kappa(\mathbf{x}) = c \models \lnot \mathscr{C}_{J, \mathcal{N}}(\mathbf{x})$, since $J \supseteq \mathcal{D}_c \supseteq I$. Ensuring completeness minimality and soundness maximality minimizes the gap between $J, I$ and provides a tighter local approximation of the underlying MLP.

4.2 The Generic Traversal Algorithm↩︎

In Algorithm [algo:generic-traversal] we present a simple traversal algorithm that explores the interval lattice $\mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$ introduced in Sec. 3. Our algorithm is generic in the sense that it can compute interval certifications with different properties depending on the parameters passed as arguments. In the sequel, we show how to implement three big-step⁷ operators on intervals. Each big step operator is the result of iteratively applying one of the small-step operators introduced in Sec. 3, i.e., $\{+, \sqcup, \sqcap, /\}$.

4.3 Minimally Complete Certifications via the $\top$–Operator↩︎

We begin our discussion on maximally complete certifications by defining the $\top$-operator (see Def. 6), between a compact decision surface $\mathcal{D}_c \subseteq \mathbb{F}$ and an input point $\mathbf{x} \in \mathbb{F}$, s.t. $\kappa(\mathbf{x}) = c$. We see that we can obtain a maximally complete interval certification, w.r.t. $\mathcal{D}_c$ and $\mathbf{x}$ as a result of the $\top$-operator. Moreover, the complete interval certification is unique for a particular class, and independent from the choice of the input $\mathbf{x}$. We show this fact in Th. [theo:complete-certification].

Definition 6 ($\top$-Operator). Consider a classifier $\kappa\colon\mathbb{F} \to \mathcal{C}$, an input point $\mathbf{x} \in \mathbb{F}$, s.t. $\kappa(\mathbf{x}) = c$, and the compact decision surface $\mathcal{D}_c$. With $\mathcal{D}_c\top\mathbf{x}$ we denote the interval $[-\underline{\mathbf{R}}, \overline{\mathbf{R}}]$, s.t., \[\label{eq:Radii} {!}{\underline{R}_i= \max\{x_i - x^\prime_i \mid x_i^\prime \leq x_i, \;\mathbf{x}^\prime \in \mathcal{D}_c\}, \;\overline{R}_i= \max\{x^\prime_i - x_i \mid x_i^\prime > x_i, \;\mathbf{x}^\prime \in \mathcal{D}_c\}. }\qquad{(3)}\]

theoremcompletecertification The interval $\mathcal{D}_c\top\mathbf{x}$ is the unique complete certification. Moreover, for any two $\mathbf{x}_1, \mathbf{x}_2 \in \mathcal{D}_c$, we have $\mathcal{D}_c\top\mathbf{x}_1 = \mathcal{D}_c\top\mathbf{x}_2$.

The interval $\mathcal{D}_c\top\mathbf{x}$ can be computed using Algorithm [algo:generic-traversal], with the parameters $I_0 = [\mathbf{x}, \mathbf{x}]$, $\varphi_{I, \mathcal{N}} = \mathscr{C}_{I, \mathcal{N}}$, and $I ~\square~ \mathbf{x}^\prime = I \sqcup [\mathbf{x}^\prime -\delta\mathbf{1}, \mathbf{x}^\prime +\delta\mathbf{1}]$, where $\delta > 0$ is a precision constant. Intuitively, with these parameters Algorithm [algo:generic-traversal] implements a bottom-up search policy (BUS), beginning from the trivial interval $[\mathbf{x}, \mathbf{x}]$, proceeding to greater intervals, by including members of the surface $\mathcal{D}_c$. The precision parameter $\delta > 0$ regulates both the outcome’s accuracy and the convergence rate of our algorithm.

theoremalgomincomplete Consider a compact decision surface $\mathcal{D}_c \subset \mathbb{F}$. Let $I \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$ the interval returned by Algorithm [algo:generic-traversal]. It holds that $\mathcal{D}_c\top\mathbf{x} \subseteq I \subseteq \mathcal{D}_c\top\mathbf{x} + [-\delta\mathbf{1}, \delta\mathbf{1}]$. Moreover, Algorithm [algo:generic-traversal] terminates after $O(d\cdot\mathcal{A}(\mathcal{D}_c\top\mathbf{x})/\delta)$ steps.

4.4 Edge Length Non-Triviality in Sound Certifications via the $\bot$-Operator↩︎

Before we proceed to maximally sound certifications, we present the $\bot$-operator that returns a special kind of sound certifications. These certifications are guaranteed (under certain assumptions) to have strictly positive minimum edge length. Let $\mathbf{x} \in \mathbb{F}$ be an input point. We consider the sequence of polyhedral cones⁸ $\langle \underline{V}_i, \overline{V}_i \rangle$ for each $i \in [d]$, in eq. 5 . We have $\underline{V}_i \cap \overline{V}_i = \{\mathbf{0}\}$, for every $i \in [d]$, and $(\cup_{i \in [d]} \underline{V}_i) \cup (\cup_{i \in [d]} \overline{V}_i) = \mathbb{R}^d$. Using the cone partition of eq. 5 we define the $\bot$-operator. \[\label{eq:cones} \begin{align} & \underline{V}_i = \left\{\mathbf{x}^\prime \in \mathbb{F}~\big\vert~ x^\prime_i \leq x_i, \forall j \in [d] ~\vert x^\prime_i \vert \geq \vert x^\prime_j \vert \right\}, \\ & \overline{V}_i = \left\{\mathbf{x}^\prime \in \mathbb{F}~\big\vert~ x^\prime_i \geq x_i, \forall j \in [d] ~\vert x^\prime_i \vert \geq \vert x^\prime_j \vert \right\}. \end{align}\tag{5}\]

Definition 7 ($\bot$-Operator). Consider a classifier $\kappa\colon\mathbb{F} \to \mathcal{C}$, an input point $\mathbf{x} \in \mathbb{F}$, s.t. $\kappa(\mathbf{x}) = c$, and the compact decision surface $\mathcal{D}_c$. With $\mathcal{D}_c\bot\mathbf{x}$ we denote the interval $[-\underline{\mathbf{r}}, \overline{\mathbf{r}}]$, s.t., \[\label{eq:radii} \underline{r}_i= \inf\{x_i - x^\prime_i \mid \mathbf{x}^\prime \in \underline{V_i} \setminus \mathcal{D}_c\}, \quad \overline{r}_i= \inf\{x^\prime_i - x_i \mid \mathbf{x}^\prime \in \overline{V_i} \setminus \mathcal{D}_c\}.\qquad{(4)}\]

In Prop. [prop:maximal-sound-approx] we establish the soundness of $\mathcal{D}_c\bot\mathbf{x}$.

propositionpropmaximalsoundapprox Let $\mathcal{D}_c \subseteq \mathbb{F}$ be a compact decision surface, s.t. $\mathbf{x} \in \mathcal{D}_c$. It holds $\mathcal{D}_c\bot\mathbf{x} \subseteq \mathcal{D}_c$.

The interval $\mathcal{D}_c\bot\mathbf{x}$ can be computed using Algorithm [algo:generic-traversal], with the parameters $I_0 = \mathbb{F}$, $\varphi_{I, \mathcal{N}} = \mathscr{S}_{I, \mathcal{N}}$, and $I ~\square~ \mathbf{x}^\prime = I \!\sideset{}{_\delta}{\mathop{\scalebox{1}[1.3]{/}}} \mathbf{x}^\prime$, as in Def. 3. Algorithm [algo:generic-traversal] implements a top-down search policy (TDS), beginning from the whole input space $\mathbb{F}$, proceeding to smaller intervals, by excluding counterexamples $\mathbf{x}^\prime \in \mathbb{F} \setminus \mathcal{D}_c$. Similar to Subsec. 4.3, the precision parameter $\delta$ regulates both the outcome’s accuracy and the convergence rate of our algorithm.

theoremtheoalgomaxsound Consider a compact decision surface $\mathcal{D}_c \subset \mathbb{F}$. Let $I \in \mathbb{I}(d)\vert^\mathbb{F}_\mathbf{x}$ the interval returned by Algorithm [algo:generic-traversal]. It holds that $\mathcal{D}_c\bot\mathbf{x} - [-\delta\mathbf{1}, \delta\mathbf{1}] \subseteq I \subseteq \mathcal{D}_c$. Moreover, the algorithm terminates after $O(d[\mathcal{A}(\mathbb{F}) - \mathcal{A}(\mathcal{D}_c\bot\mathbf{x})]/\delta)$ steps.

The following result guarantees a computed certification with non-trivial edge lengths, provided that the input belongs to the interior of the decision surface.

propositionnontrivialitylb If $\mathbf{x} \in \mathcal{D}^\circ_c$, then $\alpha(\mathcal{D}_c\bot\mathbf{x}) > 0$.

Recall that, from Prop. [prop:numerical-geometric-mean], several objectives are lower bounded by the minimum edge length. Thus, the interval $\mathcal{D}_c\bot\mathbf{x}$ provides a non-trivial lower bound to these quantities, as well. Notably, Prop. [prop:non-triviality-lb] suggests that we can verify a minimum coordinate-wise perturbation tolerance. Our experiments in Sec. 6 show that this also holds in practice. We discuss optimization aspects of interval certifications at the end of this section.

4.5 The Maximal Closure Operator $[I]$↩︎

Computing maximally sound certifications share similarities with their complete counterparts, but also exhibit important differences. The primary difference is that, in general, there will be multiple maximal sound certifications. Therefore, for a sound interval $I$, we consider its maximal closure, denoted with $[I]$, that contains all the supersets of $I$ that are maximally sound.

Definition 8 (Maximal Closure Operator). Consider a classifier $\kappa\colon\mathbb{F} \to \mathcal{C}$, an input point $\mathbf{x} \in \mathbb{F}$, s.t. $\kappa(\mathbf{x}) = c$, and the compact decision surface $\mathcal{D}_c$. Let $I \subseteq \mathcal{D}_c$ be a sound interval certification, s.t. $\mathbf{x} \in I$. With $[I]$ we denote the maximal closure* of $I$, where, $[I] = \{J \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}\mid I \subseteq J \subseteq \mathcal{D}_c\}.$*

Lem. [lem:maximal-soundness] characterises all the maximally sound interval certifications. Intuitively, an interval certification is maximally sound if expanding unilaterally any of its coordinates results in the inclusion of a counterexample. Based on Lem. [lem:maximal-soundness], we present a non-deterministic algorithm, which chooses a coordinate of each of the two interval’s endpoints to expand in each step. If the expansion leads to a non-sound certification, the coordinate is discarded, not to be expanded any further. The pseudocode of the algorithm is presented in App. 10, while its correctness is established in Th. [theo:non-det-expand].

lemmalemmaximalsoundness Consider a classifier $\kappa\colon\mathbb{F} \to \mathcal{C}$, an input point $\mathbf{x} \in \mathbb{F}$, s.t. $\kappa(\mathbf{x}) = c$, and the compact decision surface $\mathcal{D}_c$. Moreover, let $I = [\boldsymbol{\ell}, \boldsymbol{u}] \subseteq \mathcal{D}_c$. The interval $I$ is maximally sound, iff for every $i \in [d]$, and every $\delta > 0$, we have $[\boldsymbol{\ell}- \delta\mathbf{e}_i, \boldsymbol{u}] \setminus \mathcal{D}_c \neq \varnothing$ and $[\boldsymbol{\ell}, \boldsymbol{u}+ \delta\mathbf{e}_i] \setminus \mathcal{D}_c \neq \varnothing$.

theoremnondetexpand Consider a compact decision surface $\mathcal{D}_c \subset \mathbb{F}$, and $\mathbf{x} \in \mathbb{F}$ an input. Let $X \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$ be the trivial sound certification $X = [\mathbf{x}, \mathbf{x}]$. For every maximally sound interval $I \in [X]$ there is a choice of indices in the operation of Algorithm [algo:non-det-expand], resulting to an interval $J$, s.t. $I - [-\delta\mathbf{1}, \delta\mathbf{1}] \subseteq J \subseteq I$. Moreover, such $J$ is computed in $O(d\cdot\mathcal{A}(\mathbb{F})/\delta)$ non-deterministic steps.

4.6 The Space of Interval Certifications↩︎

We close our study on interval certifications by examining the structure of the interval certifications’ space and how our earlier discussion is reflected in that space. As we saw in Sec. 3, the structure $\langle \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}, \subseteq \rangle$ forms an innumerably infinite lattice [23], with $\sqcup, \sqcap$ as the join and meet operators respectively. The bottom element of this space is the trivial interval $[\mathbf{x}, \mathbf{x}]$ and the top element is the universe $\mathbb{F}$. Consider a compact decision surface $\mathcal{D}_c \subset \mathbb{F}$, s.t. $\mathbf{x} \in \mathcal{D}_c$, i.e. $\kappa(\mathbf{x}) = c$. The following (set-theoretic) inequality holds: $[\mathbf{x}, \mathbf{x}] \subseteq \mathcal{D}_c\bot\mathbf{x} \subseteq \mathcal{D}_c \subseteq \mathcal{D}_c\top\mathbf{x} \subseteq \mathbb{F}$. Naturally, every subset of $\mathcal{D}_c\bot\mathbf{x}$ is a sound certification. The interval $\mathcal{D}_c\bot\mathbf{x}$ is not maximal, but every set in its maximal closure $[\mathcal{D}_c\bot\mathbf{x}]$ is. Moreover, every complete certification includes $\mathcal{D}_c\top \mathbf{x}$. Fig. 3 illustrates the structure of the $\langle \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}, \subseteq \rangle$ lattice. Observe that the hierarchy in Fig. 3 collapses when $\mathcal{D}_c$ is an interval, i.e., when $\mathcal{D}_c \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$. This fact follows from Th.s [theo:complete-certification] and [theo:non-det-expand].

Corollary 1. $[\mathcal{D}_c\bot\mathbf{x}] = \{\mathcal{D}_c\top\mathbf{x}\}$ iff $\mathcal{D}_c \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$.

Figure 3: The structure of \mathbb{I}(d)\vert^\mathbb{F}_{\mathbf{x}}. We adopt the Hasse diagram convention depicting each element higher from the elements it dominates. \mathcal{D}_c is shown in the image with a dashed line, because, in general, \mathcal{D}_c \notin \mathbb{I}(d)\vert^\mathbb{F}_{\mathbf{x}}, and thus, technically, \mathcal{D} is not part of the diagram. Moreover, \omega(\mathcal{D}_c\bot\mathbf{x}) \leq \omega(\mathcal{D}_c) \leq \omega(\mathcal{D}_c\top\mathbf{x}), for an increasing objective \omega(\cdot). — Figure 3: The structure of $\mathbb{I}(d)\vert^\mathbb{F}_{\mathbf{x}}$. We adopt the Hasse diagram convention depicting each element higher from the elements it dominates. $\mathcal{D}_c$ is shown in the image with a dashed line, because, in general, $\mathcal{D}_c \notin \mathbb{I}(d)\vert^\mathbb{F}_{\mathbf{x}}$, and thus, technically, $\mathcal{D}$ is not part of the diagram. Moreover, $\omega(\mathcal{D}_c\bot\mathbf{x}) \leq \omega(\mathcal{D}_c) \leq \omega(\mathcal{D}_c\top\mathbf{x})$, for an increasing objective $\omega(\cdot)$.

5 Optimization over Interval Certifications↩︎

We are able to exploit the structure of the interval certification space to compute an optimal certification, w.r.t a certain objective measure and under certain assumptions. To that end, consider an arbitrary objective $\omega\colon\mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}\to \mathbb{R}_{\geq 0}$, respecting the following properties:

$\omega([\mathbf{x}, \mathbf{x}]) = 0$
For every $I_1, I_2 \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$, if $I_1 \subseteq I_2$, then $\omega(I_1) \leq \omega(I_2)$.

Note that the objectives of Sec. 3 follow these properties. In the sequel, we implicitly assume that $\omega \in \{\alpha, \pi, v, \mathcal{A}\}$. Consider the interval certifications $I, J \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$, where $I$ is sound, and $J$ is complete, w.r.t. a decision surface $D_c$. For an objective satisfying the above properties, it holds $\omega(I) \leq \omega(\mathcal{D}_c) \leq \omega(J)$. Now, consider the following dual optimization problems. \[\begin{align} & \underline{\omega} = \max \left\{\omega(I) \mid I \subseteq \mathcal{D}_c \wedge I \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}\right\}, \tag{6} \\ & \overline{\omega} = \min \left\{\omega(I) \mid I \supseteq \mathcal{D}_c \wedge I \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}\right\}. \tag{7} \end{align}\]

We call eq. 6 , the Sound Interval Maximization (SIM) problem, while eq. 7 problem. Using the $\top$-operator we can exactly compute the optimal solution $\overline{\omega}$ of the complete minimization problem, i.e. $\overline{\omega} = \omega(\mathcal{D}_c\top\mathbf{x})$, for any $\mathbf{x} \in \mathcal{D}_c$. However, the $\bot$-operator only provides a lower bound to the solution of sound maximization, i.e., $\underline{\omega} \geq \omega(\mathcal{D}_c\bot\mathbf{x})$. A better lower bound can be obtained by taking the maximal closure $[\mathcal{D}_c\bot\mathbf{x}]$. Nevertheless, finding the maximum sound interval certification is computationally intractable. Subsequently, we discuss the computational hardness of the sound maximization problem.

5.1 On the Intractability of Sound Maximization↩︎

Recent results provide evidence on the intractability of sound maximization. In particular, recall that [18] establishes the NP-completeness of the MLP verification problem. Since we use verification oracles, this hardness is inherited to our problem. Moreover, [22] demonstrates the in-approximability of sound maximization, even when restricted to uniform interval certifications, i.e., $\ell_\infty$-spheres. Building on these existing results, we further show that the decision version of the SIM problem is NP-hard. Specifically, even when the verification oracle cost is ignored, the problem admits no polynomial-time algorithm, unless $\mathbf{P} = \mathbf{NP}$.

theoremtheosoundmaxhard Consider a compact decision surface $\mathcal{D}_c$ and an input point $\mathbf{x} \in \mathcal{D}_c$. Then, the existence of a sound interval $I \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$, with $I \subseteq \mathcal{D}_c$ and $v(I) \geq \gamma$, $\gamma > 0$ cannot be decided in $\mathsf{poly}(d, n, t_{\text{oracle}})$ time, unless P=NP.

In Th. [theo:sound-max-hard], with $\mathsf{poly}(d, n, t_{\text{oracle}})$ we denote the set of all polynomials on $d, n, t_{\text{oracle}}$, where $n$ is the number of oracle calls, and $t_{\text{oracle}}$ is the worst-case time consumed by the soundness verification oracle. Note that Th. [theo:sound-max-hard] constitutes a strong intractability result, since it states that the complexity-significant parameters cannot be related polynomially. In other words, it does not suffice to keep the number of dimensions $d$ small, make few oracle calls (i.e., keep $n$ small), or implement faster verifiers (i.e., keep $t_{\text{oracle}}$ small); to efficiently and optimally solve maximum soundness. All three parameters must be kept bounded for an optimal sound certification, to be computationally possible. Thusly, we chose to examine a more efficient greedy variant in Sec. 4, based on the exclusion operator in Def. 3. Unfortunately, making the optimal decision in every (small) step does not imply overall (big-step) optimality.

The intractability of the maximum soundness problem follows from the intractability of the Maximum Empty Rectangle (MER) problem [27]–[30]. In this problem, we assume a bounding interval $\mathbb{F}$ and a finite set of forbidden points $\mathcal{F} \subset \mathbb{F}$. Our goal is to find an interval $I \subseteq \mathbb{F}$, s.t. $I \cap \mathcal{F} = \varnothing$. Namely, the interval $I$ will exclude all the forbidden points. Moreover, we require $I$ to be the maximum, w.r.t. the volume $v(\cdot)$. [28] prove that this problem is NP-hard for arbitrary number of dimensions. However, MER cannot be directly reduced to SIM. Note that in SIM, we require the given input $\mathbf{x}$ to be included in the returned interval $I$. In literature, the latter problem is known as q-MER [31], where we demand the maximum empty rectangle to include a query point. Nevertheless, [31] does not provide any intractability result. [28] prove MER’s intractability, by reducing from the Independent Set (IS). The same reduction can be applied to show, in Lem. [lem:sound-max-hard], that IS is also reduced to q-MER, by setting $\mathbf{q} = \mathbf{0}$.

lemmalemsoundmaxhard Consider an interval universe $\mathbb{F} = [\underline{\mathbf{U}}, \overline{\mathbf{U}}]$. Moreover assume a finite set of forbidden points $\mathcal{F} \subset \mathbb{F}$, and a query point $\mathbf{q} \in \mathbb{F} \setminus \mathcal{F}$. The existence of an interval $I \subseteq \mathbb{F}$, s.t. $\mathbf{q} \in I$, $I \cap \mathcal{F} = \varnothing$, and $v(I) \geq \gamma$, for given $\gamma > 0$, cannot be decided in polynomial time, unless P=NP.

Th. [theo:sound-max-hard] is derived from Lem. [lem:sound-max-hard] by considering as $\mathcal{F}$ the set of counterexamples returned by the soundness verification oracle $\mathscr{S}_{I, \mathcal{N}}$. Finally, from Prop. [prop:numerical-geometric-mean] for each interval it holds $\sqrt[d]{v(I)} \geq \alpha(I)$, therefore Lem. [lem:sound-max-hard] and Th. [theo:sound-max-hard] can be modified to use $\alpha(\cdot)$, as the desired targeted objective.

5.2 Sound Maximization on Uniform Intervals↩︎

We call the SIM problem, when constrained to uniform intervals ($\ell_\infty$-spheres) $\mathbb{B}$-SIM. For disambiguation, we call $\mathbb{I}$-SIM, the SIM problem for general intervals. As we mentioned earlier, $\mathbb{B}$-SIM’s intractability persists, even if constrained to uniform intervals, [18], [22]. However, we can compute an optimal solution in $\mathsf{poly}(d, n, t_{\text{oracle}})$ time. In particular, we can compute a maximum sound uniform interval $B = [\mathbf{x} - \rho\mathbf{1}, \mathbf{x} + \rho\mathbf{1}]$, s.t. $v(B) \geq \gamma, \gamma > 0$, in $\log(\mathcal{A}(\mathbb{F}/\delta))\cdot t_{\text{oracle}}$ time. We find the uniform interval’s radius $\rho > 0$, by applying dichotomic search on the real interval $[0, \mathcal{A}(\mathbb{F})]$. Formally, this is provided by the following result.

theoremsoundmaxcyclic Consider a compact decision surface $\mathcal{D}_c$ and an input point $\mathbf{x} \in \mathcal{D}_c$. Then, the existence of a sound uniform interval $B = [\mathbf{x} - \rho\mathbf{1}, \mathbf{x} + \rho\mathbf{1}]$, with $\mathbf{x} \in B$, $B \subseteq \mathcal{D}_c$ and $v(B) \geq \gamma$, $\gamma > 0$ can be decided in polynomial verification oracle calls.

We close our discussion on $\mathbb{B}$-SIM’s complexity, with some remarks on its relation with MER. In particular, [28] discusses a variant of MER, restricted to axis-aligned hyper-cubes, called Maximum Empty Square (MES). They also show that MES is NP-hard, for an arbitrary number of dimensions. However, in $\mathbb{B}$-SIM, we are given the center of the $\ell_\infty$-sphere. Following our terminology thus far, we would call the latter problem q-MES. Observe that despite MER and q-MER being computationally equal (both NP-hard), q-MES is properly easier than MES. Indeed, the dichotomic search method we described in Th. [theo:sound-max-cyclic] would also work for q-MES.

5.3 The Space of Uniform Interval Certifications↩︎

Let $\mathbb{B}(d)\vert_{\mathbf{x}}^{\mathbb{F}}$ be the set of all uniform intervals centered at $\mathbf{x}$. First we observe that $\mathbb{B}(d)\vert_{\mathbf{x}}^{\mathbb{F}} \subset \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$, since every uniform interval, is also an interval containing $\mathbf{x}$. However, the opposite does not hold. Moreover, $\mathbb{B}(d)\vert_{\mathbf{x}}^{\mathbb{F}}$ exhibits a more straightforward structure than $\mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$. Indeed, $\mathbb{B}(d)\vert_{\mathbf{x}}^{\mathbb{F}}$ form a totally ordered set, under set inclusion. Namely, for every $B_1, B_2 \in \mathbb{B}(d)\vert_{\mathbf{x}}^{\mathbb{F}}$, we have $B_1 \subseteq B_2$, iff $\rho_1 \leq \rho_2$, where $\rho_1, \rho_2$ the radii of $B_1, B_2$, respectively. Intuitively, this simpler structure is the reason for the differences in computational hardness between the two problems. Nevertheless, the richer solution space of $\mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$ provides non-trivial certifications to a strictly larger class of inputs.

For uniform intervals we can define $\bot_{\mathbb{B}}, \top_{\mathbb{B}}$-operations for $\mathbb{B}(d)\vert_{\mathbf{x}}^{\mathbb{F}}$, analogous to Sec. 4. To that end, consider a compact decision surface $\mathcal{D}_c \subseteq \mathbb{F}$ and an input $\mathbf{x} \in \mathcal{D}_c$. Let $\underline{\rho} > 0$ be the smaller distance between $\mathbf{x}$ and a counterexample $\mathbf{x}^\prime \notin \mathcal{D}_c$, and $\overline{\rho} > 0$ the greatest distance between $\mathbf{x}$ and another point $\mathbf{x}^{\prime\prime} \in \mathcal{D}_c$. Namely, \[\label{eq:cyclic-radii} \underline{\rho} = \inf \{\|\mathbf{x} - \mathbf{x}^\prime\|_\infty \mid \mathbf{x}^\prime \notin \mathcal{D}_c\}, ~~\overline{\rho} = \sup \{\|\mathbf{x} - \mathbf{x}^{\prime\prime}\|_\infty \mid \mathbf{x}^{\prime\prime} \in \mathcal{D}_c\}\tag{8}\] We define $\mathcal{D}_c\bot_{\mathbb{B}}\mathbf{x} = [\mathbf{x} - \underline{\rho}\mathbf{1}, \mathbf{x} + \underline{\rho}\mathbf{1}]$ and $\mathcal{D}_c\top_{\mathbb{B}}\mathbf{x} = [\mathbf{x} - \overline{\rho}\mathbf{1}, \mathbf{x} + \overline{\rho}\mathbf{1}]$. The following (set-theoretic) inequality relates the $\bot, \top$-operators in uniform and general intervals. For disambiguation, here we denote these operations with $\bot_{\mathbb{I}}, \top_{\mathbb{I}}$ for general intervals. \[\label{eq:bot-top-inequality} \mathcal{D}_c\bot_{\mathbb{B}}\mathbf{x} \subseteq \mathcal{D}_c \bot_{\mathbb{I}} \mathbf{x} \subseteq \mathcal{D}_c \subseteq \mathcal{D}_c \top_{\mathbb{I}} \mathbf{x} \subseteq \mathcal{D}\top_{\mathbb{B}}\mathbf{x}\tag{9}\] Noteworthy, for uniform intervals we have $\mathcal{D}_c\bot_{\mathbb{B}}\mathbf{x} = [\mathcal{D}_c\bot_{\mathbb{B}}\mathbf{x}]$. Since an objective $\omega(\cdot)$ respects set inclusion, $\omega(\mathcal{D}_c\bot_{\mathbb{B}}\mathbf{x}) \leq \omega(\mathcal{D}_c \bot_{\mathbb{I}} \mathbf{x}) \leq \omega(\mathcal{D}_c) \leq \omega(\mathcal{D}_c \top_{\mathbb{I}} \mathbf{x}) \leq \omega(\mathcal{D}\top_{\mathbb{B}}\mathbf{x})$. In Sec. 6, we implement the $\bot, \top$-operators both for uniform and general interval certifications. We observe that the minimum edge length of a general interval certification is, on average, about twice greater than the same objective in uniform intervals.

6 Implementation↩︎

Here, we examine the implementation and practical implications of the theoretical framework discussed earlier. We developed the open source system Parallele-pipedoNN. This system implements the operators discussed in Sec. 3, 4, and Appendix 10. In particular, Algorithm [algo:generic-traversal] with BUS policy implements the $\top$-operator, while the $\bot$-operator is implemented in the Algorithm [algo:generic-traversal] with TDS policy method. Recall that BUS policy is obtained by applying the parameters $I_0 = [\mathbf{x}, \mathbf{x}]$, $\varphi_{I, \mathcal{N}} = \mathscr{C}_{I, N}$, and $\square = \sqcup$. On the other hand, TDS is obtained for the parameters $I_0 = \mathbb{F}$, $\varphi_{I, \mathcal{N}} = \mathscr{S}_{I, N}$, and $\square = /$. Moreover, since Algorithm [algo:non-det-expand] is non-deterministic, we implemented a deterministic Sequential Dichotomic Expansion (SDE) method, presented in Appendix 10. SDE ensures maximality. Additionally, we include in our analysis evaluations regarding Algorithm [algo:generic-traversal] with either BUS or TDS policies for the case of uniform intervals. We denote these special cases of the algorithms as $\mathbb{B}$-BUS and $\mathbb{B}$-TDS, respectively. In Tbl. ¿tbl:tab:algorithms?, we overview the presented algorithms. For minimal complete certifications, we presented two algorithms, BUS and $\mathbb{B}$-BUS, for general and uniform intervals, respectively. Recall that the minimal complete uniform interval certification is not complete. SDE computes maximally sound interval certifications. TDS ensures voluminosity, under the assumption of Prop. [prop:non-triviality-lb]. Combining these two practices, we have a voluminous and maximally sound certification. Finally, $\mathbb{B}$-TDS computes maximally complete certifications for uniform intervals. Naturally, $\mathbb{B}$-TDS also ensures voluminosity, under the same conditions of Prop. [prop:non-triviality-lb]. For complete certifications, voluminosity is irrelevant. A complete interval will always have volume if $\mathcal{D}_c$ has volume. Our experiments provide counterexamples for voluminosity in SDE.

width=

6.1 Experimental Evaluation↩︎

Below we describe our experimental setup.

Hardware.: The experiments were performed in parallel on an Ubuntu 18.04 machine, with Intel Xeon E5-2640 v4 CPU, at 2.394GHz, with 38 cores, with 128GB RAM. The experiments ran in parallel, utilizing 35 cores.
Software Dependencies.: Our software is written in Python v3.8.16. The soundness and completeness of the oracles of eq. 3 and eq. 4 respectively, are implemented using the Marabou v2.0 ⁹ NN verifier. Our implementation takes as input a multilayered perceptron in open neural network exchange (ONNX) v1.16.0¹⁰ format. For linear algebra computations, we used the NumPy v1.23.5¹¹ library. For visualization, we used the Matplotlib v3.7.2¹² library. The MLPs used in the experiments were trained from scratch, using TensorFlow v2.12.0¹³.
Algorithms’ Parameters.: We evaluated all the algorithms of Tbl. ¿tbl:tab:algorithms? using the same parameters. We set the precision constant $\delta$ to $0.1$. We also set a timeout variable to 1 hour. For TDS+SDE the timeout is 2 hours, 1 hour for each component. The maximum number of iterations was set to 10,000.
Training Dataset.: We use 2 datasets, namely MNIST [32] and Fashion MNIST [33]. Both datasets consist of 28$\times$28, grayscale images, belonging to 10 classes. However, Fashion MNIST images are significantly more complex than MNIST.
Neural Networks.: We consider the following MLP architecture. applied our algorithms to 2 MLPs, of the same architecture, trained on the MNIST and Fashion MNIST datasets, respectively. Including the input and output layers, we have the architecture $\langle 784, 32, 10, 10 \rangle$, w.r.t. Def. 1. This corresponds to 25,450 trainable parameters. For training, we used the Adam [34] algorithm, Glorot [35] weight initialization, and the Categorical Crossentropy loss. By training on the 2 datasets above, this results in two MLPs, achieving $94\%$ and $82\%$ test-set accuracy for the MNIST and Fashion MNIST, respectively.
Inputs.: For each MLP, we randomly choose 5 images of the 10 classes of the test set (a total of 50 images per MLP).

width=

Tbl. ¿tbl:tab:experiments? reports descriptive statistics on the CPU time, the number of verification oracle calls, and the interval’s minimum edge length $\alpha(\cdot)$. We evaluate all six algorithms presented in this paper on both datasets. Overall, the empirical results align with our theoretical analysis. In particular, $\mathbb{B}$-BUS and $\mathbb{B}$-TDS are approximately an order of magnitude faster than their general-intervals counterpart, as expected, since they do not scale with the input dimension. This speed-up, however, comes at a cost, namely, $\mathbb{B}$-TDS attains only about half of the minimum edge length achieved by TDS (or roughly two-thirds on Fashion-MNIST). Finally, we observe that the Fashion MNIST MLP appears, on average, more robust that the MNIST MLP, despite achieving lower classification accuracy. This is consistent with prior findings, obtained via different methodologies, on the robustness-accuracy trade-off [36]–[39]. More detailed statistical results are provided in Appendix 11.

7 Conclusions & Future Work↩︎

This work develops a framework for computing maximally sound and minimally complete interval certifications for MLPs. In Sec. 4, we explore the interval certifications lattice, defining the $\top,\bot,[\cdot]$ operators. We develop algorithms that guarantee minimum completeness (Th. [theo:algo-min-complete]) and maximal soundness (Th. [theo:algo-max-sound], [theo:non-det-expand]). In Sec. 5, we study optimization on interval certifications. We observe intriguing asymmetries. The minimum complete certification can be computed in polynomial oracle calls. However, we extend previous results, by showing a stronger intractability result for sound maximization (Th. [theo:sound-max-hard]). Nevertheless, when optimization problems, are restricted to uniform intervals ($\ell_\infty$–spheres) become solvable in logarithmic number of oracle calls. Finally, we implement our theoretical insights in the ParallelelpipedoNN system, (Sec. 6), which we evaluate on MNIST and Fashion MNIST. As future work, we plan to extend our analysis to more general polyhedral certifications.

8 Omitted proofs↩︎

8.1 Proofs of Section 3 ↩︎

Proof. Applying straightforward computations we take, \[\begin{align} \mathcal{A}(I) & = \|b_i - \ell_i\|_{\infty} = \frac{1}{d}\sum_{i \in [d]}\max_{i \in [d]}\{u_i - \ell_i\} &&& \\ & \geq \frac{1}{d}\sum_{i \in [d]} u_i - \ell_i && \left[ \text{ equals } \frac{1}{d} \pi(I)\right] \\ & \geq \sqrt[d]{\prod_{i \in [d]} u_i - \ell_i} && \left[\begin{array}{l} \text{by arithmetic-geometric} \\ \text{mean inequality. Equals } \sqrt[d]{v(I)} \end{array} \right]\\ & \geq \sqrt[d]{\left(\min_{i \in [d]} \{u_i - \ell_i\}\right)^d} && \left[ \text{ equals } \alpha(I))\right]. \end{align}\]

$\hfill\Box$ ◻

Proof. Consider any interval $J = [\boldsymbol{\ell}', \boldsymbol{u}'] \subseteq I$ such that $\mathbf{x}' \notin J$. Since $\mathbf{x}' \notin J$, there exists at least one coordinate $i \in [d]$ such that either $u'_i < x'_i$ or $\ell'_i > x'_i$. In either case, the length of $J$ along coordinate $i$ satisfies $u'_i - \ell'_i \leq \max\{x'_i - \ell_i, \;u_i - x'_i\}$.

Let $k \in [d]$ be the coordinate selected in Definition 3, that is $k = \arg\max_{i \in [d]} |x_i - x'_i|$. By construction, the interval $I/\mathbf{x}'$ is obtained by shrinking $I$ only along coordinate $k$. Therefore, we have \[\alpha(I/\mathbf{x}') = \min \left\{ \min_{i \neq k}(u_i - \ell_i), \;\max\{x'_k - \ell_k, \;u_k - x'_k\} \right\}.\] Since $J \subseteq I$, we have $u'_i - \ell'_i \le u_i - \ell_i$ for all $i \in [d]$, and since $J$ excludes $\mathbf{x}'$, at least one coordinate must satisfy \[u'_i - \ell'_i \leq \max_{i \in [d]}\{x'_i - \ell_k, \;u_k - x'_i\} \leq \max\{x'_k - \ell_k, \;u_k - x'_k\}.\] Therefore, we have $\alpha(J) = \min_{i \in [d]}\{u'_i - \ell'_i\} \leq \alpha(I/\mathbf{x}')$, and the proof is complete.
$\Box$ ◻

8.2 Proofs of Section 4 ↩︎

Proof. Let $\mathbf{y} \not\in I$. Then there exists a coordination $i$ such that either $y_i < x_i - \underline{R}_i$ or $y_i > x_i + \overline{R}_i$. By formulas [def:top-operator], no point of $\mathcal{D}_c$ extends further in that direction. Hence, $\mathbf{y} \not\in \mathcal{D}_c$, and therefore $\kappa(\mathbf{y}) \neq c$. Since exiting the interval necessarily the prediction changes, we establish completeness.

Let $J = [\boldsymbol{\ell}, \boldsymbol{u}]$ be any complete certification containing $\mathbf{x}$, implying that for each coordinate $i$, we have \[\ell_i \leq \min \{x'_i \mid \mathbf{x}' \in \mathcal{D}_c\}, \quad u_i \geq \max \{x'_i \mid \mathbf{x}' \in \mathcal{D}_c\}.\] Thus, it holds $\mathcal{D}_c \top \mathbf{x} \subseteq J$. If the inclusion were strict, then there would exist a point outside $\mathcal{D}_c$ still inside $J$, violating completeness. Therefore, we conclude that $J = \mathcal{D}_c \top \mathbf{x}$.

Let $\mathbf{x}_1, \mathbf{x}_2 \in \mathcal{D}_c$. Observe that the radii $\underline{\mathbf{R}}$ and $\overline{\mathbf{R}}$ depend only on the extremal coordinates of $\mathcal{D}_c$, not on the choice of $\mathbf{x}$. Changing the reference point $\mathbf{x}$ shifts both endpoints equally, leaving the interval invariant. Hence, it holds $\mathcal{D}_c\top\mathbf{x}_1 = \mathcal{D}_c\top\mathbf{x}_2$, and the proof is complete.

$\hfill\Box$ ◻

Proof. Let $I_j = [-\boldsymbol{\ell}^j, \boldsymbol{u}^j]$, $\boldsymbol{\ell}^j, \boldsymbol{u}^j \geq \mathbf{0}$, $j \in \mathbb{N}$, be the interval in the $j$-th iteration of the Algorithm [algo:generic-traversal], when we apply the property $\mathscr{C}_{\mathcal{N}, I}(\mathbf{x}^\prime)$ and the operator $\sqcup$. Consider some $k \in \mathbb{N}$, s.t. $I_k = I_{k+1}$. W.l.o.g., let $k$ be the smallest natural with the latter property. For $I_k$ holds that $I_k \supseteq \mathcal{D}$, otherwise the $\mathscr{C}_{\mathcal{N}, I}(\mathbf{x}^\prime)$ oracle would find a counterexample $\mathbf{x}^a$, and $I_k \neq I_k \sqcup \mathbf{x}^a$, for each $\mathbf{x}^a \in I_k$. Under this configuration, the Algorithm [algo:generic-traversal] terminates after a finite number of steps, with $I_k \supseteq \mathcal{D}$. Moreover, since $\mathcal{D}_c\top\mathbf{x}$ is the unique complete certification it holds $I_k \supseteq \mathcal{D}_c\top\mathbf{x}$.

Moreover, for each $j \in [k]$, let $\mathbf{x}^j$ be the $j$-th counterexample returned from the $\mathscr{C}_{I, \mathcal{N}}(\mathbf{x}^\prime)$ oracle, s.t. $I_{j - 1} \sqcup \mathbf{x}^j = I_j$, and $I_0 = [\mathbf{0}, \mathbf{0}]$. For each $j \in [k]$, we have a strictly increasing sequence of intervals $I_0 \subset I_1 \subset \cdots \subset I_k$, since $I_{j - 1} \subset I_{j - 1} \sqcup \mathbf{x}^j = I_j$. Consider the set of the first $j$ witnesses returned by the oracle, $\mathcal{X}_j = \{\mathbf{x}^i \mid i \in [j]\}$. Naturally, $\mathcal{X}_1 \subset \mathcal{X}_2 \subset \cdots \subset \mathcal{X}_k$. For the $j$-th iteration, and the $i$-th coordinate, consider the values \[\label{eq:algo-min-complete} \underline{\theta}^j_i = \max \{-x^a_i \mid \mathbf{x}^a \in \mathcal{X}_j\}, \quad \overline{\theta}^j_i = \max \{x^a_i \mid \mathbf{x}^a \in \mathcal{X}_j\}.\tag{10}\] Clearly, it holds $\underline{\theta}^j_i, \overline{\theta}^j_i \geq 0$. Since, $\mathcal{X}_j \subset \mathcal{D}$, for each $j \in [k]$, there exist at least one index $i \in [d]$, s.t. $\underline{R}_i \leq \underline{\theta}^j_i$ and $\overline{\theta}^j_i \leq \overline{R}_i$. Next, for the $j$-th iteration, and for every $i \in [d]$, the $\sqcup$ implies that $\ell^j_i = \underline{\theta}^j_i + \delta$ and $u^j_i = \overline{\theta}^j_i + \delta$. Therefore, for each $j \in [k]$ we have $\ell^j_i \geq \underline{R}_i + \delta$ and $u^j_i = \overline{R}_i + \delta$, concluding that $I_k \subseteq \mathcal{D}_c\top\mathbf{x} + [-\delta \mathbf{1}, \delta \mathbf{1}]$.

Finally, we show the complexity of the Algorithm [algo:generic-traversal], when we apply the property $\mathscr{C}_{I, \mathcal{N}}(\mathbf{x}^\prime)$ and the operator $\sqcup$. Consider the potential function $\Phi([-\boldsymbol{\ell}, \boldsymbol{u}]) = \sum_{i\in [d]} \ell_i + u_i$, for $\boldsymbol{\ell}, \boldsymbol{u}\geq \mathbf{0}$. For each $j \in [k]$, the coordinate $i$, s.t. $\ell^j_i \leq \ell^{j - 1}_i + \delta$ or $u^j_i \leq u^{j - 1}_i + \delta$. Thus, $\Phi(I_j) \leq \Phi(I_{j-1}) + \delta$, and $\Phi(I_0) = \Phi([\mathbf{0}, \mathbf{0}]) = 0$. Now, from Prop. [prop:numerical-geometric-mean] it holds, $\Phi(I_k) = \sum_{i\in [d]} \ell^k_i + u^k_i \leq d \cdot \mathcal{A}(I_k)$. Hence, we take $\Phi(I_k) \leq d \cdot \mathcal{A}(\mathcal{D}_c\top\mathbf{x} + [-\delta \mathbf{1}, \delta \mathbf{1}]) \leq d \cdot \left(\mathcal{A}(\mathcal{D}_c\top\mathbf{x}) + 2\delta \right)$. So, we have $T = [\Phi(I_k) - \Phi(I_0)]/\delta = O(d \cdot \left(\mathcal{A}(\mathcal{D}_c\top\mathbf{x}) + 2\delta - 0 \right)/\delta) = O(d \cdot \left(\mathcal{A}(\mathcal{D}_c\top\mathbf{x})\right)/\delta)$.

$\hfill\Box$ ◻

Proof. For sake of contradiction, let $\mathbf{x}^a \in \mathcal{D}\bot\mathbf{0} \setminus \mathcal{D}$. Since $\mathbf{x}^a \in \mathcal{D}\bot\mathbf{0}$, for each $i \in [d]$, it holds that $-\underline{r}_i\leq x^a_i \leq \overline{r}_i$. Consider some $j \in [d]$, s.t. $\mathbf{x}^a \in \underline{V}_j$ or $\mathbf{x}^a \in \overline{V}_j$ (but not both, since $\mathbf{x}^a \neq \mathbf{0}$). Let $\mathbf{x}^a \in \underline{V}_j$. Then, $\underline{r}_j < -x^a_j$, or $-\underline{r}_j > x^a_j$. A contradiction. When $\mathbf{x}^a \in \overline{V}_j$, we work similarly.

$\hfill\Box$ ◻

Proof. Let $I_j = [-\boldsymbol{\ell}^j, \boldsymbol{u}^j]$, $\boldsymbol{\ell}^j, \boldsymbol{u}^j \geq \mathbf{0}$, $j \in \mathbb{N}$, be the interval in the $j$-th iteration of the Algorithm [algo:generic-traversal], when we apply the property $\mathscr{S}_{\mathcal{N}, I}(\mathbf{x}^\prime)$ and the operator $\sqcap$. W.l.o.g., let $k$ be the smallest natural with the latter property. For $I_k$ holds that $I_k \subseteq \mathcal{D}$. Otherwise, the soundness oracle $\mathscr{S}_{\mathcal{N}, I}(\mathbf{x}^\prime)$ would find a counterexample $\mathbf{x}^a$. And $I_k \neq I_k \sqcap\mathbf{x}^a$, for each $\mathbf{x}^a \in I_k$. Therefore, Algorithm [algo:generic-traversal] terminates after a finite number of steps, with $I_k \subseteq \mathcal{D}$.

Moreover, for each $j \in [k]$, let $\mathbf{x}^j$ be the $j$-th counterexample returned by the $\mathscr{S}_{I, \mathcal{N}}(\mathbf{x}^\prime)$ oracle, s.t. $I_{j-1} \sqcap \mathbf{x}^j = I_{j}$, and $I_0 = \mathbb{F}$. For each $j \in [k]$, we have a strictly decreasing sequence of intervals $I_0 \supset I_1 \supset \cdots \supset I_k$, since $I_{j-1} \supset I_{j-1} \sqcap \mathbf{x}^j = I_{j}$. Consider the set of the first $j$ witnesses returned by the oracle, $\mathcal{X}_j = \{\mathbf{x}^i \mid i \in [j]\}$. Naturally, $\mathcal{X}_1 \subset X_2 \subset \cdots \subset \mathcal{X}_k$. For the $j$–th iteration, and the $i$–th coordinate, consider the values \[\label{eq:algo-max-sound} \underline{\tau}^j_i = \min\{x^a_i \mid \mathbf{x}^a \in \underline{V}_i \cap \mathcal{X}_j\}, \quad \overline{\tau}^j_i = \min\{x^a_i \mid \mathbf{x}^a \in \overline{V}_i \cap \mathcal{X}_j\}\tag{11}\] Now, applying the operator $\sqcap$ to intervals $[-\boldsymbol{\ell}, \boldsymbol{u}]$ and $[\mathbf{x}^a, \mathbf{x}^a]$, for any $\mathbf{x}^a \in \mathbb{R}^d$, we have \[\label{eq:specification-op} \begin{cases} \ell^\prime_i = x^a_i - \delta, & \text{if}~~ \mathbf{x}^a \in \underline{V}_i \cap [-\boldsymbol{\ell}, \boldsymbol{u}],\\ u^\prime_i = x^a_i - \delta, & \text{if}~~ \mathbf{x}^a \in \overline{V}_i \cap [-\boldsymbol{\ell}, \boldsymbol{u}]. \end{cases}\tag{12}\] Otherwise, $[-\boldsymbol{\ell}, \boldsymbol{u}] =[-\boldsymbol{\ell}, \boldsymbol{u}] \sqcap \mathbf{x}^a$, when $\mathbf{x}^a \notin [-\boldsymbol{\ell}, \boldsymbol{u}]$. If $\mathbf{x}^a \in \underline{V}_i$, we update the $i$-th value of $\boldsymbol{\ell}$ to be $x^a_i - \delta$. Symmetrically, if $\mathbf{x}^a \in \overline{V}_i$, we update the $i$-th value of $\boldsymbol{u}$ to be $x^a_i - \delta$.

Since, $\mathcal{X}_j \subset \mathbb{F}\setminus \mathcal{D}$, we have $\underline{r}_i\leq \underline{\tau}_i^j$ and $\overline{r}_i\leq \overline{\tau}_i^j$, for each $j \in [k]$. From eq. 12 , for the $j$-th iteration, and the $i$-th coordinate, we have $\ell^j_i = \underline{\tau}^j_i - \delta$ and $u^j_i = \overline{\tau}^j_i - \delta$. Thus, for each $j \in [k]$ we have $\ell^j_i \geq \underline{r}_i- \delta$ and $u^j_i \geq \overline{r}_i- \delta$. Therefore, $I_k \supseteq \mathcal{D}\bot\mathbf{x} - \delta\mathbf{1}$.

Finally, we show the GenericTraversal algorithm’s complexity. Consider the potential function $\Phi([-\boldsymbol{\ell}, \boldsymbol{u}]) = \sum_{i \in [d]} \ell_i + u_i$, for $\boldsymbol{\ell}, \boldsymbol{u}\geq \mathbf{0}$. For each $j \in [k]$, there is a coordinate $i$, s.t. $\ell^j_i \leq \ell^{j-1}_i - \delta$ or $u^j_i \leq u^{j-1}_i - \delta$. Thus, $\Phi(I_j) \leq \Phi(I_{j-1}) - \delta$. Additionally, $\Phi(I_0) = d\cdot\mathcal{A}(\mathbb{F})$, and $\Phi(I_k) \geq d\cdot\mathcal{A}(\mathcal{D}\bot\mathbf{x}) - \delta$. Hence, for the complexity of the Algorithm [algo:generic-traversal], we have $T = [\Phi(I_0) - \Phi(I_k)]/\delta = O(d[\mathcal{A}(\mathbb{F}) - \mathcal{A}((\mathcal{D}\bot\mathbf{x}) + \delta]/\delta) = O(d[\mathcal{A}(\mathbb{F}) - \mathcal{A}(\mathcal{D}\bot\mathbf{x})]/\delta)$.

$\hfill\Box$ ◻

Proof. If $\mathbf{x} \in \mathcal{D}^\circ_c$, then there is some $\rho > 0$, s.t. $\mathcal{B}^{\infty}(\mathbf{x}, \rho) \subseteq \mathcal{D}$. Choose $\rho$ to be the greatest real number s.t. the previous statement holds. Then, for each $i \in [d]$ holds $\underline{r}_i, \overline{r}_i\geq \rho > 0$. Thus, $\alpha(\mathcal{D}_c\bot\mathbf{x}) > 0$.

$\hfill\Box$ ◻

Proof. $[\Rightarrow]$ We prove the contrapositive. Let some $i \in [d]$ and some $\delta > 0$, s.t. either $[-(\boldsymbol{\ell}+ \delta\mathbf{e}^i), \boldsymbol{u}] \setminus \mathcal{D}_c = \varnothing$ or $[-\boldsymbol{\ell}, \boldsymbol{u}+ \delta\mathbf{e}^i] \setminus \mathcal{D}_c = \varnothing$ (or both). W.l.o.g. let $[-(\boldsymbol{\ell}+ \delta\mathbf{e}^i), \boldsymbol{u}] \setminus \mathcal{D}_c = \varnothing$. Since $[-(\boldsymbol{\ell}+ \delta\mathbf{e}^i), \boldsymbol{u}] \supset [-\boldsymbol{\ell}, \boldsymbol{u}]$, then $[-\boldsymbol{\ell}, \boldsymbol{u}]$ is not maximal.

$[\Leftarrow]$ Let for every $i \in [d]$, and every $\delta > 0$, we assume that holds, $[-(\boldsymbol{\ell}+ \delta\mathbf{e}^i), \boldsymbol{u}] \setminus \mathcal{D}_c \neq \varnothing$ and $[-\boldsymbol{\ell}, \boldsymbol{u}+ \delta\mathbf{e}^i] \setminus \mathcal{D}_c \neq \varnothing$. Now assume some $I^\prime \supset I = [-\boldsymbol{\ell}, \boldsymbol{u}]$. There are $i \in [d]$ and $\delta > 0$, s.t. $I^\prime \supseteq [-(\boldsymbol{\ell}+ \delta\mathbf{e}^i), \boldsymbol{u}]$ or $I^\prime \supseteq [-\boldsymbol{\ell}, \boldsymbol{u}+ \delta\mathbf{e}^i]$ (or both). Therefore, $I^\prime \setminus \mathcal{D}_c \neq \varnothing$. Hence, $I$ is maximal.

$\hfill\Box$ ◻

Proof. We start from the trivial sound certification $X = [\mathbf{x}, \mathbf{x}] \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$. Let, $I^\ast = [\boldsymbol{\ell}^\ast, \boldsymbol{u}^\ast] \in [X]$ be an arbitrary maximally sound interval. Observe that Algorithm [algo:non-det-expand], at each iteration, expands exactly one coordinate of either the lower or upper endpoint by $\delta$. Therefore, it performs monotone expansions of the current interval $I$. Thus, the algorithm defines a monotone path in the interval lattice $\langle \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}, \subseteq \rangle$, starting from $X$.

Next, we consider the following non-deterministic strategy: i) if the algorithm expands a coordinate $k$ of the lower endpoint, then it chooses $k$ s.t. $\ell_k < \ell^\ast_k$, and ii) if the algorithm expands a coordinate $k$ of the upper endpoint, then it chooses $k$ s.t. $u_k < u^\ast_k$. As long as the current interval $I$ satisfies $I \subseteq I^\ast$, all expansions are sound. Since each coordinate is expanded in increments of size $\delta$, after at most \[\left\lceil \frac{u^\ast - x_k}{\delta} \right\rceil \quad \text{ or } \quad \left\lceil \frac{x_k - \ell^\ast}{\delta} \right\rceil\] steps per coordinate, the algorithm reaches an interval $J$ s.t. $I - [-\delta\mathbf{1}, \delta\mathbf{1}] \subseteq J \subseteq I$. Observe that, by Lem. [lem:maximal-soundness], for every coordinate $i$ and every $\delta > 0$, any further unilateral expansion beyond $I^\ast$ results in a counterexample.

Finally, for the complexity, there are $2d$ coordinates of all endpoints, and they can be expanded at most $O(1/\delta)$ times. Each expansion requires one call in the soundness oracle $\mathscr{S}_{I, \mathcal{N}}(\mathbf{x}^\prime)$, costing $\mathcal{A}(\mathbb{F})$. Therefore, the total number of non-deterministic steps is \[O \left( d \cdot \frac{\mathcal{A}(\mathbb{F})}{\delta}\right),\] and the proof is complete.

$\hfill\Box$ ◻

8.3 Proofs of Section 5 ↩︎

Proof. The proof relies on a reduction from q-MER to SIM. Given an instance $\mathcal{I}$ in q-MER, we can construct an instance $\mathcal{I}'$ in SIM as follows. Let $\mathbf{x} := \mathbf{q}$, we define the decision surface $\mathcal{D}_c := \mathbb{F}\setminus \mathcal{F}$. Since the set $\mathcal{F}$ is finite and $\mathbb{F}$ is compact, the set $\mathcal{D}_c$ is compact as well. Next, we interpret every forbidden point $\mathbf{f} \in \mathcal{F}$ as a counterexample, that is, given the classifier $\kappa(\cdot)$, it holds $\kappa(\mathbf{f}) \neq c$. Using the terminology of the soundness oracle, eq. 3 , we have that $\mathbf{f} \models \mathscr{I}_{I, \mathcal{N}}(\mathbf{f})$ for all points in $\mathcal{F}$. Contrarily, sound intervals are precisely those that exclude $\mathcal{F}$. Therefore, an interval $I \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}$, with $I \subseteq \mathcal{D}_c$, is sound iff $I \cap \mathcal{F} = \emptyset$. Since we have set $\mathbf{x} := \mathbf{q}$, and the objective constraint $v(I) \geq \gamma$, for $\gamma > 0$, is identical in both problems, the reduction is established. Hence, the $\mathcal{I}$ is feasible iff the $\mathcal{I}'$ is feasible. Since the problem q-MER can not be decided in polynomial time, the problem SIM can not be decided in polynomial time, as well, and the proof is complete.

$\hfill\Box$ ◻

Proof. Let $G = (V, E)$ a simple undirected graph with $|V| = d$. We fix any constant $w > 0$ and wlog we work on $[0, 1]^d$. From Lem. 2 in [28] if $I \subseteq [0, 1]^d$ is a maximum-volume feasible interval, then $\partial I$ contains $\mathbf{0}$ and the $i$-th dimension of $I$ is either $w$ or $1$. Therefore, the maximum-volume interval $I$ has $\ell_i = 0$ for every $i$, and each $u_i \in \{w, 1\}$, meaning that $I = [\mathbf{0}, \mathbf{u}]$. The interval $I$ has volume $v(I) = \prod_{i \in [d]} (u_i - \ell_i)$. Applying Th. 2 from [28], graph $G$ has an independent set of size at least $k$ iff there exists an interval $I \in \mathbb{F}$ of volume at least $w^k$. Consequently, deciding whether there exists any empty interval of volume at least $w^k$ is NP-hard. Taking $\gamma = w^k$ and $\mathbf{q} = \mathbf{0}$, every interval of the form $[\mathbf{0}, \mathbf{u}]$ contains $\mathbf{q}$, so deciding the existence of an empty rectangle that contains the query point $\mathbf{q}$ with $v(I) \geq \gamma$ is NP-hard. Therefore, the q-MER decision problem is NP-hard, and the proof is complete.

$\hfill\Box$ ◻

Proof. We present an algorithm with executed in a logarithmic number of oracle calls in Algorithm 4. Essentially, we do a dichotomic search in the real interval $[0, \mathcal{A}(\mathbb{F})]$.

Figure 4: \mathbb{B}–TopDown Search — Figure 4: $\mathbb{B}$–TopDown Search

$\hfill\Box$ ◻

Note that Algorithm 4 can easily be modified to compute complete uniform certifications. We simply use the $\mathscr{C}_{B, \mathcal{N}}$ predicate, instead of $\mathscr{S}_{B, \mathcal{N}}$, and switching steps 6, 8.

9 Geometry of the $\mathbb{R}^d$ Cone Partition↩︎

In this section, we briefly discuss the geometry involved in the cone decomposition of $\mathbb{R}^d$, introduced in eq. 5 of Sec. 4. To that end, we firstly introduce some elementary concepts of affine geometry. Then we proceed to examine the intersections of these cones.

9.1 Elements of Affine Geometry↩︎

We begin with convex bodies. For $\boldsymbol{\ell}, \boldsymbol{u}\in \mathbb{R}^d$, the line segment with endpoints $\boldsymbol{\ell}$ and $\boldsymbol{u}$ is defined as $\text{L}(\boldsymbol{\ell}, \boldsymbol{u}) = \{\mathbf{x} \in \mathbb{R}^d \mid x = \boldsymbol{\ell}+ t\cdot(\boldsymbol{u}- \boldsymbol{\ell}), ~t\in [0, 1]\}$. A set $S \subseteq \mathbb{R}^d$ is said to be convex if $L(\boldsymbol{\ell}, \boldsymbol{u}) \subseteq S$ for every $\boldsymbol{\ell}, \boldsymbol{u}\in S$. A convex body is a convex and compact subset of $\mathbb{R}^d$ with nonempty interior. An important class of convex sets is the polyhedra. Let $A \in \mathbb{R}^{m \times n}$ and $\boldsymbol{u}\in \mathbb{R}^m$. The set $P = \{\mathbf{x} \in \mathbb{R}^n \mid A\mathbf{x} \leq \boldsymbol{u}\}$ is called a (convex) polyhedron. If $\boldsymbol{u}= \mathbf{0}$, we obtain a polyhedral cone $C = \{\mathbf{x} \in \mathbb{R}^m \mid A\mathbf{x} \leq \mathbf{0}\}$.

A set of vectors $\mathbf{v}_1, \dots, \mathbf{v}_n \in \mathbb{R}^d$ is affinely independent if the vectors $\left[ \mathbf{v}_1 \atop 1 \right]$, $\dots$, $\left[ \mathbf{v}_n \atop 1 \right]$ are linearly independent. The dimension of a polyhedron $P$, denoted $\mathsf{dim}(P)$, is the cardinality of the largest affinely independent subset of $P$ minus one. Given a polyhedron $P = \{\mathbf{x} \in \mathbb{R}^m \mid A\mathbf{x} \leq \boldsymbol{u}\}$ a face $F$ is another polyhedron $F = \{\mathbf{x} \in \mathbb{R}^n \mid A^\prime\mathbf{x} \leq \boldsymbol{u}^\prime\}$, where $A^\prime$ is a submatrix of $A$ and $\boldsymbol{u}^\prime$ is the respective subvector of $\boldsymbol{u}$. A facet is a face of $P$ with dimention $\mathsf{dim}(P) - 1$.

9.2 Intersections of Cones↩︎

Figure 5: Cone Decomposition of \mathbb{R}^3. The polyhedral cones of eq. 5 , correspond to pyramids is \mathbb{R}^3. Left: The \underline{V}_1, \overline{V}_1 cones of the x_1–axis. Observe that \underline{V}_1 \cap \overline{V}_1 = \{\mathbf{0}\}. Right: The cone decomposition , of the entire \mathbb{R}^3. — Figure 5: Cone Decomposition of $\mathbb{R}^3$. The polyhedral cones of eq. 5 , correspond to *pyramids* is $\mathbb{R}^3$. Left: The $\underline{V}_1, \overline{V}_1$ cones of the $x_1$–axis. Observe that $\underline{V}_1 \cap \overline{V}_1 = \{\mathbf{0}\}$. Right: The cone decomposition , of the entire $\mathbb{R}^3$.

To gain intuition about the underlying problem, we present the cone decomposition of $\mathbb{R}^3$ in Fig. 5. Our focus is on the intersection of a collection of cones. We express the cones of eq. 5 as a set of inequalities. For each $i \in [d]$, let $\underline{U}_i, \overline{U}_i \in \mathbb{R}^{d \times d}$ denote two associated matrices. For the matrix $\underline{U}_i$, every element of the $i$-th column is $-1$. For all $m \neq n$ the entry, we have $(\underline{u}_i)_{mn} = 0$. Finally, for $n \neq i$, the diagonal entries satisfy $(\underline{u}_i)_{nn} = -1$. For $\overline{U}_i$, the construction is identical, except that every element in the $i$-th column equals $+1$. All other entries coincide with those of $\underline{U}_i$. In Fig. 6, we give an example when $d = 4$. With this notation in place, the cones from eq. 5 can now be written equivalently in the form, \[\label{eq:cones-2} \underline{V}_i = \{\mathbf{x} \in \mathbb{R}^d \mid \underline{U}_i\mathbf{x} \geq \mathbf{0} \}, \quad\overline{V}_i = \{\mathbf{x} \in \mathbb{R}^d \mid \overline{U}_i\mathbf{x} \geq \mathbf{0} \}.\tag{13}\]

Figure 6: Left, Middle: The matrices \underline{U}_2,\overline{U}_3 \in \mathbb{R}^{4\times 4}, for the cones \underline{V}_2, \overline{V}_2. It holds that \underline{V}_2 \cap \overline{V}_3 = \{\mathbf{x} \in \mathbb{R}^d \mid \underline{\overline{U}}_{23}\mathbf{x} \geq \mathbf{0}\}. — Figure 6: Left, Middle: The matrices $\underline{U}_2,\overline{U}_3 \in \mathbb{R}^{4\times 4}$, for the cones $\underline{V}_2, \overline{V}_2$. It holds that $\underline{V}_2 \cap \overline{V}_3 = \{\mathbf{x} \in \mathbb{R}^d \mid \underline{\overline{U}}_{23}\mathbf{x} \geq \mathbf{0}\}$.

Eq. 13 is equivalent to eq. 5 . Note that for each $i \in [d]$, the cones $\underline{V}_i$ and $\overline{V}_i$ both have full dimension, that is $\mathsf{dim}(\underline{V}_i) = \mathsf{dim}(\overline{V}_i) = d$. Indeed, the rows of $\underline{U}_i$ form a set of $d$ linearly independent vectors. Together with the origin, these yield $d+1$ affinely independent vectors, confirming that $\underline{V}_i$ has dimension $d$. An identical argument applies to $\overline{V}_i$.

Next, consider the intersection $\overline{V}_i \cap \overline{V}_j$ for distinct indices $i \neq j$. For any $\mathbf{x} \in \overline{V}_i \cap \overline{V}_j$ it must holds $\overline{U}_i\mathbf{x} \geq \mathbf{0}$ and $\overline{U}_j\mathbf{x} \geq \mathbf{0}$. Thusly, we can define a matrix $\overline{U}_{ij}$, s.t. holds $\overline{U}_{ij}\mathbf{x} \geq \mathbf{0}$, iff $\overline{U}_i\mathbf{x} \geq \mathbf{0}$ and $\overline{U}_j\mathbf{x} \geq \mathbf{0}$. Concretely, $\overline{U}_{ij}$ is obtained from $\overline{U}_i$ by replacing the $j$-th column with all ones, while leaving all other entries unchanged. Hence, $\overline{V}_i \cap \overline{V}_j = \{\mathbf{x} \in \mathbb{R}^d \mid \overline{U}_{ij} \mathbf{x} \geq \mathbf{0}\}$. An example for $d=4$ is shown in Fig. 6. Geometrically, this intersection reduces the dimension by one, $\mathsf{dim}(\overline{V}_i\cap \overline{V}_j) = d - 1$. Analogous constructions hold for the intersections $\underline{V}_i\cap \overline{V}_j$ and $\underline{V}_i\cap \underline{V}_j$. This agrees with the geometric intuition from Fig. 5, since the intersection of two different pyramids in $\mathbb{R}^3$ is a facet.

10 Implementing the Maximal Closure Operator↩︎

In this section, we examine a deterministic expansion method for computing maximally sound interval certifications. Essentially, the Non–deterministic Expansion method, introduced in Sec. 4, and described in Algorithm [algo:non-det-expand], defines a collection of deterministic algorithms, each making different choices on the coordinate to expand next. In Algorithm 8, we describe a simple, novel¹⁴ and deterministic method, that expands each coordinate sequentially. At each step, we make a dichotomic (or binary) search to expand the $i$-th coordinate. Below, we establish the correctness and computational complexity of the above algorithm.

Figure 8: Sequential Dichotomic Expansion

The Sequential Dichotomic Expansion algorithm satisfies Lemma [lem:maximal-soundness]. Moreover, the algorithm terminates after $O(d\cdot\log(\mathcal{A}(\mathbb{F}))$ $\mathscr{S}_{I, \mathcal{N}}(\cdot)$ oracle calls.

Proof. Let $[-\boldsymbol{\ell}, \boldsymbol{u}]$ be the interval returned by the Sequential Dichotomic Expansion algorithm. We assume that $[-\boldsymbol{\ell}, \boldsymbol{u}] \subset \mathbb{F}$. We prove that Lemma [lem:maximal-soundness] is satisfied for the $i$–th coordinate of $\boldsymbol{u}$. The case for the other coordinates of $\boldsymbol{u}$ and the coordinates of $\boldsymbol{\ell}$ are symmetrical.

Consider the interval $[\mathtt{low}, \mathtt{high}]$ of step [algo-step:expand-dichotomic-ub-while]. We show that if there is a counterexample in $(0, \underline{U}_i]$, there is always a counterexample in $(\mathtt{low}, \mathtt{high}]$, throughout the execution of the algorithm. Let $\mathtt{low}_j$, $u_{ij}$, $\mathtt{high}_j$ denote the values of the variables, of the $j$–th iteration. We prove this fact using induction.

For the base step, $[\mathtt{low}_0, \mathtt{high}_0] = [0, \overline{U}_i]$. From our assumption, there is a counterexample $\mathbf{x}^a \in [\mathtt{low}_0, \mathtt{high}_0]$. Now assume that there is a counterexample in $[\mathtt{low}_j, \mathtt{high}_j]$. We show that there is a counterexample in $[\mathtt{low}_{j+1}, \mathtt{high}_{j+1}]$. Consider the variable $u_{i(j+1)}$ at the $(j+1)$–th iteration of the algorithm. It holds $u_{i(j+1)} = \mathtt{low}_j + (\mathtt{high}_j - \mathtt{low}_j)/2$. We take two cases, either there is a counterexample in $[\mathtt{low}_i, u_{i(j+1)}]$, or not.

If there is a counterexample in $[\mathtt{low}_j, u_{i(j+1)}]$, then $\mathtt{low}_{j+1} = \mathtt{low}_j$. Moreover, $\mathtt{high}_{j+1} = u_{i(j+1)}$. Hence, exists a counter example in $[\mathtt{low}_{j+1}, \mathtt{high}_{j+1}]$. Thus, we showed the desideratum.

Now, we consider the case that there is no counterexample in $[\mathtt{low}_j, u_{i(j+1)}]$. But, from the inductive hypothesis, there is a counterexample in $[\mathtt{low}_j, \mathtt{high}_j]$. Therefore, there must be a counterexample in $[u_{i(j+1)}, \mathtt{high}_{j}]$. In this case, we have $\mathtt{low}_{j+1} = u_{i(j+1)}$ and $\mathtt{high}_{j+1} = \mathtt{high}_j$. Thus, there still exists a counterexample in $[\mathtt{low}_{j+1}, \mathtt{high}_{j+1}]$.

From the step [algo-step:expand-dichotomic-ub-while] of the algorithm, the procedure terminates when $\mathtt{high} -\mathtt{low} \leq \delta$. Moreover, $\ell_i = \mathtt{low}$. From the above, there is a counterexample in $[\mathtt{low}, \mathtt{high}]$. Thus, there is a counterexample in $[\boldsymbol{\ell}, \boldsymbol{u}+ \delta\mathbf{e}^i]$.

Finally, each expansion operation will take at most $\log(\mathcal{A}(\mathbb{F}))$ steps. We make $d$ expansions. Moreover, the maximality of the returned solution is established by Lemma [lem:maximal-soundness]. $\hfill \Box$ ◻

11 More on Experimental Evaluation↩︎

In this appendix we review some additional statistics from the experiments presented in Sec. 6, providing additional insights on the details of algorithms.

11.1 MNIST↩︎

Figure 9: Minimum edge length of the certifications computed by each algorithm, per MNIST input point.

We begin from the MNIST dataset and the corresponding MLP. Tab. ¿tbl:tab:experiments-mnist-expanded? provides a detailed description of the metrics analyzed in Sec. 6. For each metric, we report the minimum (Min.), the average (Avg.), and the maximum (Max.) values. In addition, we report the percentage of the inputs that timed out; the percentage of time consumed by the verification oracles; and the percentage of the non-trivial solutions, returned by each algorithm. Fig. [fig:mnist-analytics] shows the achieved minimum edge length for each input and algorithm. Finally, in Tab. ¿tbl:tab:examples-MNIST? presents example images illustrating the computed bounds of the instance 7-4.

width=

From Tab. ¿tbl:tab:examples-MNIST?, we observe that the morphology of each bound strongly depends on the applied algorithm. Algorithms based on symmetric interval (i.e, $\ell_\infty$-spheres) induce a uniform distortion on the given input. In contrast, sequential algorithms, such as SDE, expand each pixel in turn, once further expansion of the previous pixel is no longer possible. This results in a highly imbalanced distortion of the input image. Finally, the TDS and BUS algorithms lay between these two extremes.

width=

11.2 Fashion MNIST↩︎

Figure 10: Minimum edge length of the certifications computed by each algorithm, per Fashion MNIST input point.

Subsequently, we focus on the Fashion MNIST dataset and the corresponding MLP. Tab. ¿tbl:tab:experiments-fashion-mnist-expanded? provides a detailed description of the metrics used, reporting the minimum, the average, maximum) values, along with its standard deviation, similar to Tab. ¿tbl:tab:experiments-mnist-expanded?. In addition, we report several percentage-based metrics. Fig. 10 reports the achieved minimum edge length obtained for each input and algorithm. Finally, Tab. ¿tbl:tab:examples-Fashion-MNIST? presents example images illustrating the computed bounds of the instance 7-4.

From Fig. 10, we observe that the BUS algorithm fails to compute a correct complete certification, whereas $\mathbb{B}$-BUS succeeds. We attribute this behavior to BUS’s sensitivity to the precision parameter $\delta$. As shown in Tab. ¿tbl:tab:examples-Fashion-MNIST?, the BUS algorithm behaves well; the small value of $\alpha$ is due to the involvement of only a few pixels.

width=

References↩︎

[1]

Y. Zhu et al., “Collaborative retrieval for large language model-based conversational recommender systems,” 2025.

[2]

DeepSeek-AI et al., “DeepSeek LLM: Scaling open-source language models with longtermism.” 2024.

[3]

D. Li, P. Auerbach, and O. Okhrin, “Autonomous driving small-scale cars: A survey of recent development,” IEEE Transactions on Intelligent Transportation Systems, 2025.

[4]

F. Ma, R. Chitta, J. Zhou, Q. You, T. Sun, and J. Gao, “Dipole: Diagnosis prediction in healthcare via attention-based bidirectional recurrent neural networks,” in ICKDDM, 2017.

[5]

A. Zuiderwijk, Y.-C. Chen, and F. Salem, “Implications of the use of artificial intelligence in public governance: A systematic literature review and a research agenda,” Government Information Quarterly, 2021.

[6]

I. J. Goodfellow, J. Shlens, and C. Szegedy, “Explaining and harnessing adversarial examples,” in ICLR, 2015.

[7]

M. H. Meng et al., “Adversarial robustness of deep neural networks: A survey from a formal verification perspective,” IEEE TDSC, 2022.

[8]

C. Szegedy et al., “Intriguing properties of neural networks,” in ICLR, 2014.

[9]

A. Madry, A. Makelov, L. Schmidt, D. Tsipras, and A. Vladu, “Towards deep learning models resistant to adversarial attacks,” in ICLR, 2018.

[10]

H. Zhang et al., “Towards stable and efficient training of verifiably robust neural networks,” in ICLR, 2020.

[11]

R. Ehlers, “Formal verification of piece-wise linear feed-forward neural networks,” in ATVA, 2017.

[12]

A. Kabaha and D. Drachsler-Cohen, “Maximal robust neural network specifications via oracle-guided numerical optimization,” in VMCAI, 2023.

[13]

C. Li et al., “Towards certifying the asymmetric robustness for neural networks: Quantification and applications,” IEEE TDSC, 2022.

[14]

C. Liu, R. Tomioka, and V. Cevher, “On certifying non-uniform bounds against adversarial attacks,” in ICML, 2019.

[15]

E. Wong and J. Z. Kolter, “Provable defenses against adversarial examples via the convex outer adversarial polytope,” in ICML, 2018.

[16]

M. Mirman, M. Baader, and M. T. Vechev, “The fundamental limits of neural networks for interval certified robustness,” Trans. Mach. Learn. Res., 2022.

[17]

H. Salman, G. Yang, H. Zhang, C.-J. Hsieh, and P. Zhang, “A convex relaxation barrier to tight robustness verification of neural networks,” in NeurIPS, 2019.

[18]

G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient SMT solver for verifying deep neural networks,” in CAV, 2017.

[19]

G. Katz et al., “The marabou framework for verification and analysis of deep neural networks,” in CAV, 2019.

[20]

H. Wu et al., “Marabou 2.0: A versatile formal analyzer of neural networks,” in CAV, 2024.

[21]

G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: A calculus for reasoning about deep neural networks,” Formal Methods Syst. Des., 2022.

[22]

H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,” in NeurIPS 2018, 2018.

[23]

T. Sunaga, “Theory of an interval algebra and its application to numerical analysis,” Research Association of Applied Geometry, 1958.

[24]

K. Fukushima, “Visual feature extraction by a multilayered network of analog threshold elements,” IEEE TSSC, 1969.

[25]

A. Lomuscio and L. Maganti, “An approach to reachability analysis for feed-forward ReLU neural networks,” CoRR, 2017.

[26]

R. E. Moore, R. B. Kearfott, and M. J. Cloud, Introduction to interval analysis. SIAM, 2009.

[27]

T. M. Chan, “Faster algorithms for largest empty rectangles and boxes,” Discret. Comput. Geom., 2023.

[28]

J. Backer and J. M. Keil, “The mono- and bichromatic empty rectangle and square problems in all dimensions,” in LATIN, 2010.

[29]

B. Chazelle, R. L. (Scot) Drysdale III, and D. T. Lee, “Computing the largest empty rectangle,” SIAM J. Comput., 1986.

[30]

A. Naamad, D. T. Lee, and W.-L. Hsu, “On the maximum empty rectangle problem,” Discrete Applied Mathematics, 1984.

[31]

G. Gutiérrez and J. R. Paramá, “Finding the largest empty rectangle containing only a query point in large multidimensional databases,” in SSDBM, 2012.

[32]

L. Deng, “The mnist database of handwritten digit images for machine learning research,” IEEE Signal Processing Magazine, 2012.

[33]

H. Xiao, K. Rasul, and R. Vollgraf, “Fashion-MNIST: A novel image dataset for benchmarking machine learning algorithms,” CoRR, 2017, [Online]. Available: http://arxiv.org/abs/1708.07747.

[34]

D. P. Kingma and J. Ba, “Adam: A method for stochastic optimization,” in ICLR, 2015.

[35]

X. Glorot and Y. Bengio, “Understanding the difficulty of training deep feedforward neural networks,” in AISTATS, 2010.

[36]

A. Madry, A. Makelov, L. Schmidt, D. Tsipras, and A. Vladu, “Towards deep learning models resistant to adversarial attacks,” in ICLR, 2018.

[37]

H. Zhang, Y. Yu, J. Jiao, E. P. Xing, L. E. Ghaoui, and M. I. Jordan, “Theoretically principled trade-off between robustness and accuracy,” in ICML, 2019.

[38]

D. Tsipras, S. Santurkar, L. Engstrom, A. Turner, and A. Madry, “Robustness may be at odds with accuracy,” in ICLR, 2019.

[39]

A. Raghunathan, S. M. Xie, F. Yang, J. C. Duchi, and P. Liang, “Understanding and mitigating the tradeoff between robustness and accuracy,” in ICML, 2020.

[40]

Y. Izza, A. Ignatiev, P. J. Stuckey, and J. Marques-Silva, “Delivering inflated explanations,” in AAAI, 2024.

https://github.com/merkouris148/parallelepipedonn ↩︎
Here we use the big-M formalization of [25]. Other formalizations have also been proposed, see the survey of [7].↩︎
https://www.gurobi.com ↩︎
Note that it does not hold that $\boldsymbol{\ell}< \boldsymbol{u}$ whenever $\boldsymbol{\ell}\leq \boldsymbol{u}$ and $\boldsymbol{\ell}\neq \boldsymbol{u}$.↩︎
In general, the $\arg\max\{\vert x_i - x^\prime_i \vert \mid i \in [d] \wedge \mathbf{x} \in \mathbb{I}(d)\vert^{\mathbb{F}}_{\mathbf{x}}\}$ may provide a set of indices, meaning that there are ties w.r.t. the smallest changes we can impose in the interval. Since, in any interval, any change in any dimension is orthogonal to any changes in any other dimension, we can apply any tie-breaking rule, e.g., lexicographic ordering.↩︎
Note that soundness and completeness of a MLP verifier, w.r.t. Sec.2 differ from soundness and completeness of an interval certification w.r.t. Def. 5.↩︎
Borrowing static analysis terminology.↩︎
A polyhedral cone is a set of the form $C = \{\mathbf{x} \in \mathbb{R}^n \mid A\mathbf{x} \leq \mathbf{0}\}$, where $A \in \mathbb{R}^{m \times n}$. We briefly explore the geometry of the cones and their intersections in Appendix 9.↩︎
See https://github.com/NeuralNetworkVerification/Marabou and [20].↩︎
See https://github.com/onnx/onnx.↩︎
See https://github.com/numpy/numpy.↩︎
See https://github.com/matplotlib/matplotlib.↩︎
See https://github.com/tensorflow/tensorflow.↩︎
The authors in [40] mention a dichotomic expansion as an alternative to their linear expansion algorithm. However, they do not give any details.↩︎

Minimum Edge Length:	\(\alpha(I)\)	\(= \min_{i \in [d]} u_i - \ell_i\)
Perimeter:	\(\pi(I)\)	\(= \sum_{i \in [d]} u_i - \ell_i\)
Volume:	\(v(I)\)	\(= \prod_{i \in [d]} u_i - \ell_i\).
Diameter:	\(\mathcal{A}(I)\)	\(= \max_{i \in [d]} u_i - \ell_i = \\|u_i - \ell_i\\|_\infty\)

Interval Certifications for Multilayered Perceptrons via Lattice Traversal

Abstract

1 Introduction↩︎

2 Preliminaries↩︎

2.0.0.1 Normed Vector Spaces.

2.0.0.2 Multilayered Perceptrons.

2.0.0.3 Formal MLP Verification.

3 Intervals in Higher Dimensions↩︎

3.1 Operations on Intervals & the Interval Lattice↩︎

3.2 Interval Objectives↩︎

4 Sound & Complete Interval Certifications↩︎

4.1 Verification Oracles↩︎

4.2 The Generic Traversal Algorithm↩︎

4.3 Minimally Complete Certifications via the \(\top\)–Operator↩︎

4.4 Edge Length Non-Triviality in Sound Certifications via the \(\bot\)-Operator↩︎

4.5 The Maximal Closure Operator \([I]\)↩︎

4.6 The Space of Interval Certifications↩︎

5 Optimization over Interval Certifications↩︎

5.1 On the Intractability of Sound Maximization↩︎

5.2 Sound Maximization on Uniform Intervals↩︎

5.3 The Space of Uniform Interval Certifications↩︎

6 Implementation↩︎

6.1 Experimental Evaluation↩︎

7 Conclusions & Future Work↩︎

8 Omitted proofs↩︎

8.1 Proofs of Section 3 ↩︎

8.2 Proofs of Section 4 ↩︎

8.3 Proofs of Section 5 ↩︎

9 Geometry of the \(\mathbb{R}^d\) Cone Partition↩︎

9.1 Elements of Affine Geometry↩︎

9.2 Intersections of Cones↩︎

10 Implementing the Maximal Closure Operator↩︎

11 More on Experimental Evaluation↩︎

11.1 MNIST↩︎

11.2 Fashion MNIST↩︎

References↩︎

Subjects

Updated on Academus

Interval Certifications for Multilayered Perceptrons via Lattice Traversal

Abstract

1 Introduction↩︎

2 Preliminaries↩︎

2.0.0.1 Normed Vector Spaces.

2.0.0.2 Multilayered Perceptrons.

2.0.0.3 Formal MLP Verification.

3 Intervals in Higher Dimensions↩︎

3.1 Operations on Intervals & the Interval Lattice↩︎

3.2 Interval Objectives↩︎

4 Sound & Complete Interval Certifications↩︎

4.1 Verification Oracles↩︎

4.2 The Generic Traversal Algorithm↩︎

4.3 Minimally Complete Certifications via the \(\top\)–Operator↩︎

4.4 Edge Length Non-Triviality in Sound Certifications via the \(\bot\)-Operator↩︎

4.5 The Maximal Closure Operator \([I]\)↩︎

4.6 The Space of Interval Certifications↩︎

5 Optimization over Interval Certifications↩︎

5.1 On the Intractability of Sound Maximization↩︎

5.2 Sound Maximization on Uniform Intervals↩︎

5.3 The Space of Uniform Interval Certifications↩︎

6 Implementation↩︎

6.1 Experimental Evaluation↩︎

7 Conclusions & Future Work↩︎

8 Omitted proofs↩︎

8.1 Proofs of Section 3↩︎

8.2 Proofs of Section 4↩︎

8.3 Proofs of Section 5↩︎

9 Geometry of the \(\mathbb{R}^d\) Cone Partition↩︎

9.1 Elements of Affine Geometry↩︎

9.2 Intersections of Cones↩︎

10 Implementing the Maximal Closure Operator↩︎

11 More on Experimental Evaluation↩︎

11.1 MNIST↩︎

11.2 Fashion MNIST↩︎

References↩︎

Subjects

Updated on Academus

8.1 Proofs of Section 3 ↩︎

8.2 Proofs of Section 4 ↩︎

8.3 Proofs of Section 5 ↩︎