arXiv CSopen access

Are Safety Guarantees in Neural Networks Safe? How to Compute Trustworthy Robustness Certifications

Are Safety Guarantees in Neural Networks Safe? How to Compute Trustworthy Robustness Certifications Merkouris Papamichail1,2 , Konstantinos Varsos1,2 , Giorgos Flouris1 , and João Marques-Silva3,4 Foundation for Reasearch and Technology - Hellas, Heraklion, Greece {mercoyris,varsosk,fgeo}@ics.forth.gr 2 University of Crete, Heraklion, Greece 3 Catalan Institution for Research and Advanced Studies, Barcelona, Spain [email protected] 4 University of Lleida, Lleida, Spain

arXiv:2606.23858v1 [cs.LG] 22 Jun 2026

1

Abstract. A primary challenge in AI safety is the existence of adversarial examples —slightly distorted inputs that cause a neural network (NN) to misclassify. To mitigate this problem, recent research focuses on the computation of robustness certifications, which, for a given input, determine the largest distortion the input may receive without breaking the network’s prediction. Robustness certifications can be interpreted as an axis-aligned hyper-rectangle (multi-dimensional intervals). Most existing approaches focus on maximizing the certification’s volume, but recent intractability results prohibit the computation of volume-optimal certifications in reasonable time. We introduce the apothem measure — the minimum slack between the input and one of the interval’s faces, and show how to compute apothem-optimal certifications in a linear number of calls to a NN verifier (oracle) w.r.t. the input domain’s diameter. Moreover, we prove that we cannot have a volume-optimal, oracle-based algorithm, even if we discard the oracle costs. Also, we introduce dual certifications —an interval including all instances of a class— thus providing apothem-minimum upper bounds to a robustness certification. Further, we present the ParallelepipedoNN1 system, which we evaluate on the standard MNIST and Fashion MNIST benchmarks. A preliminary comparison with existing work on the same datasets reveals at least two-fold improvement w.r.t. the minimum edge length. Keywords: AI Safety · Adversarial Robustness · Interval Algebra.

1

Introduction

Neural Networks (NNs) have been successfully applied to a variety of machine learning tasks, achieving both high performance and empirical accuracy. However, it has been observed that slight distortions of the input can break the network’s prediction. Such distorted inputs are called adversarial examples [28,7] 1

https://github.com/merkouris148/parallelepipedonn

2

M. Papamichail et al.

and motivated research on robustness certification. In robustness certification we are presented with an input and must compute the largest distortion the input may receive without causing a misclassification. By calculating tolerance intervals for each dimension and taking their Cartesian product, we are left with an axis-aligned hyper-cube, or multi-dimensional interval. This geometrical interpretation allows us to express robustness certification as an optimization problem such that finding the best certification corresponds to optimizing w.r.t. a given measure. The most widely used approach in the area is to express robustness certification as a constrained convex optimization problem, and then solving it numerically using first order differential methods [30,20,18,12]. This approach also leverages powerful NN frameworks (e.g., PyTorch, TensorFlow) for efficiently computing the necessary gradients. Despite its efficiency, this approach comes at a cost: in order to be applied to real world NNs, the network needs to be linearly relaxed. As the ReLU activation function is non-differentiable, traditional NNs can only be described using boolean variables that lead to non-linear constraints, and thus linear relaxation is in effect an approximation. In particular, linearly relaxing a NN results in false positives, flagging safe inputs as adversarial examples. This leads to artificially smaller robustness certifications, underestimating the network’s local stability. This uncertainty hinders the applicability of robustness certifications in practice. For example, consider the common robustness certifications’ quality measure, the volume [30,19,18]. Suppose that in order to consider the network robust, we need to achieve a volume threshold of v1 . However, we calculated a certification of volume v2 , with v2 < v1 . Does the network meet the desired safety guarantees? Should we retrain it, or is its robustness underestimated? Since volume optimality cannot be guaranteed, these questions cannot be answered. This work aims to mitigate this exact problem. Firstly, we introduce the apothem measure, which measures the minimum “slack” between the input and one of the faces of the hyper-rectangle. Next, we show how to compute apothemoptimal robustness certifications by iteratively querying a NN verifier (oracle). For arbitrary certifications, this can be done in a linear number of oracle calls w.r.t. the input domain’s diameter. If we constrain ourselves to uniform certifications (allowing only uniform distortion), we achieve apothem optimality in logarithmic oracle calls w.r.t. the input domain’s diameter. Further, we introduce the notion of dual certifications, which covers all the inputs of a specific class. Hence, a dual certification includes all possible robustness certifications of a class, constituting an upper bound to any increasing quality measure. Finally, we show that optimality cannot be achieved in polynomial time for the volume metric by an oracle-based algorithm, even if we discard the oracle costs. Returning to our original example, our apothem-optimal algorithms can be used to compute a robustness certification. If the threshold is ϖ1 , but we computed ϖ2 , with ϖ2 < ϖ1 , we know that the network is to blame and should be retrained. Moreover, if we need to use another quality measure, like volume, we can compute the dual certification. If the dual’s volume is v2 and we need to have v1 , with v1 > v2 , we know that no such certification exists, for this NN.

Trustworthy Robustness Certifications in NNs

3

We implemented our algorithms in the ParallelepipedoNN system, which we evaluate on the standard MNIST and Fashion MNIST datasets on multiple measures. Notably, a preliminary comparison with existing software reveals a two-fold improvement w.r.t. the certification’s minimum edge length, and at least an order of magnitude improvement w.r.t. the certification’s diameter.

2

Multi-Dimensional Intervals

We begin with some foundational results from Sunaga’s Interval Algebra [27]. Firstly, we generalize the ≤ ⊆ R × R relation to multi-dimensional spaces. For two vectors ℓ, u ∈ Rd we write ℓ ≤ u iff ℓi ≤ ui for all i ∈ [d], and ℓ < u iff ℓi < ui for all i ∈ [d]. Multi-dimensional intervals are defined as follows: Definition 1 (Multi-Dimensional Intervals). Let ℓ, u ∈ Rd , with ℓ ≤ u. An interval [ℓ, u] ⊂ Rd is the set of points x ∈ Rd such that ℓ ≤ x ≤ u. Finally, I(d) denotes the space of d–dimensional intervals, i.e., I(d) = {S ⊂ Rd | ∃ ℓ, u ∈ Rd , ℓ ≤ u, S = [ℓ, u]}. The multi-dimensional intervals of Def. 1 are used to formalize the concept of robustness certification. Let I1 , . . . , Id be the sequence of (one-dimensional) tolerance intervals of a robustness certification. Recall that we can perturb freely each feature i within Ii , without breaking the prediction. Concretely, this robustness certification can be represented by the multi-dimensional interval I = I1 ×· · ·×Id . Assume F ⊂ Rd be the input domain of a particular neural network. For a given input x ∈ F, we can express the robustness certifications of x as intervals of the form [x − a, x + b], where a, b ≥ 0. Intuitively, the vectors a, b correspond to the maximum subtractive and additive perturbations not breaking the network’s prediction. Inversely, for any interval I containing x, there are vectors a, b ≥ 0, s.t. I = [x − a, x + b]. For the domain F and an input x, I(d)|Fx denotes the space of all the intervals of F containing x. For any x ∈ Rd , we call the interval [x, x] = {x} trivial. For a radius ρ > 0, we call intervals of the form [x − ρ1, x + ρ1] uniform. Uniform intervals geometrically represent axis-aligned hyper-cubes. Moreover, for any vector v ≥ 0, we call intervals of the form [x − v, x + v] symmetric. Finally, arbitrary intervals are characterized by two vectors a, b ≥ 0, s.t. [x − a, x + b]. See Fig. 1 (left). 2.1

Operations on Intervals, and the Interval Lattice

Recall that we denote the space of intervals in F that contain an input x with I(d)|Fx . The space I(d)|Fx is highly structured by simple algebraic operations. Definition 2. Let [ℓ, u], [m, n] ∈ I(d)|Fx . We define the operations: ∆

1. [ℓ, u] + [m, n] = [ℓ + m, u + n] ∆ 2. [ℓ, u] ⊔ [m, n] = [min{ℓ, m}, max{u, n}] ∆ 3. [ℓ, u] ⊓ [m, n] = [max{ℓ, m}, min{u, n}]

4

M. Papamichail et al.

Fig. 1: Left: Interval Families: uniform, symmetric, and arbitrary. Right: Interval Measures: A diameter, π perimeter, v volume, α minimum edge, ϖ apothem.

It is easy to see that I(d)|Fx is closed under the operations in Def. 2. The summation of two intervals, corresponds to the well-known Minkowski sum. We sometimes abuse notation, writing x+[ℓ, u], instead of [x, x]+[ℓ, u] (analogously for the other operations). The ⊔, ⊓ operations were introduced by Sunaga [27], and reveal the underlying lattice structure. A partially ordered set is a lattice when for any two elements the least upper bound (lub) and greatest lower bound (glb) exist. In the I(d)|Fx latttice structure, the lub is given by the join operation ⊔, and the glb by the meet operation ⊓. Theorem 1 (Interval Lattice [27]). The interval space I(d)|Fx , under ⊆ constitutes a complete lattice with ⊔, ⊓ as the meet and join operations, respectively. 2.2

Interval Objectives

We proceed by discussing interval measures. A measure µ : I(d)|Fx → R≥0 is a function assigning a positive real value to an interval. The trivial interval has to have zero measure, and a measure must be monotone w.r.t. set-inclusion. We also introduce the novel apothem measure. Definition 3 (Interval Measures). Consider an interval I = x + [ℓ, u] ∈ I(d)|Fx , with ℓ ≤ u. Then we define the following measures: n o Apothem: ϖ(I) = min mini∈[d] (xi − ℓi ), minj∈[d] (uj − xj ) Minimum Edge: α(I) = min P i∈[d] ui − ℓi Perimeter: π(I) = i∈[d] ui − ℓi Q Volume: v(I) = i∈[d] ui − ℓi . Diameter: A(I) = maxi∈[d] ui − ℓi = ∥ui − ℓi ∥∞ All the measures of Def. 3 are depicted in Fig. 1 (right). In our experimental evaluation, we also use the average edge length E(I), defined as E(I) = π(I)/d. Apothem2 measures the minimum “slack” between the input x and one of the 2

In Euclidean geometry apothem is a line between the polygon’s center and a faces.

Trustworthy Robustness Certifications in NNs

5

faces of the corresponding hyper-rectangle. In the sequel, we see that a robustness certification’s faces will be bounded by adversarial examples. Hence, we can use the apothem to measure the minimum distance between the input x and the nearest adversarial example. Prop. 1 relates the above measures. We include omitted proofs in App. A. Proposition 1. For an interval I ∈ I(d)|Fx and the measures of Def. 3 we have, A(I) ≥

3

p 1 · π(I) ≥ d v(I) ≥ α(I) ≥ 2 · ϖ(I) d

(1)

Robustness Operators

Here we will work abstractly, in order to consider the combinatorial aspects of robustness certification and its relation to multi-dimensional intervals. In particular, consider the domain of a neural network F and a set of adversarial examples V ⊂ F. Moreover, let x ∈ F be the given input. A robustness certification will be an interval I ∈ I(d)|Fx , s.t. x ∈ I and I ∩ V = ∅. The technicalities on how we obtain the set of adversarial examples V will be discussed in Section 4. For now, let’s assume that this set is complete, meaning that if we manage to exclude its members, there is no other input in the domain F breaking the prediction. This lets us focus on a subtle, but important problem. From all the candidate intervals J ⊆ F \ V, which one should we choose? We proceed in two steps. Firstly, we consider the case of excluding a single adversarial example v ∈ V, defining the apothem-optimal, “small-step” 3 , constrain operator. Then, we generalize for multiple adversarial examples, where we define the “big-step”, bottom operator, also ensuring apothem-optimality. Finally, we discuss dual certifications, returned by the big-step, top operator. 3.1

Small-Step Robustness

Now we discuss our “small-step” robustness operator. For an input x, consider an interval I s.t. x ∈ I. Moreover, let v ∈ I be an adversarial example we want to exclude. Our small-step robustness operator will do just that, excluding the adversarial example v from the interval I, in an apothem-optimal manner. We call this operation constrain, and denote it by I/v. Subsequently, let I ′ = I/v. Recall that the intervals are essentially sets of 2d inequalities, each corresponding to a lower or upper bound for one of the d coordinates of the input space, written compactly as I = x+[ℓ, u], with ℓ ≤ 0 ≤ u. To ensure that v ∈ / I ′, it suffices to ensure that one of these inequalities fails. To achieve apothemoptimality, we choose the dimension k ∈ [d] for which |vk − xk | is maximum. If vk − xk > 0, then the upper bound must be reduced to exclude v, by changing the k-th dimension of u to produce a u′ that leaves v out of I ′ ; otherwise the lower bound must be increased accordingly. 3

“Small-step” operators deal with one example, while “big-step” with sets.

6

M. Papamichail et al.

Fig. 2: Left: The constrain operator. Right: How the domain space can be partitioned in cones. The cone Ci contains all the adversarial examples that result in modifying the i-th coordinate of the upper endpoint u. An important technicality here is that we use a precision constant δ > 0 to ensure a “meaningful” reduction of the interval. When modifying the upper bound, we set u′k = vk − xk − δ, and symmetrically for the lower bound. This serves two purposes. First, it excludes v in a “strict sense” (otherwise v would be in the border of I ′ ). Second, it avoids infinitesimal modifications. As we will see later, this is necessary to guarantee the termination of our algorithms. This process is visualized in Fig. 2 (left) and defined formally below. Definition 4 (Constrain Operator). Consider an input x ∈ F, an interval I = x + [ℓ, u], with ℓ ≤ 0 ≤ u, an adversarial example v ∈ I, and a precision constant δ > 0. Let k = argmaxi∈[d] {|vi −xi |}. We define the constrain operation I/δ v = x + [ℓ′ , u′ ], where: – If vk − xk > 0 then ℓ′ = ℓ, u′i = ui for all i ∈ [d] \ {k} and u′k = max{0, vk − xk − δ}. – If vk − xk < 0 then ℓ′i = ℓi for all i ∈ [d] \ {k}, ℓ′k = min{0, vk − xk + δ}, and u′ = u. Note that vk − xk ̸= 0 because, by construction, x ̸= v. The reason for max and min in the definition is to ensure that x ∈ I ′ , i.e., ℓ′ ≤ 0 ≤ u′ . Subsequently, we omit δ, writing I/v. The operator’s apothem-optimality is established below. Proposition 2. Consider an interval I ∈ I(d)|Fx and a point v ∈ I. For any interval J ∈ I(d)|Fx , with v ∈ / J and J ⊆ I, we have ϖ(J) ≤ ϖ(I/v). Proof. W.l.o.g. let x = 0. For any J ∈ I(d)|Fx and v ∈ F, it holds v ∈ / J, iff maxi∈[d] |vi | > ϖ(J). Also, ϖ(I/v) = min{ϖ(I), maxi∈[d] |vi |}. ■ 3.2

Big-Step Robustness

Now we revert to the original problem of handling a set of adversarial examples. Observe that the small-step constrain operator implicitly defines a partition of F into 2d regions4 , denoted by Ci , Ci , for i ∈ [d], see Fig. 2 (right). 4

Corresponding to polyhedral cones, C = {x ∈ Rn | Ax ≤ 0}, A ∈ Rm×n .

Trustworthy Robustness Certifications in NNs

7

Fig. 3: Left: The bottom interval V⊥x. Right: The dual top interval Q⊤x.

Definition 5 (Cone Partition). Consider the domain F ⊂ Rd , and an input x ∈ F. The cone partition w.r.t. x is defined by the sequence {Ci , Ci }i∈[d] , where  Ci = v ∈ F  Ci = v ∈ F

vi ≤ xi , ∀j ∈ [d] |vi − xi | ≥ |vj − xj | , vi ≥ xi , ∀j ∈ [d] |vi − xi | ≥ |vj − xj | .

(2)

For a given set of adversarial examples V, let V⊥x denote the bottom interval, where (V⊥x)∩V = ∅, see Figure 3 (Left). Since x ∈ (V⊥x), we write the bottom interval as V⊥x = x + [−r, r], with r, r ≥ 0. The k-th coordinate of the upper endpoint r is set to the minimum coordinate-wise absolute distance |xk − vk |. We work similarly for the k-th coordinate of the lower endpoint r. Definition 6 (⊥-Operator). Consider a domain F and an input x ∈ F. Let V ⊂ F be a set of adversarial examples. Moreover, assume the values ri , ri > 0, where ri = inf{xi − vi | v ∈ Ci ∩ V} and ri = inf{vi − xi | v ∈ Ci ∩ V}. Then, V⊥x denotes the bottom interval, where V⊥x = x + [−r, r]. Observe that, by definition, the bottom interval can be unbounded. Indeed, if one of the cones is empty, e.g., Ci = ∅, then the corresponding coordinate-wise absolute distance approaches infinity, i.e., ri → +∞. This happens trivially, when inputs lay at the border of the domain F, thus Ci ∩ F = ∅. Hence, no adversarial examples exist. Note that unbounded intervals can still have bounded apothem, unless equal to Rd . We discuss this issue again in Sec. 5. Subsequently, we show that the bottom operator is apothem optimal. Theorem 2 (⊥-Operator Optimality). Consider a domain F and an input x ∈ F. Let V ⊂ F be a set of adversarial examples. The following hold: 1. (V⊥x) ∩ V = ∅. 2. For every J ∈ I(d)|Fx , s.t. x ∈ J and J ∩ V = ∅, we have ϖ(J) ≤ ϖ(V⊥x). Proof. The first desideratum is trivial from Def. 6. We prove the second. W.l.o.g. let the apothem be achieved by the coordinate rk . From the Def. 6 there is a adversarial example v ∈ V, s.t. rk = vk . Assume the interval J = x + [ℓ, u],

8

M. Papamichail et al.

ℓ ≤ 0 ≤ u, with J ∩ V = ∅. For sake of contradiction, ϖ(J) > ϖ(V⊥x). It holds, uk ≥ ϖ(J) > rk . Thus, uk > vk . Since J ∩ V = ∅, there is a coordinate j, s.t. uj ≤ vj . However, ϖ(J) ≤ uj ≤ vj ≤ vk ≤ rk = ϖ(V⊥x) < ϖ(J), where we have vj ≤ vk , since v ∈ C k . A contradiction. ■ As we discussed before, we can translate the bottom operator to consecutive constrain operations. Below we establish that the resulting interval will always include the bottom interval, regardless of the order with which we perform the constrains. This enables us to apply the bottom operator in practice. Further, since in real-world cases adversarial examples will arrive in an on-line manner, we can exclude them upon arrival using the constrain operator. Proposition 3. Consider a domain F, and an input x ∈ F. Let V ⊂ F be a set of adversarial examples. We assume an ordering in V, i.e., V = v1 , v2 , . . . , vn . Let I = F /v1 /v2 · · · /vn 5 . Then, x ∈ I, I ∩ V = ∅, and I ⊇ V⊥x. 3.3

Dual Certifications

Here we discuss the dual problem, which enables us to efficiently compute upper bounds to the robustness certification. We consider the inverse situation: for the domain F and input x, we take a set of positive inputs Q ⊂ F, and compute an interval I ∈ I(d)|Fx , s.t. x ∈ I and I ∪ Q = I. The interval I is obtained by the top operator Q⊤x, see Fig. 3 (Right). We work symmetrically to the bottom operator. In particular, the dual certification can be written in the form Q⊤x = x + [−R, R], with R, R ≥ 0. Now the i-th coordinate Ri is set to the maximum coordinate-wise absolute distance between x and the positive points of Q. For R we work similarly. Definition 7 (⊤-Operator). Consider a domain F and an input x ∈ F. Let Q ⊂ F be a set of positive points. Moreover, assume the values Ri , Ri > 0, where Ri = sup{xi − qi | q ∈ Q} and Ri = sup{qi − xi | q ∈ ∩Q}. Then, Q⊤x denotes the top interval, where Q⊤x = x + [−R, R]. Note that since Q ⊂ F, the top interval is always bounded. We prove the optimality of the top operator in Thm. 3. However, we follow a different approach than the Thm. 2. First, we prove the correctness of the top operator. Then, we show that the bottom operator returns a minimal interval that includes all the points in Q. Finally, we show that any minimal interval including Q is unique. This results in apothem optimality. Theorem 3. (⊤-Operator Optimality) Consider a domain F and an input x ∈ F. Let Q ⊂ F be a set of positive points. The following hold: 1. (Q⊤x) ∪ Q = (Q⊤x). 2. There is no interval J ∈ I(d)|Fx , s.t. x ∈ J, J ∪ Q = J, and J ⊂ (Q⊤x). 5

We assume left associativity of the / operator.

Trustworthy Robustness Certifications in NNs

9

3. Let I, J ∈ I(d)|Fx two intervals, s.t. (Q ∪ {x}) ⊆ I, J. Moreover, let I, J be minimal, w.r.t. set inclusion, achieving this property. Then, I = J. 4. For every J ∈ I(d)|Fx , s.t. x ∈ J, and J ∪ Q = J, then ϖ(J) ≥ ϖ(Q⊤x). Proof (Sketch). 1. Immediate consequence of Def. 7. 2. We prove that if J ⊂ (Q⊤x), then there is some q ∈ Q, s.t. q ∈ / J. 3. Let I, J be minimal intervals. Then we prove that the intersection I ∩ J also includes Q ∪ {x}. Thus, reaching a contradiction. 4. Follows from the previous results. ■ Again, the top interval can be translated in a sequence of small-step interval operations. In particular, we use the join operator ⊔ of Def. 2 to include the points in Q. We abuse the notation writing I ⊔ q, instead of I ⊔ [q, q]. Proposition 4. Consider a domain F and an input x ∈ F. Let Q ⊂ F be a set of positive points. We assume an ordering in Q, i.e., Q = q1 , q2 , . . . , qn . Let I = [x, x] ⊔ q1 ⊔ q2 · · · ⊔ qn 6 . Then, I = Q⊤x. We close our discussion on the dual certification by establishing the (weak) duality of the bottom and top operators in the following theorem. Theorem 4. (Weak ⊥, ⊤-Duality) Consider an input domain F, and a partition into positive points Q and adversarial examples V, i.e., Q ∩ V = ∅ and Q ∪ V = F. Then, for an input x ∈ F, we have (V⊥x) ∩ F ⊆ Q⊤x and for every increasing measure µ : I(d)|Fx → R≥0 of Def. 2, we have µ[(V⊥x) ∩ F] ≤ µ[Q⊤x]. Note that since the bottom interval may be unbounded, we take the intersection (V⊥x) ∩ F. In the sequel, we discuss how the above observations can be applied to adversarial robustness of NN classifiers. There, all the points of a particular class c are positive. The rest of the points are adversarial examples.

4

Algorithms

In this section we discuss how the notions of Sec. 3 can be applied to compute the adversarial robustness of neural network classifiers. This is achieved by encoding the bottom and top operators as small-step interval operations, applying Prop. 3 and 4. However, for NNs we cannot have explicit descriptions of the adversarial examples V or positive points Q. Instead, we only have the description of the NN, its weights, biases and activation functions. Using this, we construct first order formulas Q, S that are satisfied only for points in V, Q, respectively. ReLU NNs can be expressed as a set of inequalities with real and boolean variables. This formalism is called in the literature mixed integer linear programming (MILP) [21,5]. Using existing MILP solvers (e.g. GLPK7 ), MILPs can be solved efficiently and accurately. Moreover, specific tools have been developed and optimized for NN MILPs. One such tool is the Marabou [15,31] software for NN verification, which we also use in our ParallelepipedoNN software. 6 7

We assume left associativity of the ⊔ operator. https://www.gnu.org/software/glpk/

10

M. Papamichail et al.

Therefore, despite not having an explicit description of the V, Q sets, we can construct oracles (first-order formulas, solvable with a MILP solver) V , Q, which either assert that an interval I is included in a set P ∈ {V, Q}, or return a counterexample p ∈ I \ P. Then, we use the counterexample p to refine the current interval using an operator □ ∈ {/, ⊔}. 4.1

From Abstract Sets to Neural Networks

Assume the input dimension din and the output dimension dout . Let F ⊂ Rdin denote the input (feature) space and S ⊂ Rdout denote the output (score) space. A NN is a function of the form σ : F → S. In this work we are interested in ReLU activated NNs. For the one-dimensional case, the ReLU function r : R → R≥0 is defined as r(x) = max(x, 0). For the d-dimensional case we have r : Rd → Rd≥0 , where r(x) = (r(x1 ), . . . , r(xd )). We follow the definition in [4]. Definition 8 (Neural Network Classifiers). A neural network σ : F → S, with F ⊂ Rdin , S ⊂ Rdout is described as the tuple σ = ⟨L, D, W, B⟩, where: – L ∈ N denotes the number of layers. – D denotes the architecture, i.e. a sequence din = d0 , d1 , . . . , dL−1 , dL = dout . – W denotes the sequence of weight matrices, s.t. W (i) ∈ Rdi ×di−1 , for i ∈ [L] – B denotes a sequence of biases s.t. b(i) ∈ Rdi for i ∈ [L]. The value of σ(x) is given as the value σ (L) in the system of equations below.  σ (0) = x (3) σ (i) = r[W (i) σ (i−1) + b(i) ], ∀i ∈ [L] For classification problems, we also assume a set of classes C, s.t. |C| = dout . A classifier is a function of the form κ : F → C, where κ(x) = arg maxi∈dout σ(x). As discussed we can formulate a NN as a MILP to formally describe the input/output relation of the neural network as a logic formula. Let ν be that formula. For every input x ∈ F and every output y ∈ S the pair satisfies ν if and only if the network σ(·) with input x outputs y. Now assume a fixed input x ∈ F and an interval I = [ℓ, u] ∈ I(din )|Fx , s.t. x ∈ I. We have the following.     ^ _ VI,ν (p) ≡  ℓi < pi ∧ pi < ui  ∧ ν(p, y) ∧  yj − yc > ϵ (4) j̸=c

i∈[din ]

 QI,ν (p) ≡ 

 _ i∈[din ]



pi < ℓi ∨ ui < pi  ∧ ν(p, y) ∧ 

 ^

yc − yj > ϵ

(5)

j̸=c

Above, ϵ > 0 is a precision constant. The predicate VI,ν is satisfied only by adversarial examples, i.e., for inputs that belong to the current interval I and maximize a different score than the target class c. Symmetrically, the predicate QI,ν is satisfied by a c-instance not included in the current interval I. When there is no solution in I for VI,ν , we reached a robust certification. Symmetrically, when there is no solution outside of I for QI,ν , we reached a dual certification.

Trustworthy Robustness Certifications in NNs

11

Algorithm 1: RefineCheck(Io , PI,ν , □) Input: We assume the following arguments: • Io ∈ I(d)|Fx , an initial interval. • PI,ν , a property to be falsified. • □ : I(d)|Fx × F → I(d)|Fx , a refinement operator. Output: I, an interval s.t. |= ¬PI,ν 1 I ← Io 2 while ∃p, s.t. p |= PI,ν do 3 I←I □p return I

4

4.2

Refine & Check Algorithm

We now have all the components to develop our refine & check algorithm, whose pseudocode is given in Alg. 1. Starting from an initial interval Io , the algorithm repeatedly checks whether the current interval I falsifies some given property PI,ν . The check is delegated to a NN verifier (line 2), which receives as input the MILP encoding of the network, the interval I, and the property PI,ν . If the property is not falsified, the verifier returns a counterexample p that satisfies the property. The interval is then refined using p via some given operator □, producing the interval I □ p (line 3). The procedure continues until the verifier asserts that PI,ν is falsified, in which case the current interval is returned. Different instantiations of Alg. 1 can be obtained by appropriately choosing its parameters. Eq. (6) shows how to compute the apothem-optimal robustness certification. In this setting, the initial interval is the whole domain F, the property to be falsified is given by eq. (4), and the refinement operator is the constrain operator of Def. 4. The correctness of eq. (6) is given by Prop. 3, which shows that the bottom operator can be realized as a sequence of constrain operations. We call Alg. 1 instantiated in this manner as Top-Down Search (TDS). Finally, since we begin from the domain F, TDS computes the intersection (V ⊥x) ∩ F. (V ⊥x) ∩ F = RefineCheck(F, VI,ν , /)

Top-Down Search (TDS)

(6)

Q⊤x = RefineCheck([x, x], QI,ν , ⊔)

Bottom-Up Search (BUS)

(7)

Eq. (7) presents the implementation for dual certifications. The construction proceeds symmetrically. The interval is initialized to the trivial [x, x], the property to be falsified is given by eq. (5), and the refinement operator is the join operator ⊔ of Def. 2. The correctness of eq. (7) follows from Prop. 4, which shows that the top operator can be expressed as a sequence of join operations. We refer to the parametrization in eq. (7) as Bottom-Up Search (BUS). Observe that the abstract sets V and Q introduced in Sec. 3 have now been translated into the verification properties V and Q. This was possible only because we managed to translate the “global”, big-step, bottom and top operations, to “local”, small-step, operations. Based on the small-step operators, we are able

12

M. Papamichail et al.

to construct the on-line refine & check method of Alg. 1. In this setting the set P, that is P ∈ {V, Q}, is constructed incrementally, and contains all the counterexamples p returned by the NN verifier during the execution of Alg. 1. 4.3

The Complexity of Apothem Optimality

Our refine & check algorithm allows us to calculate the computational complexity of both operators in a single proof. To that end, let P be the set of all counterexamples returned by the NN verifier, and n = |P|. Moreover, let tPI,ν be the time consumed by the NN verifier (in the worst case) to test the satisfiability of the property PI,ν . Finally, let t□ be the execution time of the refinement operation □. Then, in each iteration, Alg. 1 processes one counterexample, makes a query to the NN verifier, and applies a refinement operator. Theorem 5. Let n be the number of counterexamples returned by the NN verifier. Let tPI,ν be the worst-case time to check whether property PI,ν holds. Finally, let t□ be the worst-case time required by the operator □. Then, the refine & check method of Alg. 1 terminates after O[n · (t□ + tPI,ν )] steps. If □ ∈ {/, ⊔}, then t□ = O(d), and Alg. 1 concludes in O[nd + ntPI,ν ] time. Although the number n of counterexamples is unknown, we can bound it from above using the precision constant δ. The constrain operator only modifies one inequality of the given interval at each refinement step, and each inequality can be modified at most A(F)/δ times, where A(F) is the domain’s diameter. Since each interval is defined by 2d inequalities, the total number of counterexamples is bounded by 2d · A(F)/δ. The join operator ⊔ is more intervening, modifying all 2d inequalities at once, resulting in A(F)/δ counterexamples. Corollary 1. Let tPI,ν be the worst case time for verifying property PI,ν . TDS terminates after O[(A(F)/δ)(d2 + d · tPI,ν )] time. BUS terminates after O[(A(F)/δ)(d + tPI,ν )] time. 4.4

The Intractability of Volume Optimality

From Thm. 5 we can compute an apothem optimal robustness certification in poly(n, d, tPI,ν ) time. Namely, even if NN verification can be computed in constant time, i.e., tPI,ν = O(1), our algorithm becomes polynomial. This does not hold for other measures, like the volume, where we cannot have polynomial time volume-optimality, even if NN verification costs are ignored. To see that, recall the abstract robustness certification problem, introduced in Sec. 3. There, we had a set V ⊂ F of adversarial examples and an input point x ∈ F. Our goal was to compute an interval I ∈ I(d)|Fx , s.t. x ∈ I and V ∩ I = ∅. For a constant γ > 0, we want to decide if there is I ∈ I(d)|Fx with the above properties and v(I) ≥ γ. This problem is closely related to Maximum Empty Rectangle (MER) [24,3,1,2] and query-Maximum Empty Square (q-MES) [8] problems. Next, we establish an intractability result based on the proof of MER’s intractability by Backer and Keil in [1].

Trustworthy Robustness Certifications in NNs

13

Theorem 6. Consider a set of adversarial examples V ⊂ F, an input x ∈ F, and a constant γ > 0. Moreover, let n = |V|, let d be the dimension s.t. F ⊂ Rd , and let tPI,ν be the worst-case time check whether property PI,ν holds. Then, the existence of a robustness certification I ∈ I(d)|Fx , with x ∈ I, I ∩ V = ∅ and v(I) ≥ γ cannot be decided in poly(n, d, tPI,ν ) time, unless P = NP. Proof (Sketch). We use the argument of [1] reducing from the independent set problem to maximum volume adversarial robustness. In [1] each vertex of a given graph maps to a dimension, each edge maps to a point. The graph has an independent set of size k iff there is a sufficiently large empty interval. Thus, given a graph G, we use the methodology in [1] to construct a set of adversarial examples V. However, we also need to define an input x that must be included to the interval. We set x = 0. From Lemma 2 in [1] the origin will always be included in a maximum volume interval. Thus, our choice of x does not effect the validity of the argument. This concludes the reduction. ■ 4.5

Notes on Uniform Certifications

We close this section with some notes on uniform robustness certifications (originally used in [30]), i.e., certifications of the form I = [x − ρ1, x + ρ1] for ρ > 0 and some input x ∈ F. In our setting, we can use binary search to determine the maximum radius excluding the adversarial examples in V, or the minimum radius including the positive examples Q. The top and bottom operators of Sec. 3, when restricted to uniform certifications, are denoted by ⊤B and ⊥B respectively, while the corresponding algorithms B-BUS and B-TDS. These operators can be computed in logarithmic log(A(F)/δ) oracle calls. We use uniform certifications as a baseline in our following experimentation.

5

Implementation

In this section, we review the ParallelepipedoNN system, where we implement the algorithms and operations discussed earlier. In particular, we present two case studies based on the MNIST [17] and the Fashion MNIST [33] datasets. Specifically, we train two ReLU NNs and compute robustness and dual certifications for each dataset-network pair. For robustness certifications, we use the TDS algorithm of eq. (6) and its uniform variant B-TDS (see Subsec. 4.5). For dual certifications, we use the BUS algorithm of eq. (7) and its uniform variant B-BUS. We comment on the CPU time, oracle queries and edge lengths. Experimental Setup. We ran our experiments in parallel on an Ubuntu 18.04 machine, with Intel Xeon E5-2640 v4 CPU at 2.394GHz with 38 cores, with 128GB RAM. We utilized 35 cores. ParallelepipedoNN is written in Python v3.8.16. We used the Marabou v2.0 [15,31] NN verifier. Our implementation takes as input a NN in open neural network exchange (ONNX) v1.16.08 format. For linear 8

See https://github.com/onnx/onnx.

14

M. Papamichail et al.

Fig. 4: Apothems in TDS (blue), BUS (red), and their difference (green), w.r.t. iterations, on a “7” MNIST image. After 860, we extend BUS with dashed line.

algebra computations, we used the NumPy v1.23.5 library. For visualization, we used the Matplotlib v3.7.2 library. The NNs used were trained from scratch, using TensorFlow v2.12.0. We evaluated all the algorithms using the same parameters. We set the precision constant δ to δ = 0.1, and a timeout to 1 hour. We use 2 datasets, namely MNIST [17] and Fashion MNIST [33]. Both datasets consist of 28×28 grayscale images, belonging to 10 classes. The NN architecture is D = ⟨784, 32, 10, 10⟩, w.r.t. Def. 8. The last layer is fully connected, without activation function. This corresponds to 25,450 trainable parameters. For training, we used the Adam [16] algorithm, Glorot [6] weight initialization, and the Categorical Crossentropy loss. The achieved test-set accuracy is 94% and 82% for the MNIST and Fashion MNIST, respectively. For each NN, we randomly chose 5 images of the 10 classes of the test set (a total of 50 images per NN). Measures in Practice. Note that one totally black or totally white pixel suffices to place a grayscale image to the border of the input space, making V ⊥x, and most measures, trivially unbounded. Therefore, for all measures, except the apothem, we use the intersection (V ⊥x) ∩ F. The apothem is computed in the (possibly unbounded) bottom interval V ⊥x. This is achieved by excluding the interval’s faces that stayed still during TDS’ execution. Hence, only adversarially bounded faces are considered, and the apothem returns the distance between the input and the nearest adversarial example. Running One Instance. In Fig. 4 we plot the apothem of the TDS and BUS algorithms as a function of the iterations, on a “7” MNIST image. TDS computes an apothem-maximum robustness certification, beginning from the whole domain, and gradually shrinking. In plateaus, the non-minimum edges are shrinking, thus the apothem stays constant. BUS computes an apothem-minimum dual certification. Note that BUS terminates in much fewer iterations than TDS, because it updates all edges in each iteration. Finally, we depict the difference in apothems between the i-th robustness and dual certifications. In this case, the two apothems happen to converge at 0.1 distance. Experimental Results. In Tbl. 1 we present results on the CPU time, the percentage of time spent in oracle calls, the number of oracle calls, the apothem

Time sec./min.

Verif. Perc.

# Verif. Calls

Apoth. ϖ

Min. Edge α

Avg. Edge E

Diam. A

Perim. π

MNIST

15

TDS 56.93m B–TDS 20.16s BUS 16.13m B–BUS 1.9s

99% 98% 96% 95%

691.3 9.98 895.73 4.0

0.14 0.04 1.0 0.81

0.15 0.04 0.86 0.81

0.53 0.05 1.0 0.83

1.0 0.08 1.0 1.0

415.55 35.76 781.4 650.92

Fashion MNIST

Trustworthy Robustness Certifications in NNs

TDS 9.19m B–TDS 5.66s BUS 13.55m B–BUS 2.7s

95% 94% 96% 96%

700.88 9.62 757.36 4.0

0.01 0.1 1.0 0.81

0.07 0.1 0.9 0.81

0.66 0.14 1.0 0.89

1.0 0.19 1.0 1.0

516.85 108.05 783.75 697.81

Data

Alg.

Table 1: Experiments on MNIST and Fashion MNIST datasets. Averages over 50 samples from each datasets. Values are rounded up to two decimal places.

ϖ, the minimum edge length α, the average edge length E = π(I)/d, the diameter A, and the perimeter π. In Tbl. 1, for each problem we denote with bold the best value. For robustness certifications we observe a tradeoff between quality and performance. The uniform algorithm B-TDS performs much faster than its arbitrary counterpart. This is expected by the discussion in Subsection 4.5. However, TDS achieves 3 times better quality, on average, as reported by α (in MNIST), the average edge length (in Fashion MNIST), etc. For the dual certification problem, we observe a different tendency. In both efficiency and quality the uniform variants perform better. We conjecture that this is due to numerical errors. The number of iterations and verification calls does not only affect the CPU time, but also introduces numerical errors. Observe that the majority of our computational time is consumed by oracle calls. Thus, our method inherits the oracle’s shortcomings in performance and precision. Finally, in general, the robustness and dual certifications are not close. This is because the difference between the robustness and dual certifications show how close is a class’ decision surface to an axis-aligned hyper-rectangle. Due to the complexity of NN decision surfaces, we expect this to happen rarely. Comparison with Existing Software. A direct comparison with existing software is currently impossible. Software incompatibilities (e.g., between PyTorch, TensorFlow, and ONNX, or Marabou and ERAN, etc.) raise implementation obstacles. Moreover, most existing algorithms do not output their certifications, but only a final average. Thus, a direct experimental comparison falls outside this paper’s scope. Nevertheless, a preliminary comparison reveals a two-fold improvement w.r.t. the certification’s minimum edge length, and an order of magnitude improvement w.r.t. the certification’s diameter. We now make a preliminary comparison, as points of reference. Liu et al. [20] train 3 networks for MNIST, with 3 hidden layers and architectures ⟨3 × 100⟩ = ⟨100, 100, 100⟩, ⟨3 × 300⟩ and ⟨3 × 500⟩. In each case, they report minimum edge length of α ≃ 0.06, for uniform certifications, and α ≃ 0.07, for symmetric certi-

16

M. Papamichail et al.

fications. For Fashion MNIST, they use a network with architecture ⟨3 × 1024⟩. They report α ≃ 0.026, for uniform and α ≃ 0.028, for symmetric certifications. The implementation, and the NN architectures of Li et al. [18] are not publicly available. They train 3 NNs for MNIST (MNIST100, MNIST300, MNIST500), and one NN for Fashion MNIST (FMNIST100). They report α of 0.058, 0.041, 0.045, and 0.072, for MNIST100, MNIST300, MNIST500, and FMNIST100, respectively. Finally, Kabahala and Drachsler-Cohen [12] report average edge length E of 0.196 and 0.1 for two MNIST NNs (⟨3 × 50⟩, ⟨3 × 100⟩), whereas for two Fashion MNIST NNs (⟨3 × 50⟩, ⟨3 × 250⟩) they report E of 0.191 and 0.037.

6

Related Work

Interval arithmetic [27,23] has been used in NN adversarial analysis (e.g. [30,14,34]). However, they do not make explicit use of the underlying lattice structure [27]. Adversarial robustness is the problem of deciding whether an area is free of adversarial examples. Several approaches exist [22], such as abstraction (e.g. [26]), satisfiability modulo theories (SMT) (e.g. [13,14]), and MILP (e.g. [15,31]). In this work we focus on robustness certification which is the optimization variant of the above. Most approaches rely on differentiable optimization, where the NN is firstly linearly relaxed (by taking the convex approximation of the ReLU activation) and then solved either by computing a feasible solution to the dual convex program [30], or by the augmented Langrage method [20,18]. These methods are scalable and can be applied to large NNs, but suffer from approximation errors [25] and lack optimality guarantees. More recent work [12] follows a hybrid approach, achieving maximality by querying a NN verifier to check for adversarial examples before deciding on the edge to refine using differentiable methods. Optimization happens w.r.t. the average edge length E, but optimality is not proved. Similar oracle-based iterative schemes have been applied in formal AI-explainability [9,32,10,11], where an explanation can be interpreted as a special form of interval [11]. Existing work on robustness certification mostly focuses on optimizing the volume [30,20,18], through optimizing minimum edge length. Deciding on the adversarial robustness of a uniform area is NP-hard [13], and even approximating the optimal α is intractable for uniform certifications [29]. However, volume optimality stays intractable even if the oracle costs are discarded.

7

Conclusions

We proposed a method to compute trustworthy robustness certifications by ensuring optimality w.r.t. the apothem. Moreover, we introduced the notion of dual certifications, which gives an upper bound to the certification’s quality. We also developed the ParallelepipedoNN system, which was evaluated over the MNIST and Fashion MNIST datasets. Our evaluation shows promising results w.r.t. existing implementations. Nevertheless, a direct experimental comparison is needed. We leave the latter as future work.

Trustworthy Robustness Certifications in NNs

17

References 1. Backer, J., Keil, J.M.: The Mono- and Bichromatic Empty Rectangle and Square Problems in All Dimensions. In: Latin American Theoretical Informatics Symposium (2010) 2. Chan, T.M.: Faster Algorithms for Largest Empty Rectangles and Boxes. Discrete & Computational Geometry (2023) 3. Chazelle, B., III, R.L.S.D., Lee, D.T.: Computing the Largest Empty Rectangle. SIAM Journal on Computing (1986) 4. Fefferman, C.: Reconstructing a neural net from its output. Revista Matemática Iberoamericana (1994) 5. Fischetti, M., Jo, J.: Deep neural networks and mixed integer linear optimization. Constraints - An International Journal (2018) 6. Glorot, X., Bengio, Y.: Understanding the Difficulty of Training Deep Feedforward Neural Networks. In: Conference on Artificial Intelligence and Statistics (2010) 7. Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and Harnessing Adversarial Examples. In: International Conference on Learning Representations (2015) 8. Gutiérrez, G., Paramá, J.R.: Finding the Largest Empty Rectangle Containing Only a Query Point in Large Multidimensional Databases. In: Scalable Scientific Data Management (2012) 9. Ignatiev, A., Narodytska, N., Marques-Silva, J.: Abduction-Based Explanations for Machine Learning Models. In: Association for the Advancement of Artificial Intelligence (2019) 10. Izza, Y., Huang, X., Morgado, A., Planes, J., Ignatiev, A., Marques-Silva, J.: Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation. Principles of Knowledge Representation and Reasoning (2024) 11. Izza, Y., Ignatiev, A., Stuckey, P.J., Marques-Silva, J.: Delivering Inflated Explanations. In: Association for the Advancement of Artificial Intelligence (2024) 12. Kabaha, A., Drachsler-Cohen, D.: Maximal Robust Neural Network Specifications via Oracle-Guided Numerical Optimization. In: International Conference on Verification, Model Checking, and Abstract Interpretation (2023) 13. Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Computer-Aided Verification (2017) 14. Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: a Calculus for Reasoning about Deep Neural Networks. Formal Methods System Design (2022) 15. Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljic, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.W.: The Marabou Framework for Verification and Analysis of Deep Neural Networks. In: Computer-Aided Verification (2019) 16. Kingma, D.P., Ba, J.: Adam: A Method for Stochastic Optimization. In: International Conference on Learning Representations (2015) 17. LeCun, Y., Cortes, C., Burges, C.J.: MNIST handwritten digit database. ATT Labs (2010) 18. Li, C., Ji, S., Weng, H., Li, B., Shi, J., Beyah, R., Guo, S., Wang, Z., Wang, T.: Towards Certifying the Asymmetric Robustness for Neural Networks: Quantification and Applications. IEEE Transactions on Dependable and Secure Computing (2022)

18

M. Papamichail et al.

19. Liu, C., Arnon, T., Lazarus, C., Barrett, C.W., Kochenderfer, M.J.: Algorithms for Verifying Deep Neural Networks. Foundations and Trends in Optimization (2019) 20. Liu, C., Tomioka, R., Cevher, V.: On Certifying Non-Uniform Bounds against Adversarial Attacks. In: International Conference on Machine Learning (2019) 21. Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward ReLU neural networks. Computer Research Repository (2017) 22. Meng, M.H., Bai, G., Teo, S.G., Hou, Z., Xiao, Y., Lin, Y., Dong, J.S.: Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective. Computing Research Repository (2022) 23. Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. SIAM (2009) 24. Naamad, A., Lee, D.T., Hsu, W.L.: On the maximum empty rectangle problem. Discrete Applied Mathematics (1984) 25. Salman, H., Yang, G., Zhang, H., Hsieh, C.J., Zhang, P.: A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks. In: Advances in Neural Information Processing Systems (2019) 26. Singh, G., Gehr, T., Püschel, M., Vechev, M.T.: An Abstract Domain for Certifying Neural Networks. Proceeding of the ACM on Programming Languages (2019) 27. Sunaga, T.: Theory of an Interval Algebra and its Application to Numerical Analysis. Research Association of Applied Geometry (1958) 28. Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J., Fergus, R.: Intriguing properties of neural networks. In: International Conference on Learning Representations (2014) 29. Weng, T.W., Zhang, H., Chen, H., Song, Z., Hsieh, C.J., Daniel, L., Boning, D.S., Dhillon, I.S.: Towards Fast Computation of Certified Robustness for ReLU Networks. In: International Conference on Machine Learning (2018) 30. Wong, E., Kolter, J.Z.: Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In: International Conference on Machine Learning (2018) 31. Wu, H., Isac, O., Zeljic, A., Tagomori, T., Daggitt, M.L., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.W.: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In: Computer-Aided Verification (2024) 32. Wu, M., Wu, H., Barrett, C.W.: VeriX: Towards Verified Explainability of Deep Neural Networks. In: Advances in Neural Information Processing Systems (2023) 33. Xiao, H., Rasul, K., Vollgraf, R.: Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms. Computer Research Repository (2017) 34. Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., Hsieh, C.J.: Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. In: International Conference on Learning Representations (2021)

A

Omitted proofs

A.1

Proofs of Section 2

Proposition 1. For an interval I ∈ I(d)|Fx and the measures of Def. 3 we have, A(I) ≥

p 1 · π(I) ≥ d v(I) ≥ α(I) ≥ 2 · ϖ(I) d

(1)

Trustworthy Robustness Certifications in NNs

19

Proof. Applying straightforward computations we take, A(I) = ∥ui − ℓi ∥∞ =

1 X max{ui − ℓi } d i∈[d] i∈[d]

≥

1 X d i∈[d] sY

≥ d



1 equals π(I) d



by arithmetic-geometric p mean inequality. Equals d v(I)

ui − ℓi ui − ℓi

i∈[d]

s ≥

d



d

 min{ui − ℓi }

[ equals α(I))]

i∈[d]

s =

d



d min(ui − xi + xi − ℓi )

i∈[d]

s ≥

d

 d min min(ui − xi ), min (xj − ℓj ) i∈[d]

j∈[d]



due to non-negativity. Equals ϖ(I)



■ A.2

Proofs of Section 3

In some of the proofs below, we assume w.l.o.g. that the input point is the origin, i.e., x = 0. If x ̸= 0, the same arguments apply after translating the space by −x, by working in F − x. Proposition 3. Consider a domain F, and an input x ∈ F. Let V ⊂ F be a set of adversarial examples. We assume an ordering in V, i.e., V = v1 , v2 , . . . , vn . Let I = F /v1 /v2 · · · /vn 9 . Then, x ∈ I, I ∩ V = ∅, and I ⊇ V⊥x. Proof. W.l.o.g. we assume x = 0. Let Ij be the sequence of intervals produced by Alg. 1, under property VI,ν (·) and operator /. It holds the following,  Ij+1 = Ij /vj+1 , if ∃ vj+1 ∈ Ij \ V . (8) Ij+1 = Ij , otherwise From eq. (8), Ij+1 ⊆ Ii , for j = 0, . . . , n − 1, and finally I = In . Now for a point x ∈ F assume that x ∈ Ij for some j. If no constraint is applied, Ij+1 = Ij , so x ∈ Ij+1 . Otherwise, Ij+1 = Ij /vj+1 . By Def. 6 x ∈ Ij /vj+1 , so x ∈ Ij+1 . Hence, it holds x ∈ In = I. Again from eq. (8), since the constrain operator only removes points, Ij+1 ⊆ Ij . Therefore, for all i ≤ j, vi ̸∈ Ij , implies vi ̸∈ Ij+1 . By induction to the number of adversarial points in V we take v ̸∈ I, for all v ∈ V, hence I ∩ V = ∅. 9

We assume left associativity of the / operator.



20

M. Papamichail et al.

From Def. 6, for every coordinate i, −ri < vi − xi < ri for every v ∈ V. Hence no adversarial example lies inside the interval s.t. (x + [−r, r]) ∪ V = ∅. Now consider the construction of I from eq. (8) and assume that at some step j it holds V⊥x ⊆ Ij . Applying the next constraint and we take Ij+1 = Ij /vj+1 . Let k = arg maxi |vj+1,i − xi |. If vj+1,i > xi , the new upper bound becomes u′k = max{0, vj+1,i − xi − δ} and by definition of rk we have, rk ≤ vj+1,i − xi − δ. Therefore, xk + rk ≤ xk + u′k . Since all other coordinates remain unchanged we take V⊥x ⊆ Ij+1 . By induction over all adversarial examples, V⊥x ⊆ I. If vj+1,i < xi the new lower bound becomes lk′ = min{0, vj+1,i − xi + δ}. We work analogously as in the previous case and we conclude that V⊥x ⊆ Ij+1 . ■ Theorem 3. (⊤-Operator Optimality) Consider a domain F and an input x ∈ F. Let Q ⊂ F be a set of positive points. The following hold: 1. (Q⊤x) ∪ Q = (Q⊤x). 2. There is no interval J ∈ I(d)|Fx , s.t. x ∈ J, J ∪ Q = J, and J ⊂ (Q⊤x). 3. Let I, J ∈ I(d)|Fx two intervals, s.t. (Q ∪ {x}) ⊆ I, J. Moreover, let I, J be minimal, w.r.t. set inclusion, achieving this property. Then, I = J. 4. For every J ∈ I(d)|Fx , s.t. x ∈ J, and J ∪ Q = J, then ϖ(J) ≥ ϖ(Q⊤x). Proof. The first desideratum results immediately from Def. 7. For the second desideratum, we will prove that if J ⊂ (Q⊤x), then there is some q ∈ Q, s.t. q ∈ / J. Let Q⊤x = x + [−r, r], with r, r ≥ 0 as in Def. 7. Consider the k-th coordinate of the upper endpoint ri . From Def. 7 there is some q ∈ Q, s.t. qk = rk . Since, x ∈ J, we write J = x + [−d, d], with d, d ≥ 0. Since, J ⊂ (Q⊤x), then [−d, d] ⊂ [−r, r]. Thus, there is a coordinate of the upper of lower endpoint of J, that is dominated by the respective coordinate of Q⊤x. W.l.o.g. let dk < rk = qk , thus dk < qk , and q ∈ / J. A contradiction. For the third desideratum, we work as follows. Let I, J be minimal intervals that include Q ∪ x. Then, I ∩ J = I ⊓ J ∈ I(d)|Fx . Moreover, Q ⊆ I ∩ J. Thus, the intersection I ∩ J satisfies the above properties, and is included in both I, J. A contradiction, since we assumed that I, J are minimal. The fourth desideratum follows from the previous. From 2 we established that Q⊤x is minimal. From 3 we establish that the minimal is unique. Finally, the apothem is increasing w.r.t. set inclusion. Thus, Q⊤x is minimum. ■ Proposition 4. Consider a domain F and an input x ∈ F. Let Q ⊂ F be a set of positive points. We assume an ordering in Q, i.e., Q = q1 , q2 , . . . , qn . Let I = [x, x] ⊔ q1 ⊔ q2 · · · ⊔ qn 10 . Then, I = Q⊤x. Proof. W.l.o.g., we assume x = 0. First we show that Alg. 1, under property QI,ν (·) and operator ⊔, terminates after a finite number of steps. To that end, let Ij = [−ℓj , uj ], with ℓj , uj ≥ 0, j ∈ N, be the interval in the j-th iteration. For the sequence of intervals holds,  Ij+1 = Ij ⊔ [qj+1 − δ1, qj+1 + δ1], if ∃ qj+1 ∈ F \ Ij (9) Ij+1 = Ij , otherwise 10

We assume left associativity of the ⊔ operator.

Trustworthy Robustness Certifications in NNs

21

From eq. (9) Ij ⊆ Ij+1 , for j = 0, . . . , n − 1, and finally I = In . Therefore, I0 = x and Ij = x + [−aj , bj ], with aj , bj ≥ 0 and a0 , b0 = = 0. For the positive point qk+1 , the minimum interval update provides aj+1 i j j+1 j max{ai , xi − qj+1,i }, and bi = max{bi , qj+1,i − xi }. After processing all points in Q we take, ani = maxj {xi −qj,i | qj ∈ Q} and bni = maxj {qj+1,i −xi | qj ∈ Q}. So, we have, In = x + [−an , bn ]. By Def. 7, Ri = sup{xi − qi | q ∈ Q} and Ri = sup{qi − xi | q ∈ Q}. Since Q is finite, we take Ri = max{xi − qi | q ∈ Q} = maxj {xi − qj,i } = ani and Ri = maxj {qj,i − xi | q ∈ Q} = bni . Hence, ■ In = x + [−R, R] = Q⊤x. Theorem 4. (Weak ⊥, ⊤-Duality) Consider an input domain F, and a partition into positive points Q and adversarial examples V, i.e., Q ∩ V = ∅ and Q ∪ V = F. Then, for an input x ∈ F, we have (V⊥x) ∩ F ⊆ Q⊤x and for every increasing measure µ : I(d)|Fx → R≥0 of Def. 2, we have µ[(V⊥x) ∩ F] ≤ µ[Q⊤x]. Proof. From 1. in Thm. 2 we have (V⊥x)∩V = ∅. Since Q∩V = ∅, it holds either Q ⊂ (V⊥x) ∩ F or (V⊥x) ∩ F ⊆ Q. If the first inclusion holds, then there exists some x′ ∈ (V⊥x) ∩ F s.t. x′ ̸∈ Q and x′ ̸∈ V. This, in turn, yields Q ∪ V ⊂ F, a contradiction. Therefore, it holds (V⊥x) ⊆ Q. Now, from 1. in Thm. 3 we have that (Q⊤x)∪Q = (Q⊤x), meaning that Q ⊆ (Q⊤x). Combining all together we take (V⊥x) ∩ F ⊆ Q⊤x. Finally, since µ is an increasing measure the inequality µ[(V⊥x) ∩ F] ≤ µ[Q⊤x] follows. ■ A.3

Proofs of Section 4

Theorem 5. Let n be the number of counterexamples returned by the NN verifier. Let tPI,ν be the worst-case time to check whether property PI,ν holds. Finally, let t□ be the worst-case time required by the operator □. Then, the refine & check method of Alg. 1 terminates after O[n · (t□ + tPI,ν )] steps. If □ ∈ {/, ⊔}, then t□ = O(d), and Alg. 1 concludes in O[nd + ntPI,ν ] time. Proof. From lines 2-3 in Alg. 1, that updates the interval I, we have complexity O(t□ + tPI,ν ). Then Alg. 1 is linear to the number of oracle calls, therefore, is O(n). Hence the total time complexity becomes O(n · (t□ + tPI,ν )). Now, consider the potential function Φ : I(d)|F0 → R≥0 s.t., Φ([−ℓ, u]) =

X

ℓi + ui ,

for ℓ, u ≥ 0.

(10)

i∈[d]

For □ = ⊔, we have I0 = [0, 0], and Φ(I0 ) = 0. For every j ∈ [d], the potential is upper-bounded, as proved in Prop. 4 as well, i.e., Φ(Ij ) ≤ Φ(F). Moreover, for every interval properly included in F, the potential function is increasing with Φ(Ij+1 ) ≤ Φ(Ij ) + δ for some δ > 0. Since the potential increases by at least δ at each iteration while remaining bounded, the sequence generated from eq. (10) must converge. Thus, there exists an index k ∈ N, s.t. Ik = Ik+1 , and the algorithm terminates after a finite number of steps, so t⊔ = O(d).

22

M. Papamichail et al.

For □ = /, we have I0 = F, and Φ(I0 ) = Φ(F). Moreover, Φ(Ij ) ≥ 0 for all j ∈ N and for every interval not included in Ij , the potential is strictly decreasing, that is Φ(Ij+1 ) ≤ Φ(Ij ) − δ for some δ > 0. Therefore, there exists an index k ∈ N, s.t. Ik = Ik+1 , and the algorithm terminates after finitely many steps. The number of iterations is bounded by t/ = O(d). The final argument follows plugging into the total complexity of Alg. 1 the time complexity of operators {/, ⊔}. ■ Theorem 6. Consider a set of adversarial examples V ⊂ F, an input x ∈ F, and a constant γ > 0. Moreover, let n = |V|, let d be the dimension s.t. F ⊂ Rd , and let tPI,ν be the worst-case time check whether property PI,ν holds. Then, the existence of a robustness certification I ∈ I(d)|Fx , with x ∈ I, I ∩ V = ∅ and v(I) ≥ γ cannot be decided in poly(n, d, tPI,ν ) time, unless P = NP. 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 [1] if I ⊆ [0, 1]d is a maximum-volume feasible interval, then ∂I contains 0 and the i-th dimension of I is either w or 1. Therefore, the maximum-volume interval I has ℓi = 0 for every i, Q and each ui ∈ {w, 1}, meaning that I = [0, u]. The interval I has volume v(I) = i∈[d] (ui − ℓi ). Applying Th. 2 from [1], graph G has an independent set of size at least k iff there exists an interval I ∈ F of volume at least wk . Consequently, deciding whether there exists any empty interval of volume at least wk is NP-hard. Taking γ = wk and q = 0, every interval of the form [0, u] contains q, so deciding the existence of an empty rectangle that contains the query point q with v(I) ≥ γ is NP-hard. Therefore, the q-MER decision problem is NP-hard, and the proof is complete. ■