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
Source: [https://arxiv.org/html/2606.23858](https://arxiv.org/html/2606.23858)
11institutetext:Foundation for Reasearch and Technology \- Hellas, Heraklion, Greece11email:\{mercoyris,varsosk,fgeo\}@ics\.forth\.gr22institutetext:University of Crete, Heraklion, Greece33institutetext:Catalan Institution for Research and Advanced Studies, Barcelona, Spain33email:jpms@icrea\.cat44institutetext:University of Lleida, Lleida, Spain###### 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 theParallelepipedoNN111[https://github\.com/merkouris148/parallelepipedonn](https://github.com/merkouris148/parallelepipedonn)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\.

## 1Introduction

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](https://arxiv.org/html/2606.23858#bib.bib28),[7](https://arxiv.org/html/2606.23858#bib.bib7)\]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](https://arxiv.org/html/2606.23858#bib.bib30),[20](https://arxiv.org/html/2606.23858#bib.bib20),[18](https://arxiv.org/html/2606.23858#bib.bib18),[12](https://arxiv.org/html/2606.23858#bib.bib12)\]\. 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](https://arxiv.org/html/2606.23858#bib.bib30),[19](https://arxiv.org/html/2606.23858#bib.bib19),[18](https://arxiv.org/html/2606.23858#bib.bib18)\]\. Suppose that in order to consider the network robust, we need to achieve a volume threshold ofv1v\_\{1\}\. However, we calculated a certification of volumev2v\_\{2\}, withv2<v1v\_\{2\}<v\_\{1\}\.*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 apothem\-optimal 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\\varpi\_\{1\}, but we computedϖ2\\varpi\_\{2\}, withϖ2<ϖ1\\varpi\_\{2\}<\\varpi\_\{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 isv2v\_\{2\}and we need to havev1v\_\{1\}, withv1\>v2v\_\{1\}\>v\_\{2\}, we*know*that*no*such certification exists, for this NN\.

We implemented our algorithms in theParallelepipedoNNsystem, 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\.

## 2Multi\-Dimensional Intervals

We begin with some foundational results from Sunaga’s*Interval Algebra*\[[27](https://arxiv.org/html/2606.23858#bib.bib27)\]\. Firstly, we generalize the≤⊆ℝ×ℝ\\leq~\\subseteq\\mathbb\{R\}\\times\\mathbb\{R\}relation to multi\-dimensional spaces\. For two vectorsℓ,𝒖∈ℝd\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\\in\\mathbb\{R\}^\{d\}we writeℓ≤𝒖\\boldsymbol\{\\ell\}\\leq\\boldsymbol\{u\}*iff*ℓi≤ui\\ell\_\{i\}\\leq u\_\{i\}for alli∈\[d\]i\\in\[d\], andℓ<𝒖\\boldsymbol\{\\ell\}<\\boldsymbol\{u\}*iff*ℓi<ui\\ell\_\{i\}<u\_\{i\}for alli∈\[d\]i\\in\[d\]\. Multi\-dimensional intervals are defined as follows:

###### Definition 1\(Multi\-Dimensional Intervals\)

Letℓ,𝒖∈ℝd\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\\in\\mathbb\{R\}^\{d\}, withℓ≤𝒖\\boldsymbol\{\\ell\}\\leq\\boldsymbol\{u\}\. An*interval*\[ℓ,𝒖\]⊂ℝd\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\subset\\mathbb\{R\}^\{d\}is the set of points𝐱∈ℝd\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}such thatℓ≤𝐱≤𝒖\\boldsymbol\{\\ell\}\\leq\\mathbf\{x\}\\leq\\boldsymbol\{u\}\. Finally,𝕀​\(d\)\\mathbb\{I\}\(d\)denotes the space ofdd–dimensional intervals, i\.e\.,𝕀​\(d\)=\{S⊂ℝd∣∃ℓ,𝒖∈ℝd,ℓ≤𝒖,S=\[ℓ,𝒖\]\}\\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\}\]\\\}\.

The multi\-dimensional intervals of Def\.[1](https://arxiv.org/html/2606.23858#Thmdefinition1)are used to formalize the concept of robustness certification\. LetI1,…,IdI\_\{1\},\\dots,I\_\{d\}be the sequence of \(one\-dimensional\) tolerance intervals of a robustness certification\. Recall that we can perturb freely each featureiiwithinIiI\_\{i\}, without breaking the prediction\. Concretely, this robustness certification can be represented by the multi\-dimensional intervalI=I1×⋯×IdI=I\_\{1\}\\times\\cdots\\times I\_\{d\}\.

Assume𝔽⊂ℝd\\mathbb\{F\}\\subset\\mathbb\{R\}^\{d\}be the*input domain*of a particular neural network\. For a given input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, we can express the robustness certifications of𝐱\\mathbf\{x\}as intervals of the form\[𝐱−𝐚,𝐱\+𝐛\]\[\\mathbf\{x\}\-\\mathbf\{a\},\\mathbf\{x\}\+\\mathbf\{b\}\], where𝐚,𝐛≥𝟎\\mathbf\{a\},\\mathbf\{b\}\\geq\\mathbf\{0\}\. Intuitively, the vectors𝐚,𝐛\\mathbf\{a\},\\mathbf\{b\}correspond to the maximum subtractive and additive perturbations not breaking the network’s prediction\. Inversely, for any intervalIIcontaining𝐱\\mathbf\{x\}, there are vectors𝐚,𝐛≥𝟎\\mathbf\{a\},\\mathbf\{b\}\\geq\\mathbf\{0\}, s\.t\.I=\[𝐱−𝐚,𝐱\+𝐛\]I=\[\\mathbf\{x\}\-\\mathbf\{a\},\\mathbf\{x\}\+\\mathbf\{b\}\]\. For the domain𝔽\\mathbb\{F\}and an input𝐱\\mathbf\{x\},𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}denotes the space of all the intervals of𝔽\\mathbb\{F\}containing𝐱\\mathbf\{x\}\.

For any𝐱∈ℝd\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}, we call the interval\[𝐱,𝐱\]=\{𝐱\}\[\\mathbf\{x\},\\mathbf\{x\}\]=\\\{\\mathbf\{x\}\\\}*trivial*\. For a radiusρ\>0\\rho\>0, we call intervals of the form\[𝐱−ρ​𝟏,𝐱\+ρ​𝟏\]\[\\mathbf\{x\}\-\\rho\\mathbf\{1\},\\mathbf\{x\}\+\\rho\\mathbf\{1\}\]*uniform*\. Uniform intervals geometrically represent axis\-aligned*hyper\-cubes*\. Moreover, for any vector𝐯≥𝟎\\mathbf\{v\}\\geq\\mathbf\{0\}, we call intervals of the form\[𝐱−𝐯,𝐱\+𝐯\]\[\\mathbf\{x\}\-\\mathbf\{v\},\\mathbf\{x\}\+\\mathbf\{v\}\]*symmetric*\. Finally,*arbitrary*intervals are characterized by two vectors𝐚,𝐛≥𝟎\\mathbf\{a\},\\mathbf\{b\}\\geq\\mathbf\{0\}, s\.t\.\[𝐱−𝐚,𝐱\+𝐛\]\[\\mathbf\{x\}\-\\mathbf\{a\},\\mathbf\{x\}\+\\mathbf\{b\}\]\. See Fig\.[1](https://arxiv.org/html/2606.23858#S2.F1)\(left\)\.

![Refer to caption](https://arxiv.org/html/2606.23858v1/figures/intro/certifications.png)
![Refer to caption](https://arxiv.org/html/2606.23858v1/figures/intro/objectives.png)

Figure 1:Left: Interval Families: uniform, symmetric, and arbitrary\. Right: Interval Measures:𝒜\\mathcal\{A\}diameter,π\\piperimeter,vvvolume,α\\alphaminimum edge,ϖ\\varpiapothem\.### 2\.1Operations on Intervals, and the Interval Lattice

Recall that we denote the space of intervals in𝔽\\mathbb\{F\}that contain an input𝐱\\mathbf\{x\}with𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\. The space𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}is highly structured by simple algebraic operations\.

###### Definition 2

Let\[ℓ,𝒖\],\[𝒎,𝒏\]∈𝕀​\(d\)\|𝐱𝔽\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\],\[\\boldsymbol\{m\},\\boldsymbol\{n\}\]\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\. We define the operations:

1. 1\.\[ℓ,𝒖\]\+\[𝒎,𝒏\]​=Δ​\[ℓ\+𝒎,𝒖\+𝒏\]\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\+\[\\boldsymbol\{m\},\\boldsymbol\{n\}\]\\overset\{\\Delta\}\{=\}\[\\boldsymbol\{\\ell\}\+\\boldsymbol\{m\},\\boldsymbol\{u\}\+\\boldsymbol\{n\}\]
2. 2\.\[ℓ,𝒖\]⊔\[𝒎,𝒏\]​=Δ​\[min⁡\{ℓ,𝒎\},max⁡\{𝒖,𝒏\}\]\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\sqcup\[\\boldsymbol\{m\},\\boldsymbol\{n\}\]\\overset\{\\Delta\}\{=\}\[\\min\\\{\\boldsymbol\{\\ell\},\\boldsymbol\{m\}\\\},\\max\\\{\\boldsymbol\{u\},\\boldsymbol\{n\}\\\}\]
3. 3\.\[ℓ,𝒖\]⊓\[𝒎,𝒏\]​=Δ​\[max⁡\{ℓ,𝒎\},min⁡\{𝒖,𝒏\}\]\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\sqcap\[\\boldsymbol\{m\},\\boldsymbol\{n\}\]\\overset\{\\Delta\}\{=\}\[\\max\\\{\\boldsymbol\{\\ell\},\\boldsymbol\{m\}\\\},\\min\\\{\\boldsymbol\{u\},\\boldsymbol\{n\}\\\}\]

It is easy to see that𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}is*closed*under the operations in Def\.[2](https://arxiv.org/html/2606.23858#Thmdefinition2)\. The summation of two intervals, corresponds to the well\-known*Minkowski sum*\. We sometimes abuse notation, writing𝐱\+\[ℓ,𝒖\]\\mathbf\{x\}\+\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\], instead of\[𝐱,𝐱\]\+\[ℓ,𝒖\]\[\\mathbf\{x\},\\mathbf\{x\}\]\+\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\(analogously for the other operations\)\. The⊔,⊓\\sqcup,\\sqcapoperations were introduced by Sunaga\[[27](https://arxiv.org/html/2606.23858#bib.bib27)\], 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𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}latttice structure, the lub is given by the*join*operation⊔\\sqcup, and the glb by the*meet*operation⊓\\sqcap\.

###### Theorem 2\.1\(Interval Lattice\[[27](https://arxiv.org/html/2606.23858#bib.bib27)\]\)

The interval space𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, under⊆\\subseteqconstitutes a complete*lattice*with⊔,⊓\\sqcup,\\sqcapas the*meet*and*join*operations, respectively\.

### 2\.2Interval Objectives

We proceed by discussing interval measures\. A*measure*μ:𝕀​\(d\)\|𝐱𝔽→ℝ≥0\\mu\\colon\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\\to\\mathbb\{R\}\_\{\\geq 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 intervalI=𝐱\+\[ℓ,𝒖\]∈𝕀​\(d\)\|𝐱𝔽I=\\mathbf\{x\}\+\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, withℓ≤𝒖\\boldsymbol\{\\ell\}\\leq\\boldsymbol\{u\}\. Then we define the following measures:

Apothem:ϖ​\(I\)\\varpi\(I\)=min⁡\{mini∈\[d\]⁡\(xi−ℓi\),minj∈\[d\]⁡\(uj−xj\)\}=\\min\\Big\\\{\\min\_\{i\\in\[d\]\}\(x\_\{i\}\-\\ell\_\{i\}\),\\min\_\{j\\in\[d\]\}\(u\_\{j\}\-x\_\{j\}\)\\Big\\\}Minimum Edge:α​\(I\)\\alpha\(I\)=mini∈\[d\]⁡ui−ℓi=\\min\_\{i\\in\[d\]\}u\_\{i\}\-\\ell\_\{i\}Perimeter:π​\(I\)\\pi\(I\)=∑i∈\[d\]ui−ℓi=\\sum\_\{i\\in\[d\]\}u\_\{i\}\-\\ell\_\{i\}Volume:v​\(I\)v\(I\)=∏i∈\[d\]ui−ℓi=\\prod\_\{i\\in\[d\]\}u\_\{i\}\-\\ell\_\{i\}\.Diameter:𝒜​\(I\)\\mathcal\{A\}\(I\)=maxi∈\[d\]⁡ui−ℓi=‖ui−ℓi‖∞=\\max\_\{i\\in\[d\]\}u\_\{i\}\-\\ell\_\{i\}=\\\|u\_\{i\}\-\\ell\_\{i\}\\\|\_\{\\infty\}

All the measures of Def\.[3](https://arxiv.org/html/2606.23858#Thmdefinition3)are depicted in Fig\.[1](https://arxiv.org/html/2606.23858#S2.F1)\(right\)\. In our experimental evaluation, we also use the*average edge length*E¯​\(I\)\\overline\{E\}\(I\), defined asE¯​\(I\)=π​\(I\)/d\\overline\{E\}\(I\)=\\pi\(I\)/d\. Apothem222In Euclidean geometry*apothem*is a line between the polygon’s center and a faces\.measures the minimum “slack” between the input𝐱\\mathbf\{x\}and one of the 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𝐱\\mathbf\{x\}and the nearest adversarial example\. Prop\.[3](https://arxiv.org/html/2606.23858#Thmdefinition3)relates the above measures\. We include omitted proofs in App\.[0\.A](https://arxiv.org/html/2606.23858#Pt0.A1)\.

\{restatable\}

propositionnumericalgeometricmean For an intervalI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}and the measures of Def\.[3](https://arxiv.org/html/2606.23858#Thmdefinition3)we have,

𝒜​\(I\)≥1d⋅π​\(I\)≥v​\(I\)d≥α​\(I\)≥2⋅ϖ​\(I\)\\mathcal\{A\}\(I\)\\geq\\frac\{1\}\{d\}\\cdot\\pi\(I\)\\geq\\sqrt\[d\]\{v\(I\)\}\\geq\\alpha\(I\)\\geq 2\\cdot\\varpi\(I\)\(1\)

## 3Robustness 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𝔽\\mathbb\{F\}and a set of adversarial examples𝒱⊂𝔽\\mathcal\{V\}\\subset\\mathbb\{F\}\. Moreover, let𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}be the given input\. A robustness certification will be an intervalI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, s\.t\.𝐱∈I\\mathbf\{x\}\\in I*and*I∩𝒱=∅I\\cap\\mathcal\{V\}=\\varnothing\.

The technicalities on how we obtain the set of adversarial examples𝒱\\mathcal\{V\}will be discussed in Section[4](https://arxiv.org/html/2606.23858#S4)\. 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𝔽\\mathbb\{F\}breaking the prediction\. This lets us focus on a subtle, but important problem\.*From all the candidate intervalsJ⊆𝔽∖𝒱J\\subseteq\\mathbb\{F\}\\setminus\\mathcal\{V\}, which one should we choose?*

We proceed in two steps\. Firstly, we consider the case of excluding a single adversarial example𝐯∈𝒱\\mathbf\{v\}\\in\\mathcal\{V\}, defining the apothem\-optimal, “small\-step”333“Small\-step” operators deal with one example, while “big\-step” with sets\.,*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\.1Small\-Step Robustness

![Refer to caption](https://arxiv.org/html/2606.23858v1/figures/robustness/small-step-1.png)
![Refer to caption](https://arxiv.org/html/2606.23858v1/figures/robustness/small-step-2.png)

Figure 2:Left: The constrain operator\. Right: How the domain space can be partitioned in cones\. The coneCi¯\\overline\{C\_\{i\}\}contains all the adversarial examples that result in modifying theii\-th coordinate of the upper endpoint𝒖\\boldsymbol\{u\}\.Now we discuss our “small\-step” robustness operator\. For an input𝐱\\mathbf\{x\}, consider an intervalIIs\.t\.𝐱∈I\\mathbf\{x\}\\in I\. Moreover, let𝐯∈I\\mathbf\{v\}\\in Ibe an adversarial example we want to exclude\. Our small\-step robustness operator will do just that, excluding the adversarial example𝐯\\mathbf\{v\}from the intervalII, in an*apothem\-optimal*manner\. We call this operation*constrain*, and denote it byI/𝐯I/\\mathbf\{v\}\. Subsequently, letI′=I/𝐯I^\{\\prime\}=I/\\mathbf\{v\}\.

Recall that the intervals are essentially sets of2​d2dinequalities, each corresponding to a lower or upper bound for one of theddcoordinates of the input space, written compactly asI=𝐱\+\[ℓ,𝒖\]I=\\mathbf\{x\}\+\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\], withℓ≤𝟎≤𝒖\\boldsymbol\{\\ell\}\\leq\\mathbf\{0\}\\leq\\boldsymbol\{u\}\. To ensure that𝐯∉I′\\mathbf\{v\}\\notin I^\{\\prime\}, it suffices to ensure that one of these inequalities fails\. To achieve apothem\-optimality, we choose the dimensionk∈\[d\]k\\in\[d\]for which\|vk−xk\|\|v\_\{k\}\-x\_\{k\}\|is maximum\. Ifvk−xk\>0v\_\{k\}\-x\_\{k\}\>0, then the upper bound must be reduced to exclude𝐯\\mathbf\{v\}, by changing thekk\-th dimension of𝒖\\boldsymbol\{u\}to produce a𝒖′\\boldsymbol\{u\}^\{\\prime\}that leaves𝐯\\mathbf\{v\}out ofI′I^\{\\prime\}; otherwise the lower bound must be increased accordingly\.

An important technicality here is that we use a precision constantδ\>0\\delta\>0to ensure a “meaningful” reduction of the interval\. When modifying the upper bound, we setuk′=vk−xk−δu\_\{k\}^\{\\prime\}=v\_\{k\}\-x\_\{k\}\-\\delta, and symmetrically for the lower bound\. This serves two purposes\. First, it excludes𝐯\\mathbf\{v\}in a “strict sense” \(otherwise𝐯\\mathbf\{v\}would be in the border ofI′I^\{\\prime\}\)\. 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](https://arxiv.org/html/2606.23858#S3.F2)\(left\) and defined formally below\.

###### Definition 4\(Constrain Operator\)

Consider an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, an intervalI=𝐱\+\[ℓ,𝒖\]I=\\mathbf\{x\}\+\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\], withℓ≤𝟎≤𝒖\\boldsymbol\{\\ell\}\\leq\\mathbf\{0\}\\leq\\boldsymbol\{u\}, an adversarial example𝐯∈I\\mathbf\{v\}\\in I, and a precision constantδ\>0\\delta\>0\. Letk=a​r​g​m​a​xi∈\[d\]​\{\|vi−xi\|\}k=argmax\_\{i\\in\[d\]\}\\\{\|v\_\{i\}\-x\_\{i\}\|\\\}\. We define the*constrain operation*I/δ𝐯=𝐱\+\[ℓ′,𝒖′\]I/\_\{\\delta\}~\\mathbf\{v\}=\\mathbf\{x\}\+\[\\boldsymbol\{\\ell\}^\{\\prime\},\\boldsymbol\{u\}^\{\\prime\}\], where:

- •Ifvk−xk\>0v\_\{k\}\-x\_\{k\}\>0thenℓ′=ℓ\\boldsymbol\{\\ell\}^\{\\prime\}=\\boldsymbol\{\\ell\},ui′=uiu\_\{i\}^\{\\prime\}=u\_\{i\}for alli∈\[d\]∖\{k\}i\\in\[d\]\\setminus\\\{k\\\}anduk′=max⁡\{0,vk−xk−δ\}u\_\{k\}^\{\\prime\}=\\max\\\{0,v\_\{k\}\-x\_\{k\}\-\\delta\\\}\.
- •Ifvk−xk<0v\_\{k\}\-x\_\{k\}<0thenℓi′=ℓi\\ell\_\{i\}^\{\\prime\}=\\ell\_\{i\}for alli∈\[d\]∖\{k\}i\\in\[d\]\\setminus\\\{k\\\},ℓk′=min⁡\{0,vk−xk\+δ\}\\ell\_\{k\}^\{\\prime\}=\\min\\\{0,v\_\{k\}\-x\_\{k\}\+\\delta\\\}, and𝒖′=𝒖\\boldsymbol\{u\}^\{\\prime\}=\\boldsymbol\{u\}\.

Note thatvk−xk≠0v\_\{k\}\-x\_\{k\}\\neq 0because, by construction,𝐱≠𝐯\\mathbf\{x\}\\neq\\mathbf\{v\}\. The reason formax\\maxandmin\\minin the definition is to ensure that𝐱∈I′\\mathbf\{x\}\\in I^\{\\prime\}, i\.e\.,ℓ′≤𝟎≤𝒖′\\boldsymbol\{\\ell\}^\{\\prime\}\\leq\\mathbf\{0\}\\leq\\boldsymbol\{u\}^\{\\prime\}\. Subsequently, we omitδ\\delta, writingI/𝐯I/\\mathbf\{v\}\. The operator’s apothem\-optimality is established below\.

\{restatable\}

propositionintervalexclusion Consider an intervalI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}and a point𝐯∈I\\mathbf\{v\}\\in I\. For any intervalJ∈𝕀​\(d\)\|𝐱𝔽J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, with𝐯∉J\\mathbf\{v\}\\notin JandJ⊆IJ\\subseteq I, we haveϖ​\(J\)≤ϖ​\(I/𝐯\)\\varpi\(J\)\\leq\\varpi\(I/\\mathbf\{v\}\)\.

###### Proof

W\.l\.o\.g\. let𝐱=𝟎\\mathbf\{x\}=\\mathbf\{0\}\. For anyJ∈𝕀​\(d\)\|𝐱𝔽J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}and𝐯∈𝔽\\mathbf\{v\}\\in\\mathbb\{F\}, it holds𝐯∉J\\mathbf\{v\}\\notin J,*iff*maxi∈\[d\]⁡\|vi\|\>ϖ​\(J\)\\max\_\{i\\in\[d\]\}\|v\_\{i\}\|\>\\varpi\(J\)\. Also,ϖ​\(I/𝐯\)=min⁡\{ϖ​\(I\),maxi∈\[d\]⁡\|vi\|\}\\varpi\(I/\\mathbf\{v\}\)=\\min\\\{\\varpi\(I\),\\max\_\{i\\in\[d\]\}\|v\_\{i\}\|\\\}\.■\\blacksquare

### 3\.2Big\-Step Robustness

![Refer to caption](https://arxiv.org/html/2606.23858v1/figures/robustness/big-step.png)
![Refer to caption](https://arxiv.org/html/2606.23858v1/figures/robustness/dual.png)

Figure 3:Left: The bottom interval𝒱⊥𝐱\\mathcal\{V\}\\bot\\mathbf\{x\}\. Right: The dual top interval𝒬⊤𝐱\\mathcal\{Q\}\\top\\mathbf\{x\}\.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𝔽\\mathbb\{F\}into2​d2dregions444Corresponding to polyhedral cones,C=\{𝐱∈ℝn∣A​𝐱≤𝟎\}C=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{n\}\\mid A\\mathbf\{x\}\\leq\\mathbf\{0\}\\\},A∈ℝm×nA\\in\\mathbb\{R\}^\{m\\times n\}\., denoted byCi¯,Ci¯\\overline\{C\_\{i\}\},\\underline\{C\_\{i\}\}, fori∈\[d\]i\\in\[d\], see Fig\.[2](https://arxiv.org/html/2606.23858#S3.F2)\(right\)\.

###### Definition 5\(Cone Partition\)

Consider the domain𝔽⊂ℝd\\mathbb\{F\}\\subset\\mathbb\{R\}^\{d\}, and an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}\. The cone partition w\.r\.t\.𝐱\\mathbf\{x\}is defined by the sequence\{Ci¯,Ci¯\}i∈\[d\]\\\{\\underline\{C\_\{i\}\},\\overline\{C\_\{i\}\}\\\}\_\{i\\in\[d\]\}, where

C¯i=\{𝐯∈𝔽\|vi≤xi,∀j∈\[d\]​\|vi−xi\|≥\|vj−xj\|\},C¯i=\{𝐯∈𝔽\|vi≥xi,∀j∈\[d\]​\|vi−xi\|≥\|vj−xj\|\}\.\\begin\{split\}&\\underline\{C\}\_\{i\}=\\left\\\{\\mathbf\{v\}\\in\\mathbb\{F\}~\\big\|~v\_\{i\}\\leq x\_\{i\},\\forall j\\in\[d\]~\|v\_\{i\}\-x\_\{i\}\|\\geq\|v\_\{j\}\-x\_\{j\}\|\\right\\\},\\\\ &\\overline\{C\}\_\{i\}=\\left\\\{\\mathbf\{v\}\\in\\mathbb\{F\}~\\big\|~v\_\{i\}\\geq x\_\{i\},\\forall j\\in\[d\]~\|v\_\{i\}\-x\_\{i\}\|\\geq\|v\_\{j\}\-x\_\{j\}\|\\right\\\}\.\\end\{split\}\(2\)

For a given set of adversarial examples𝒱\\mathcal\{V\}, let𝒱⊥𝐱\\mathcal\{V\}\\bot\\mathbf\{x\}denote the*bottom interval*, where\(𝒱⊥𝐱\)∩𝒱=∅\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathcal\{V\}=\\varnothing, see Figure[3](https://arxiv.org/html/2606.23858#S3.F3)\(Left\)\. Since𝐱∈\(𝒱⊥𝐱\)\\mathbf\{x\}\\in\(\\mathcal\{V\}\\bot\\mathbf\{x\}\), we write the bottom interval as𝒱⊥𝐱=𝐱\+\[−𝐫¯,𝐫¯\]\\mathcal\{V\}\\bot\\mathbf\{x\}=\\mathbf\{x\}\+\[\-\\underline\{\\mathbf\{r\}\},\\overline\{\\mathbf\{r\}\}\], with𝐫¯,𝐫¯≥𝟎\\underline\{\\mathbf\{r\}\},\\overline\{\\mathbf\{r\}\}\\geq\\mathbf\{0\}\. Thekk\-th coordinate of the upper endpoint𝐫¯\\overline\{\\mathbf\{r\}\}is set to the*minimum*coordinate\-wise absolute distance\|xk−vk\|\|x\_\{k\}\-v\_\{k\}\|\. We work similarly for thekk\-th coordinate of the lower endpoint𝐫¯\\underline\{\\mathbf\{r\}\}\.

###### Definition 6\(⊥\\bot\-Operator\)

Consider a domain𝔽\\mathbb\{F\}and an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}\. Let𝒱⊂𝔽\\mathcal\{V\}\\subset\\mathbb\{F\}be a set of adversarial examples\. Moreover, assume the valuesri¯,ri¯\>0\\underline\{r\_\{i\}\},\\overline\{r\_\{i\}\}\>0, wherer¯i=inf\{xi−vi∣𝐯∈Ci¯∩𝒱\}\\underline\{r\}\_\{i\}=\\inf\\\{x\_\{i\}\-v\_\{i\}\\mid\\mathbf\{v\}\\in\\underline\{C\_\{i\}\}\\cap\\mathcal\{V\}\\\}andr¯i=inf\{vi−xi∣𝐯∈Ci¯∩𝒱\}\\overline\{r\}\_\{i\}=\\inf\\\{v\_\{i\}\-x\_\{i\}\\mid\\mathbf\{v\}\\in\\overline\{C\_\{i\}\}\\cap\\mathcal\{V\}\\\}\. Then,𝒱⊥𝐱\\mathcal\{V\}\\bot\\mathbf\{x\}denotes the bottom interval, where𝒱⊥𝐱=𝐱\+\[−𝐫¯,𝐫¯\]\\mathcal\{V\}\\bot\\mathbf\{x\}=\\mathbf\{x\}\+\[\-\\underline\{\\mathbf\{r\}\},\\overline\{\\mathbf\{r\}\}\]\.

Observe that, by definition, the bottom interval can be*unbounded*\. Indeed, if one of the cones is empty, e\.g\.,Ci¯=∅\\overline\{C\_\{i\}\}=\\varnothing, then the corresponding coordinate\-wise absolute distance approaches infinity, i\.e\.,ri¯→\+∞\\overline\{r\_\{i\}\}\\to\+\\infty\. This happens trivially, when inputs lay at the border of the domain𝔽\\mathbb\{F\}, thusCi¯∩𝔽=∅\\overline\{C\_\{i\}\}\\cap\\mathbb\{F\}=\\varnothing\. Hence, no adversarial examples exist\. Note that unbounded intervals can still have bounded apothem, unless equal toℝd\\mathbb\{R\}^\{d\}\. We discuss this issue again in Sec\.[5](https://arxiv.org/html/2606.23858#S5)\. Subsequently, we show that the bottom operator is apothem optimal\.

###### Theorem 3\.1\(⊥\\bot\-Operator Optimality\)

Consider a domain𝔽\\mathbb\{F\}and an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}\. Let𝒱⊂𝔽\\mathcal\{V\}\\subset\\mathbb\{F\}be a set of adversarial examples\. The following hold:

1. 1\.\(𝒱⊥𝐱\)∩𝒱=∅\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathcal\{V\}=\\varnothing\.
2. 2\.For everyJ∈𝕀​\(d\)\|𝐱𝔽J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, s\.t\.𝐱∈J\\mathbf\{x\}\\in JandJ∩𝒱=∅J\\cap\\mathcal\{V\}=\\varnothing, we haveϖ​\(J\)≤ϖ​\(𝒱⊥𝐱\)\\varpi\(J\)\\leq\\varpi\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\.

###### Proof

The first desideratum is trivial from Def\.[6](https://arxiv.org/html/2606.23858#Thmdefinition6)\. We prove the second\. W\.l\.o\.g\. let the apothem be achieved by the coordinaterk¯\\overline\{r\_\{k\}\}\. From the Def\.[6](https://arxiv.org/html/2606.23858#Thmdefinition6)there is a adversarial example𝐯∈𝒱\\mathbf\{v\}\\in\\mathcal\{V\}, s\.t\.rk¯=vk\\overline\{r\_\{k\}\}=v\_\{k\}\. Assume the intervalJ=𝐱\+\[ℓ,𝒖\]J=\\mathbf\{x\}\+\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\],ℓ≤𝟎≤𝒖\\boldsymbol\{\\ell\}\\leq\\mathbf\{0\}\\leq\\boldsymbol\{u\}, withJ∩𝒱=∅J\\cap\\mathcal\{V\}=\\varnothing\. For sake of contradiction,ϖ​\(J\)\>ϖ​\(𝒱⊥𝐱\)\\varpi\(J\)\>\\varpi\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\. It holds,uk≥ϖ​\(J\)\>rku\_\{k\}\\geq\\varpi\(J\)\>r\_\{k\}\. Thus,uk\>vku\_\{k\}\>v\_\{k\}\. SinceJ∩𝒱=∅J\\cap\\mathcal\{V\}=\\varnothing, there is a coordinatejj, s\.t\.uj≤vju\_\{j\}\\leq v\_\{j\}\. However,ϖ​\(J\)≤uj≤vj≤vk≤rk=ϖ​\(𝒱⊥𝐱\)<ϖ​\(J\)\\varpi\(J\)\\leq u\_\{j\}\\leq v\_\{j\}\\leq v\_\{k\}\\leq r\_\{k\}=\\varpi\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)<\\varpi\(J\), where we havevj≤vkv\_\{j\}\\leq v\_\{k\}, since𝐯∈C¯k\\mathbf\{v\}\\in\\overline\{C\}\_\{k\}\. A contradiction\.■\\blacksquare

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\.

\{restatable\}

propositionbottranslation Consider a domain𝔽\\mathbb\{F\}, and an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}\. Let𝒱⊂𝔽\\mathcal\{V\}\\subset\\mathbb\{F\}be a set of adversarial examples\. We assume an ordering in𝒱\\mathcal\{V\}, i\.e\.,𝒱=𝐯1,𝐯2,…,𝐯n\\mathcal\{V\}=\\mathbf\{v\}\_\{1\},\\mathbf\{v\}\_\{2\},\\dots,\\mathbf\{v\}\_\{n\}\. LetI=𝔽/𝐯1/𝐯2​⋯/𝐯nI=\\mathbb\{F\}~/\\mathbf\{v\}\_\{1\}~/\\mathbf\{v\}\_\{2\}~\\cdots~/\\mathbf\{v\}\_\{n\}555We assume left associativity of the//operator\.\. Then,𝐱∈I\\mathbf\{x\}\\in I,I∩𝒱=∅I\\cap\\mathcal\{V\}=\\varnothing, andI⊇𝒱⊥𝐱I\\supseteq\\mathcal\{V\}\\bot\\mathbf\{x\}\.

### 3\.3Dual 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𝔽\\mathbb\{F\}and input𝐱\\mathbf\{x\}, we take a set of positive inputs𝒬⊂𝔽\\mathcal\{Q\}\\subset\\mathbb\{F\}, and compute an intervalI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, s\.t\.𝐱∈I\\mathbf\{x\}\\in IandI∪𝒬=II\\cup\\mathcal\{Q\}=I\.

The intervalIIis obtained by the top operator𝒬⊤𝐱\\mathcal\{Q\}\\top\\mathbf\{x\}, see Fig\.[3](https://arxiv.org/html/2606.23858#S3.F3)\(Right\)\. We work symmetrically to the bottom operator\. In particular, the dual certification can be written in the form𝒬⊤𝐱=𝐱\+\[−𝐑¯,𝐑¯\]\\mathcal\{Q\}\\top\\mathbf\{x\}=\\mathbf\{x\}\+\[\-\\underline\{\\mathbf\{R\}\},\\overline\{\\mathbf\{R\}\}\], with𝐑¯,𝐑¯≥𝟎\\underline\{\\mathbf\{R\}\},\\overline\{\\mathbf\{R\}\}\\geq\\mathbf\{0\}\. Now theii\-th coordinateRi¯\\overline\{R\_\{i\}\}is set to the*maximum*coordinate\-wise absolute distance between𝐱\\mathbf\{x\}and the positive points of𝒬\\mathcal\{Q\}\. For𝐑¯\\underline\{\\mathbf\{R\}\}we work similarly\.

###### Definition 7\(⊤\\top\-Operator\)

Consider a domain𝔽\\mathbb\{F\}and an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}\. Let𝒬⊂𝔽\\mathcal\{Q\}\\subset\\mathbb\{F\}be a set of positive points\. Moreover, assume the valuesRi¯,Ri¯\>0\\underline\{R\_\{i\}\},\\overline\{R\_\{i\}\}\>0, whereRi¯=sup\{xi−qi∣𝐪∈𝒬\}\\underline\{R\_\{i\}\}=\\sup\\\{x\_\{i\}\-q\_\{i\}\\mid\\mathbf\{q\}\\in\\mathcal\{Q\}\\\}andRi¯=sup\{qi−xi∣𝐪∈∩𝒬\}\\overline\{R\_\{i\}\}=\\sup\\\{q\_\{i\}\-x\_\{i\}\\mid\\mathbf\{q\}\\in\\cap\\mathcal\{Q\}\\\}\. Then,𝒬⊤𝐱\\mathcal\{Q\}\\top\\mathbf\{x\}denotes the top interval, where𝒬⊤𝐱=𝐱\+\[−𝐑¯,𝐑¯\]\\mathcal\{Q\}\\top\\mathbf\{x\}=\\mathbf\{x\}\+\[\-\\underline\{\\mathbf\{R\}\},\\overline\{\\mathbf\{R\}\}\]\.

Note that since𝒬⊂𝔽\\mathcal\{Q\}\\subset\\mathbb\{F\}, the top interval is*always bounded*\. We prove the optimality of the top operator in Thm\.[7](https://arxiv.org/html/2606.23858#Thmdefinition7)\. However, we follow a different approach than the Thm\.[3\.1](https://arxiv.org/html/2606.23858#S3.Thmtheorem1)\. 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𝒬\\mathcal\{Q\}\. Finally, we show that any minimal interval including𝒬\\mathcal\{Q\}is*unique*\. This results in apothem optimality\.

\{restatable\}

theoremtopoperator*\(⊤\\top\-Operator Optimality\)*Consider a domain𝔽\\mathbb\{F\}and an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}\. Let𝒬⊂𝔽\\mathcal\{Q\}\\subset\\mathbb\{F\}be a set of positive points\. The following hold:

1. 1\.\(𝒬⊤𝐱\)∪𝒬=\(𝒬⊤𝐱\)\(\\mathcal\{Q\}\\top\\mathbf\{x\}\)\\cup\\mathcal\{Q\}=\(\\mathcal\{Q\}\\top\\mathbf\{x\}\)\.
2. 2\.There is no intervalJ∈𝕀​\(d\)\|𝐱𝔽J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, s\.t\.𝐱∈J\\mathbf\{x\}\\in J,J∪𝒬=JJ\\cup\\mathcal\{Q\}=J, andJ⊂\(𝒬⊤𝐱\)J\\subset\(\\mathcal\{Q\}\\top\\mathbf\{x\}\)\.
3. 3\.LetI,J∈𝕀​\(d\)\|𝐱𝔽I,J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}two intervals, s\.t\.\(𝒬∪\{𝐱\}\)⊆I,J\(\\mathcal\{Q\}\\cup\\\{\\mathbf\{x\}\\\}\)\\subseteq I,J\. Moreover, letI,JI,Jbe*minimal*, w\.r\.t\. set inclusion, achieving this property\. Then,I=JI=J\.
4. 4\.For everyJ∈𝕀​\(d\)\|𝐱𝔽J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, s\.t\.𝐱∈J\\mathbf\{x\}\\in J, andJ∪𝒬=JJ\\cup\\mathcal\{Q\}=J, thenϖ​\(J\)≥ϖ​\(𝒬⊤𝐱\)\\varpi\(J\)\\geq\\varpi\(\\mathcal\{Q\}\\top\\mathbf\{x\}\)\.

###### Proof\(Sketch\)

*1\.*Immediate consequence of Def\.[7](https://arxiv.org/html/2606.23858#Thmdefinition7)\.*2\.*We prove that ifJ⊂\(𝒬⊤𝐱\)J\\subset\(\\mathcal\{Q\}\\top\\mathbf\{x\}\), then there is some𝐪∈Q\\mathbf\{q\}\\in Q, s\.t\.𝐪∉J\\mathbf\{q\}\\notin J\.*3\.*LetI,JI,Jbe minimal intervals\. Then we prove that the intersectionI∩JI\\cap Jalso includes𝒬∪\{𝐱\}\\mathcal\{Q\}\\cup\\\{\\mathbf\{x\}\\\}\. Thus, reaching a contradiction\.*4\.*Follows from the previous results\.■\\blacksquare

Again, the top interval can be translated in a sequence of small\-step interval operations\. In particular, we use the join operator⊔\\sqcupof Def\.[2](https://arxiv.org/html/2606.23858#Thmdefinition2)to include the points in𝒬\\mathcal\{Q\}\. We abuse the notation writingI⊔𝐪I\\sqcup\\mathbf\{q\}, instead ofI⊔\[𝐪,𝐪\]I\\sqcup\[\\mathbf\{q\},\\mathbf\{q\}\]\.

\{restatable\}

propositiontoptranslation Consider a domain𝔽\\mathbb\{F\}and an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}\. Let𝒬⊂𝔽\\mathcal\{Q\}\\subset\\mathbb\{F\}be a set of positive points\. We assume an ordering in𝒬\\mathcal\{Q\}, i\.e\.,𝒬=𝐪1,𝐪2,…,𝐪n\\mathcal\{Q\}=\\mathbf\{q\}\_\{1\},\\mathbf\{q\}\_\{2\},\\dots,\\mathbf\{q\}\_\{n\}\. LetI=\[𝐱,𝐱\]⊔𝐪1⊔𝐪2​⋯⊔𝐪nI=\[\\mathbf\{x\},\\mathbf\{x\}\]\\sqcup\\mathbf\{q\}\_\{1\}\\sqcup\\mathbf\{q\}\_\{2\}\\cdots\\sqcup\\mathbf\{q\}\_\{n\}666We assume left associativity of the⊔\\sqcupoperator\.\. Then,I=𝒬⊤𝐱I=\\mathcal\{Q\}\\top\\mathbf\{x\}\.

We close our discussion on the dual certification by establishing the \(weak\) duality of the bottom and top operators in the following theorem\.

\{restatable\}

theoremduality*\(Weak⊥,⊤\\bot,\\top\-Duality\)*Consider an input domain𝔽\\mathbb\{F\}, and a partition into positive points𝒬\\mathcal\{Q\}and adversarial examples𝒱\\mathcal\{V\}, i\.e\.,𝒬∩𝒱=∅\\mathcal\{Q\}\\cap\\mathcal\{V\}=\\varnothingand𝒬∪𝒱=𝔽\\mathcal\{Q\}\\cup\\mathcal\{V\}=\\mathbb\{F\}\. Then, for an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, we have\(𝒱⊥𝐱\)∩𝔽⊆𝒬⊤𝐱\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}\\subseteq\\mathcal\{Q\}\\top\\mathbf\{x\}and for every increasing measureμ:𝕀​\(d\)\|𝐱𝔽→ℝ≥0\\mu\\colon\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\\to\\mathbb\{R\}\_\{\\geq 0\}of Def\.[2](https://arxiv.org/html/2606.23858#Thmdefinition2), we haveμ​\[\(𝒱⊥𝐱\)∩𝔽\]≤μ​\[𝒬⊤𝐱\]\\mu\[\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}\]\\leq\\mu\[\\mathcal\{Q\}\\top\\mathbf\{x\}\]\.

Note that since the bottom interval may be unbounded, we take the intersection\(𝒱⊥𝐱\)∩𝔽\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{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 classccare positive\. The rest of the points are adversarial examples\.

## 4Algorithms

In this section we discuss how the notions of Sec\.[3](https://arxiv.org/html/2606.23858#S3)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\.2](https://arxiv.org/html/2606.23858#Thmproofx2)and[3\.3](https://arxiv.org/html/2606.23858#Thmproofx3)\. However, for NNs we cannot have explicit descriptions of the adversarial examples𝒱\\mathcal\{V\}or positive points𝒬\\mathcal\{Q\}\. Instead, we only have the description of the NN, its weights, biases and activation functions\. Using this, we construct first order formulas𝒬,𝒮\\mathscr\{Q\},\\mathscr\{S\}that are satisfied only for points in𝒱,𝒬\\mathcal\{V\},\\mathcal\{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](https://arxiv.org/html/2606.23858#bib.bib21),[5](https://arxiv.org/html/2606.23858#bib.bib5)\]\. Using existing MILP solvers \(e\.g\. GLPK777[https://www\.gnu\.org/software/glpk/](https://www.gnu.org/software/glpk/)\), 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](https://arxiv.org/html/2606.23858#bib.bib15),[31](https://arxiv.org/html/2606.23858#bib.bib31)\]software for NN verification, which we also use in ourParallelepipedoNNsoftware\.

Therefore, despite not having an explicit description of the𝒱,𝒬\\mathcal\{V\},\\mathcal\{Q\}sets, we can construct*oracles*\(first\-order formulas, solvable with a MILP solver\)𝒱,𝒬\\mathscr\{V\},\\mathscr\{Q\}, which either*assert*that an intervalIIis included in a set𝒫∈\{𝒱,𝒬\}\\mathcal\{P\}\\in\\\{\\mathcal\{V\},\\mathcal\{Q\}\\\}, or return a*counterexample*𝐩∈I∖𝒫\\mathbf\{p\}\\in I\\setminus\\mathcal\{P\}\. Then, we use the counterexample𝐩\\mathbf\{p\}to refine the current interval using an operator□∈\{/,⊔\}\\square\\in\\\{/,\\sqcup\\\}\.

### 4\.1From Abstract Sets to Neural Networks

Assume the input dimensiondin\{d\_\{\\text\{in\}\}\}and the output dimensiondoutd\_\{\\text\{out\}\}\. Let𝔽⊂ℝdin\\mathbb\{F\}\\subset\\mathbb\{R\}^\{\{d\_\{\\text\{in\}\}\}\}denote the input \(feature\) space and𝕊⊂ℝdout\\mathbb\{S\}\\subset\\mathbb\{R\}^\{d\_\{\\text\{out\}\}\}denote the output \(score\) space\. A NN is a function of the formσ:𝔽→𝕊\\sigma\\colon\\mathbb\{F\}\\to\\mathbb\{S\}\. In this work we are interested in ReLU activated NNs\. For the one\-dimensional case, the ReLU functionr:ℝ→ℝ≥0r\\colon\\mathbb\{R\}\\to\\mathbb\{R\}\_\{\\geq 0\}is defined asr​\(x\)=max⁡\(x,0\)r\(x\)=\\max\(x,0\)\. For thedd\-dimensional case we have𝐫:ℝd→ℝ≥𝟎d\\mathbf\{r\}\\colon\\mathbb\{R\}^\{d\}\\to\\mathbb\{R\}^\{d\}\_\{\\geq\\mathbf\{0\}\}, where𝐫​\(𝐱\)=\(r​\(x1\),…,r​\(xd\)\)\\mathbf\{r\}\(\\mathbf\{x\}\)=\(r\(x\_\{1\}\),\\dots,r\(x\_\{d\}\)\)\. We follow the definition in\[[4](https://arxiv.org/html/2606.23858#bib.bib4)\]\.

###### Definition 8\(Neural Network Classifiers\)

A*neural network*σ:𝔽→𝕊\\sigma\\colon\\mathbb\{F\}\\to\\mathbb\{S\}, with𝔽⊂ℝdin,𝕊⊂ℝdout\\mathbb\{F\}\\subset\\mathbb\{R\}^\{\{d\_\{\\text\{in\}\}\}\},\\mathbb\{S\}\\subset\\mathbb\{R\}^\{d\_\{\\text\{out\}\}\}is described as the tupleσ=⟨L,D,W,B⟩\\sigma=\\langle L,D,W,B\\rangle, where:

- •L∈ℕL\\in\\mathbb\{N\}denotes the number of*layers*\.
- •DDdenotes the*architecture*, i\.e\. a sequencedin=d0,d1,…,dL−1,dL=dout\{d\_\{\\text\{in\}\}\}=d\_\{0\},d\_\{1\},\\dots,d\_\{L\-1\},d\_\{L\}=d\_\{\\text\{out\}\}\.
- •WWdenotes the sequence of*weight matrices*, s\.t\.W\(i\)∈ℝdi×di−1W^\{\(i\)\}\\in\\mathbb\{R\}^\{d\_\{i\}\\times d\_\{i\-1\}\}, fori∈\[L\]i\\in\[L\]
- •BBdenotes a sequence of*biases*s\.t\.𝐛\(i\)∈ℝdi\\mathbf\{b\}^\{\(i\)\}\\in\\mathbb\{R\}^\{d\_\{i\}\}fori∈\[L\]i\\in\[L\]\.

The value ofσ​\(𝐱\)\\sigma\(\\mathbf\{x\}\)is given as the valueσ\(L\)\\sigma^\{\(L\)\}in the system of equations below\.

σ\(0\)=𝐱σ\(i\)=𝐫​\[W\(i\)​σ\(i−1\)\+𝐛\(i\)\],∀i∈\[L\]\}\\left\.\\begin\{array\}\[\]\{ll\}\\sigma^\{\(0\)\}&=\\mathbf\{x\}\\\\ \\sigma^\{\(i\)\}&=\\mathbf\{r\}\[W^\{\(i\)\}\\sigma^\{\(i\-1\)\}\+\\mathbf\{b\}^\{\(i\)\}\],\\quad\\forall i\\in\[L\]\\end\{array\}\\right\\\}\(3\)For classification problems, we also assume a set of classes𝒞\\mathcal\{C\}, s\.t\.\|𝒞\|=dout\|\\mathcal\{C\}\|=d\_\{\\text\{out\}\}\. A classifier is a function of the formκ:𝔽→𝒞\\kappa\\colon\\mathbb\{F\}\\to\\mathcal\{C\}, whereκ​\(𝐱\)=arg⁡maxi∈dout⁡σ​\(𝐱\)\\kappa\(\\mathbf\{x\}\)=\\arg\\max\_\{i\\in d\_\{\\text\{out\}\}\}\\sigma\(\\mathbf\{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ν\\nube that formula\. For every input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}and every output𝐲∈𝕊\\mathbf\{y\}\\in\\mathbb\{S\}the pair*satisfies*ν\\nuif and only if the networkσ​\(⋅\)\\sigma\(\\cdot\)with input𝐱\\mathbf\{x\}outputs𝐲\\mathbf\{y\}\. Now assume a fixed input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}and an intervalI=\[ℓ,𝒖\]∈𝕀​\(din\)\|𝐱𝔽I=\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\in\\mathbb\{I\}\(\{d\_\{\\text\{in\}\}\}\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, s\.t\.𝐱∈I\\mathbf\{x\}\\in I\. We have the following\.

𝒱I,ν​\(𝐩\)\\displaystyle\\mathscr\{V\}\_\{I,\\nu\}\(\\mathbf\{p\}\)≡\(⋀i∈\[din\]ℓi<pi∧pi<ui\)∧ν​\(𝐩,𝐲\)∧\(⋁j≠cyj−yc\>ϵ\)\\displaystyle\\equiv~\\left\(\\bigwedge\_\{i\\in\[\{d\_\{\\text\{in\}\}\}\]\}\\ell\_\{i\}<p\_\{i\}\\land p\_\{i\}<u\_\{i\}\\right\)~\\land~\\nu\(\\mathbf\{p\},\\mathbf\{y\}\)~\\land~\\left\(\\bigvee\_\{j\\neq c\}y\_\{j\}\-y\_\{c\}\>\\epsilon\\right\)\(4\)𝒬I,ν​\(𝐩\)\\displaystyle\\mathscr\{Q\}\_\{I,\\nu\}\(\\mathbf\{p\}\)≡\(⋁i∈\[din\]pi<ℓi∨ui<pi\)∧ν​\(𝐩,𝐲\)∧\(⋀j≠cyc−yj\>ϵ\)\\displaystyle\\equiv\\left\(\\bigvee\_\{i\\in\[\{d\_\{\\text\{in\}\}\}\]\}p\_\{i\}<\\ell\_\{i\}\\lor u\_\{i\}<p\_\{i\}\\right\)~\\land~\\nu\(\\mathbf\{p\},\\mathbf\{y\}\)~\\land~\\left\(\\bigwedge\_\{j\\neq c\}y\_\{c\}\-y\_\{j\}\>\\epsilon\\right\)\(5\)Above,ϵ\>0\\epsilon\>0is a precision constant\. The predicate𝒱I,ν\\mathscr\{V\}\_\{I,\\nu\}is satisfied only by adversarial examples, i\.e\., for inputs that belong to the current intervalIIand maximize a different score than the target classcc\. Symmetrically, the predicate𝒬I,ν\\mathscr\{Q\}\_\{I,\\nu\}is satisfied by acc\-instance not included in the current intervalII\. When there is no solution inIIfor𝒱I,ν\\mathscr\{V\}\_\{I,\\nu\}, we reached a robust certification\. Symmetrically, when there is no solution outside ofIIfor𝒬I,ν\\mathscr\{Q\}\_\{I,\\nu\}, we reached a dual certification\.

### 4\.2Refine & Check Algorithm

Input:We assume the following arguments:

∙\\bulletIo∈𝕀​\(d\)\|𝐱𝔽I\_\{o\}\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, an initial interval\.

∙\\bullet𝒫I,ν\\mathscr\{P\}\_\{I,\\nu\}, a property to be falsified\.

∙\\bullet□:𝕀​\(d\)\|𝐱𝔽×𝔽→𝕀​\(d\)\|𝐱𝔽\\square\\colon\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\\times\\mathbb\{F\}\\to\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, a refinement operator\.

Output:

II, an interval s\.t\.

⊧¬𝒫I,ν\\models\\lnot\\mathscr\{P\}\_\{I,\\nu\}
I←IoI\\leftarrow I\_\{o\}

while*∃𝐩\\exists\\mathbf\{p\}, s\.t\.𝐩⊧𝒫I,ν\\mathbf\{p\}\\models\\mathscr\{P\}\_\{I,\\nu\}*do

I←I​□​𝐩I\\leftarrow I~\\square~\\mathbf\{p\}
end while

return*II*

Algorithm 1RefineCheck\(Io,𝒫I,ν,□\)\(I\_\{o\},\\mathscr\{P\}\_\{I,\\nu\},\\square\)We now have all the components to develop our*refine & check*algorithm, whose pseudocode is given in Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)\. Starting from an initial intervalIoI\_\{o\}, the algorithm repeatedly checks whether the current intervalII*falsifies*some given property𝒫I,ν\\mathscr\{P\}\_\{I,\\nu\}\. The check is delegated to a NN verifier \(line[1](https://arxiv.org/html/2606.23858#algorithm1)\), which receives as input the MILP encoding of the network, the intervalII, and the property𝒫I,ν\\mathscr\{P\}\_\{I,\\nu\}\. If the property is not falsified, the verifier returns a*counterexample*𝐩\\mathbf\{p\}that satisfies the property\. The interval is then*refined*using𝐩\\mathbf\{p\}via some given operator□\\square, producing the intervalI​□​𝐩I~\\square~\\mathbf\{p\}\(line[1](https://arxiv.org/html/2606.23858#algorithm1)\)\. The procedure continues until the verifier asserts that𝒫I,ν\\mathscr\{P\}\_\{I,\\nu\}is falsified, in which case the current interval is returned\.

Different instantiations of Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)can be obtained by appropriately choosing its parameters\. Eq\. \([6](https://arxiv.org/html/2606.23858#S4.E6)\) shows how to compute the*apothem\-optimal robustness certification*\. In this setting, the initial interval is the whole domain𝔽\\mathbb\{F\}, the property to be falsified is given by eq\. \([4](https://arxiv.org/html/2606.23858#S4.E4)\), and the refinement operator is the constrain operator of Def\.[4](https://arxiv.org/html/2606.23858#Thmdefinition4)\. The correctness of eq\. \([6](https://arxiv.org/html/2606.23858#S4.E6)\) is given by Prop\.[3\.2](https://arxiv.org/html/2606.23858#Thmproofx2), which shows that the bottom operator can be realized as a sequence of constrain operations\. We call Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)instantiated in this manner asTop\-Down Search\(TDS\)\. Finally, since we begin from the domain𝔽\\mathbb\{F\}, TDS computes the intersection\(𝒱⊥𝐱\)∩𝔽\(\\mathscr\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}\.

\(𝒱⊥𝐱\)∩𝔽=RefineCheck​\(𝔽,𝒱I,ν,/\)\\displaystyle\(\\mathscr\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}=\\textsc\{RefineCheck\}\(\\mathbb\{F\},\\mathscr\{V\}\_\{I,\\nu\},/\)Top\-Down Search \(TDS\)\(6\)𝒬⊤𝐱=RefineCheck​\(\[𝐱,𝐱\],𝒬I,ν,⊔\)\\displaystyle\\mathscr\{Q\}\\top\\mathbf\{x\}=\\textsc\{RefineCheck\}\(\[\\mathbf\{x\},\\mathbf\{x\}\],\\mathscr\{Q\}\_\{I,\\nu\},\\sqcup\)Bottom\-Up Search \(BUS\)\(7\)
Eq\. \([7](https://arxiv.org/html/2606.23858#S4.E7)\) presents the implementation for*dual certifications*\. The construction proceeds symmetrically\. The interval is initialized to the trivial\[𝐱,𝐱\]\[\\mathbf\{x\},\\mathbf\{x\}\], the property to be falsified is given by eq\. \([5](https://arxiv.org/html/2606.23858#S4.E5)\), and the refinement operator is the join operator⊔\\sqcupof Def\.[2](https://arxiv.org/html/2606.23858#Thmdefinition2)\. The correctness of eq\. \([7](https://arxiv.org/html/2606.23858#S4.E7)\) follows from Prop\.[3\.3](https://arxiv.org/html/2606.23858#Thmproofx3), which shows that the top operator can be expressed as a sequence of join operations\. We refer to the parametrization in eq\. \([7](https://arxiv.org/html/2606.23858#S4.E7)\) asBottom\-Up Search\(BUS\)\.

Observe that the abstract sets𝒱\\mathcal\{V\}and𝒬\\mathcal\{Q\}introduced in Sec\.[3](https://arxiv.org/html/2606.23858#S3)have now been translated into the verification properties𝒱\\mathscr\{V\}and𝒬\\mathscr\{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 to construct the*on\-line*refine & check method of Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)\. In this setting the set𝒫\\mathcal\{P\}, that is𝒫∈\{𝒱,𝒬\}\\mathcal\{P\}\\in\\\{\\mathcal\{V\},\\mathcal\{Q\}\\\}, is constructed incrementally, and contains all the counterexamples𝐩\\mathbf\{p\}returned by the NN verifier during the execution of Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)\.

### 4\.3The 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𝒫\\mathcal\{P\}be the set of all counterexamples returned by the NN verifier, andn=\|𝒫\|n=\|\\mathcal\{P\}\|\. Moreover, lett𝒫I,νt\_\{\\mathscr\{P\}\_\{I,\\nu\}\}be the time consumed by the NN verifier \(in the worst case\) to test the satisfiability of the property𝒫I,ν\\mathscr\{P\}\_\{I,\\nu\}\. Finally, lett□t\_\{\\square\}be the execution time of the refinement operation□\\square\. Then, in each iteration, Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)processes one counterexample, makes a query to the NN verifier, and applies a refinement operator\.

\{restatable\}

theoremgenericcomplexity Letnnbe the number of counterexamples returned by the NN verifier\. Lett𝒫I,νt\_\{\\mathscr\{P\}\_\{I,\\nu\}\}be the worst\-case time to check whether property𝒫I,ν\\mathscr\{P\}\_\{I,\\nu\}holds\. Finally, lett□t\_\{\\square\}be the worst\-case time required by the operator□\\square\. Then, the refine & check method of Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)terminates afterO​\[n⋅\(t□\+t𝒫I,ν\)\]O\[n\\cdot\(t\_\{\\square\}\+t\_\{\\mathscr\{P\}\_\{I,\\nu\}\}\)\]steps\. If□∈\{/,⊔\}\\square\\in\\\{/,\\sqcup\\\}, thent□=O​\(d\)t\_\{\\square\}=O\(d\), and Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)concludes inO​\[n​d\+n​t𝒫I,ν\]O\[nd\+nt\_\{\\mathscr\{P\}\_\{I,\\nu\}\}\]time\. Although the numbernnof counterexamples is unknown, we can bound it from above using the precision constantδ\\delta\. The constrain operator only modifies one inequality of the given interval at each refinement step, and each inequality can be modified*at most*𝒜​\(𝔽\)/δ\\mathcal\{A\}\(\\mathbb\{F\}\)/\\deltatimes, where𝒜​\(𝔽\)\\mathcal\{A\}\(\\mathbb\{F\}\)is the domain’s diameter\. Since each interval is defined by2​d2dinequalities, the total number of counterexamples is bounded by2​d⋅𝒜​\(𝔽\)/δ2d\\cdot\\mathcal\{A\}\(\\mathbb\{F\}\)/\\delta\. The join operator⊔\\sqcupis more intervening, modifying all2​d2dinequalities at once, resulting in𝒜​\(𝔽\)/δ\\mathcal\{A\}\(\\mathbb\{F\}\)/\\deltacounterexamples\.

###### Corollary 1

Lett𝒫I,νt\_\{\\mathscr\{P\}\_\{I,\\nu\}\}be the worst case time for verifying property𝒫I,ν\\mathscr\{P\}\_\{I,\\nu\}\. TDS terminates afterO​\[\(𝒜​\(𝔽\)/δ\)​\(d2\+d⋅t𝒫I,ν\)\]O\[\(\\mathcal\{A\}\(\\mathbb\{F\}\)/\\delta\)\(d^\{2\}\+d\\cdot t\_\{\\mathscr\{P\}\_\{I,\\nu\}\}\)\]time\. BUS terminates afterO​\[\(𝒜​\(𝔽\)/δ\)​\(d\+t𝒫I,ν\)\]O\[\(\\mathcal\{A\}\(\\mathbb\{F\}\)/\\delta\)\(d\+t\_\{\\mathscr\{P\}\_\{I,\\nu\}\}\)\]time\.

### 4\.4The Intractability of Volume Optimality

From Thm\.[4\.3](https://arxiv.org/html/2606.23858#S4.SS3)we can compute an*apothem optimal*robustness certification inpoly​\(n,d,t𝒫I,ν\)\\textsf\{poly\}\(n,d,t\_\{\\mathscr\{P\}\_\{I,\\nu\}\}\)time\. Namely, even if NN verification can be computed in constant time, i\.e\.,t𝒫I,ν=O​\(1\)t\_\{\\mathscr\{P\}\_\{I,\\nu\}\}=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](https://arxiv.org/html/2606.23858#S3)\. There, we had a set𝒱⊂𝔽\\mathcal\{V\}\\subset\\mathbb\{F\}of adversarial examples and an input point𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}\. Our goal was to compute an intervalI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, s\.t\.𝐱∈I\\mathbf\{x\}\\in Iand𝒱∩I=∅\\mathcal\{V\}\\cap I=\\varnothing\. For a constantγ\>0\\gamma\>0, we want to decide if there isI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}with the above properties andv​\(I\)≥γv\(I\)\\geq\\gamma\. This problem is closely related to*Maximum Empty Rectangle \(MER\)*\[[24](https://arxiv.org/html/2606.23858#bib.bib24),[3](https://arxiv.org/html/2606.23858#bib.bib3),[1](https://arxiv.org/html/2606.23858#bib.bib1),[2](https://arxiv.org/html/2606.23858#bib.bib2)\]and*query\-Maximum Empty Square \(q\-MES\)*\[[8](https://arxiv.org/html/2606.23858#bib.bib8)\]problems\. Next, we establish an intractability result based on the proof of MER’s intractability by Backer and Keil in\[[1](https://arxiv.org/html/2606.23858#bib.bib1)\]\.

\{restatable\}

theoremsoundmaxhard Consider a set of adversarial examples𝒱⊂𝔽\\mathcal\{V\}\\subset\\mathbb\{F\}, an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, and a constantγ\>0\\gamma\>0\. Moreover, letn=\|𝒱\|n=\|\\mathcal\{V\}\|, letddbe the dimension s\.t\.𝔽⊂ℝd\\mathbb\{F\}\\subset\\mathbb\{R\}^\{d\}, and lett𝒫I,νt\_\{\\mathscr\{P\}\_\{I,\\nu\}\}be the worst\-case time check whether property𝒫I,ν\\mathscr\{P\}\_\{I,\\nu\}holds\. Then, the existence of a robustness certificationI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, with𝐱∈I\\mathbf\{x\}\\in I,I∩𝒱=∅I\\cap\\mathcal\{V\}=\\varnothingandv​\(I\)≥γv\(I\)\\geq\\gamma*cannot*be decided inpoly​\(n,d,t𝒫I,ν\)\\textsf\{poly\}\(n,d,t\_\{\\mathscr\{P\}\_\{I,\\nu\}\}\)time, unlessP=NP\\textbf\{P\}=\\textbf\{NP\}\.

###### Proof\(Sketch\)

We use the argument of\[[1](https://arxiv.org/html/2606.23858#bib.bib1)\]reducing from the independent set problem to maximum volume adversarial robustness\. In\[[1](https://arxiv.org/html/2606.23858#bib.bib1)\]each vertex of a given graph maps to a dimension, each edge maps to a point\. The graph has an independent set of sizekkiff there is a sufficiently large empty interval\.

Thus, given a graphGG, we use the methodology in\[[1](https://arxiv.org/html/2606.23858#bib.bib1)\]to construct a set of adversarial examples𝒱\\mathcal\{V\}\. However, we also need to define an input𝐱\\mathbf\{x\}that must be included to the interval\. We set𝐱=𝟎\\mathbf\{x\}=\\mathbf\{0\}\. From Lemma 2 in\[[1](https://arxiv.org/html/2606.23858#bib.bib1)\]the origin will always be included in a maximum volume interval\. Thus, our choice of𝐱\\mathbf\{x\}does not effect the validity of the argument\. This concludes the reduction\.■\\hfill\\blacksquare

### 4\.5Notes on Uniform Certifications

We close this section with some notes on uniform robustness certifications \(originally used in\[[30](https://arxiv.org/html/2606.23858#bib.bib30)\]\), i\.e\., certifications of the formI=\[𝐱−ρ​𝟏,𝐱\+ρ​𝟏\]I=\[\\mathbf\{x\}\-\\rho\\mathbf\{1\},\\mathbf\{x\}\+\\rho\\mathbf\{1\}\]forρ\>0\\rho\>0and some input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}\. In our setting, we can use binary search to determine the maximum radius excluding the adversarial examples in𝒱\\mathcal\{V\}, or the minimum radius including the positive examples𝒬\\mathcal\{Q\}\. The top and bottom operators of Sec\.[3](https://arxiv.org/html/2606.23858#S3),*when restricted to uniform certifications*, are denoted by⊤𝔹\\top\_\{\\mathbb\{B\}\}and⊥𝔹\\bot\_\{\\mathbb\{B\}\}respectively, while the corresponding algorithms𝔹\\mathbb\{B\}\-BUS and𝔹\\mathbb\{B\}\-TDS\. These operators can be computed in logarithmiclog⁡\(𝒜​\(𝔽\)/δ\)\\log\(\\mathcal\{A\}\(\\mathbb\{F\}\)/\\delta\)oracle calls\. We use uniform certifications as a*baseline*in our following experimentation\.

## 5Implementation

In this section, we review theParallelepipedoNNsystem, where we implement the algorithms and operations discussed earlier\. In particular, we present two case studies based on the MNIST\[[17](https://arxiv.org/html/2606.23858#bib.bib17)\]and the Fashion MNIST\[[33](https://arxiv.org/html/2606.23858#bib.bib33)\]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](https://arxiv.org/html/2606.23858#S4.E6)\) and its*uniform variant*𝔹\\mathbb\{B\}\-TDS \(see Subsec\.[4\.5](https://arxiv.org/html/2606.23858#S4.SS5)\)\. For dual certifications, we use the BUS algorithm of eq\. \([7](https://arxiv.org/html/2606.23858#S4.E7)\) and its*uniform variant*𝔹\\mathbb\{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\.ParallelepipedoNNis written in Python v3\.8\.16\. We used the Marabou v2\.0\[[15](https://arxiv.org/html/2606.23858#bib.bib15),[31](https://arxiv.org/html/2606.23858#bib.bib31)\]NN verifier\. Our implementation takes as input a NN in open neural network exchange \(ONNX\) v1\.16\.0888See[https://github\.com/onnx/onnx](https://github.com/onnx/onnx)\.format\. For linear 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δ\\deltatoδ=0\.1\\delta=0\.1, and a*timeout*to 1 hour\. We use 2 datasets, namely MNIST\[[17](https://arxiv.org/html/2606.23858#bib.bib17)\]and Fashion MNIST\[[33](https://arxiv.org/html/2606.23858#bib.bib33)\]\. Both datasets consist of 28×\\times28 grayscale images, belonging to 10 classes\. The NN architecture isD=⟨784,32,10,10⟩D=\\langle 784,32,10,10\\rangle, w\.r\.t\. Def\.[8](https://arxiv.org/html/2606.23858#Thmdefinition8)\. The last layer is fully connected, without activation function\. This corresponds to 25,450 trainable parameters\. For training, we used the Adam\[[16](https://arxiv.org/html/2606.23858#bib.bib16)\]algorithm, Glorot\[[6](https://arxiv.org/html/2606.23858#bib.bib6)\]weight initialization, and the Categorical Crossentropy loss\. The achieved test\-set accuracy is94%94\\%and82%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\)\.

![Refer to caption](https://arxiv.org/html/2606.23858v1/figures/experiments/evolution-best-v4-nt-low-res.png)Figure 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\.
#### 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𝒱⊥𝐱\\mathscr\{V\}\\bot\\mathbf\{x\}, and most measures, trivially unbounded\. Therefore, for all measures,*except the apothem*, we use the intersection\(𝒱⊥𝐱\)∩𝔽\(\\mathscr\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}\. The apothem is computed in the \(possibly unbounded\) bottom interval𝒱⊥𝐱\\mathscr\{V\}\\bot\\mathbf\{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](https://arxiv.org/html/2606.23858#S5.F4)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 theii\-th robustness and dual certifications\. In this case, the two apothems happen to converge at 0\.1 distance\.

DataAlg\.Timesec\./min\.Verif\.Perc\.\# Verif\.CallsApoth\.ϖ\\varpiMin\.Edgeα\\alphaAvg\.EdgeE¯\\overline\{E\}Diam\.𝒜\\mathcal\{A\}Perim\.π\\piMNISTTDS56\.93m99%691\.30\.140\.150\.531\.0415\.55𝔹\\mathbb\{B\}–TDS20\.16s98%9\.980\.040\.040\.050\.0835\.76BUS16\.13m96%895\.731\.00\.861\.01\.0781\.4𝔹\\mathbb\{B\}–BUS1\.9s95%4\.00\.810\.810\.831\.0650\.92FashionMNISTTDS9\.19m95%700\.880\.010\.070\.661\.0516\.85𝔹\\mathbb\{B\}–TDS5\.66s94%9\.620\.10\.10\.140\.19108\.05BUS13\.55m96%757\.361\.00\.91\.01\.0783\.75𝔹\\mathbb\{B\}–BUS2\.7s96%4\.00\.810\.810\.891\.0697\.81

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

In Tbl\.[1](https://arxiv.org/html/2606.23858#S5.T1)we present results on the CPU time, the percentage of time spent in oracle calls, the number of oracle calls, the apothemϖ\\varpi, the minimum edge lengthα\\alpha, the average edge lengthE¯=π​\(I\)/d\\overline\{E\}=\\pi\(I\)/d, the diameter𝒜\\mathcal\{A\}, and the perimeterπ\\pi\. In Tbl\.[1](https://arxiv.org/html/2606.23858#S5.T1), for each problem we denote with bold the best value\. For robustness certifications we observe a tradeoff between quality and performance\. The uniform algorithm𝔹\\mathbb\{B\}\-TDS performs much faster than its arbitrary counterpart\. This is expected by the discussion in Subsection[4\.5](https://arxiv.org/html/2606.23858#S4.SS5)\. However, TDS achieves 3 times better quality, on average, as reported byα\\alpha\(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](https://arxiv.org/html/2606.23858#bib.bib20)\]train 3 networks for MNIST, with 3 hidden layers and architectures⟨3×100⟩=⟨100,100,100⟩,⟨3×300⟩\\langle 3\\times 100\\rangle=\\langle 100,100,100\\rangle,\\langle 3\\times 300\\rangleand⟨3×500⟩\\langle 3\\times 500\\rangle\. In each case, they report minimum edge length ofα≃0\.06\\alpha\\simeq 0\.06, for uniform certifications, andα≃0\.07\\alpha\\simeq 0\.07, for symmetric certifications\. For Fashion MNIST, they use a network with architecture⟨3×1024⟩\\langle 3\\times 1024\\rangle\. They reportα≃0\.026\\alpha\\simeq 0\.026, for uniform andα≃0\.028\\alpha\\simeq 0\.028, for symmetric certifications\. The implementation, and the NN architectures of Li et al\.\[[18](https://arxiv.org/html/2606.23858#bib.bib18)\]are not publicly available\. They train 3 NNs for MNIST \(MNIST100, MNIST300, MNIST500\), and one NN for Fashion MNIST \(FMNIST100\)\. They reportα\\alphaof0\.0580\.058,0\.0410\.041,0\.0450\.045, and0\.0720\.072, for MNIST100, MNIST300, MNIST500, and FMNIST100, respectively\. Finally, Kabahala and Drachsler\-Cohen\[[12](https://arxiv.org/html/2606.23858#bib.bib12)\]report average edge lengthE¯\\overline\{E\}of0\.1960\.196and0\.10\.1for two MNIST NNs \(⟨3×50⟩\\langle 3\\times 50\\rangle,⟨3×100⟩\\langle 3\\times 100\\rangle\), whereas for two Fashion MNIST NNs \(⟨3×50⟩\\langle 3\\times 50\\rangle,⟨3×250⟩\\langle 3\\times 250\\rangle\) they reportE¯\\overline\{E\}of0\.1910\.191and0\.0370\.037\.

## 6Related Work

Interval arithmetic\[[27](https://arxiv.org/html/2606.23858#bib.bib27),[23](https://arxiv.org/html/2606.23858#bib.bib23)\]has been used in NN adversarial analysis \(e\.g\.\[[30](https://arxiv.org/html/2606.23858#bib.bib30),[14](https://arxiv.org/html/2606.23858#bib.bib14),[34](https://arxiv.org/html/2606.23858#bib.bib34)\]\)\. However, they do not make explicit use of the underlying lattice structure\[[27](https://arxiv.org/html/2606.23858#bib.bib27)\]\.

Adversarial robustness is the problem of*deciding*whether an area is free of adversarial examples\. Several approaches exist\[[22](https://arxiv.org/html/2606.23858#bib.bib22)\], such as abstraction \(e\.g\.\[[26](https://arxiv.org/html/2606.23858#bib.bib26)\]\), satisfiability modulo theories \(SMT\) \(e\.g\.\[[13](https://arxiv.org/html/2606.23858#bib.bib13),[14](https://arxiv.org/html/2606.23858#bib.bib14)\]\), and MILP \(e\.g\.\[[15](https://arxiv.org/html/2606.23858#bib.bib15),[31](https://arxiv.org/html/2606.23858#bib.bib31)\]\)\.

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](https://arxiv.org/html/2606.23858#bib.bib30)\], or by the augmented Langrage method\[[20](https://arxiv.org/html/2606.23858#bib.bib20),[18](https://arxiv.org/html/2606.23858#bib.bib18)\]\. These methods are scalable and can be applied to large NNs, but suffer from approximation errors\[[25](https://arxiv.org/html/2606.23858#bib.bib25)\]and lack optimality guarantees\. More recent work\[[12](https://arxiv.org/html/2606.23858#bib.bib12)\]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 lengthE¯\\overline\{E\}, but optimality is not proved\. Similar oracle\-based iterative schemes have been applied in formal AI\-explainability\[[9](https://arxiv.org/html/2606.23858#bib.bib9),[32](https://arxiv.org/html/2606.23858#bib.bib32),[10](https://arxiv.org/html/2606.23858#bib.bib10),[11](https://arxiv.org/html/2606.23858#bib.bib11)\], where an explanation can be interpreted as a special form of interval\[[11](https://arxiv.org/html/2606.23858#bib.bib11)\]\.

Existing work on robustness certification mostly focuses on optimizing the volume\[[30](https://arxiv.org/html/2606.23858#bib.bib30),[20](https://arxiv.org/html/2606.23858#bib.bib20),[18](https://arxiv.org/html/2606.23858#bib.bib18)\], through optimizing minimum edge length\. Deciding on the adversarial robustness of a*uniform*area isNP\-hard\[[13](https://arxiv.org/html/2606.23858#bib.bib13)\], and even approximating the optimalα\\alphais intractable for uniform certifications\[[29](https://arxiv.org/html/2606.23858#bib.bib29)\]\. However, volume optimality stays intractable even if the oracle costs are discarded\.

## 7Conclusions

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 theParallelepipedoNNsystem, 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\.

## 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\)
- \[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\)

## Appendix 0\.AOmitted proofs

### 0\.A\.1Proofs of Section[2](https://arxiv.org/html/2606.23858#S2)

###### Proof

Applying straightforward computations we take,

𝒜​\(I\)\\displaystyle\\mathcal\{A\}\(I\)=‖ui−ℓi‖∞=1d​∑i∈\[d\]maxi∈\[d\]⁡\{ui−ℓi\}\\displaystyle=\\\|u\_\{i\}\-\\ell\_\{i\}\\\|\_\{\\infty\}=\\frac\{1\}\{d\}\\sum\_\{i\\in\[d\]\}\\max\_\{i\\in\[d\]\}\\\{u\_\{i\}\-\\ell\_\{i\}\\\}≥1d​∑i∈\[d\]ui−ℓi\\displaystyle\\geq\\frac\{1\}\{d\}\\sum\_\{i\\in\[d\]\}u\_\{i\}\-\\ell\_\{i\}\[equals​1d​π​\(I\)\]\\displaystyle\\left\[\\text\{ equals \}\\frac\{1\}\{d\}\\pi\(I\)\\right\]≥∏i∈\[d\]ui−ℓid\\displaystyle\\geq\\sqrt\[d\]\{\\prod\_\{i\\in\[d\]\}u\_\{i\}\-\\ell\_\{i\}\}\[by arithmetic\-geometricmean inequality\. Equals​v​\(I\)d\]\\displaystyle\\left\[\\begin\{array\}\[\]\{l\}\\text\{by arithmetic\-geometric\}\\\\ \\text\{mean inequality\. Equals \}\\sqrt\[d\]\{v\(I\)\}\\end\{array\}\\right\]≥\[mini∈\[d\]⁡\{ui−ℓi\}\]dd\\displaystyle\\geq\\sqrt\[d\]\{\\left\[\\min\_\{i\\in\[d\]\}\\\{u\_\{i\}\-\\ell\_\{i\}\\\}\\right\]^\{d\}\}\[equalsα\(I\)\)\]\\displaystyle\\left\[\\text\{ equals \}\\alpha\(I\)\)\\right\]=\[mini∈\[d\]⁡\(ui−xi\+xi−ℓi\)\]dd\\displaystyle=\\sqrt\[d\]\{\\left\[\\min\_\{i\\in\[d\]\}\(u\_\{i\}\-x\_\{i\}\+x\_\{i\}\-\\ell\_\{i\}\)\\right\]^\{d\}\}≥min\{mini∈\[d\]\(ui−xi\),minj∈\[d\]\(xj−ℓj\)\}dd\\displaystyle\\geq\\sqrt\[d\]\{\\min\\left\\\{\\min\_\{i\\in\[d\]\}\(u\_\{i\}\-x\_\{i\}\),\\min\_\{j\\in\[d\]\}\(x\_\{j\}\-\\ell\_\{j\}\)\\right\\\}^\{d\}\}\[due to non\-negativity\.Equals​ϖ​\(I\)\]\\displaystyle\\left\[\\begin\{array\}\[\]\{l\}\\text\{due to non\-negativity\.\}\\\\ \\text\{Equals \}\\varpi\(I\)\\end\{array\}\\right\]■\\blacksquare

### 0\.A\.2Proofs of Section[3](https://arxiv.org/html/2606.23858#S3)

In some of the proofs below, we assume w\.l\.o\.g\. that the input point is the origin, i\.e\.,𝐱=𝟎\\mathbf\{x\}=\\mathbf\{0\}\. If𝐱≠𝟎\\mathbf\{x\}\\neq\\mathbf\{0\}, the same arguments apply after translating the space by−𝐱\-\\mathbf\{x\}, by working in𝔽−𝐱\\mathbb\{F\}\-\\mathbf\{x\}\.

###### Proof

W\.l\.o\.g\. we assume𝐱=𝟎\\mathbf\{x\}=\\mathbf\{0\}\. LetIjI\_\{j\}be the sequence of intervals produced by Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1), under property𝒱I,ν​\(⋅\)\\mathscr\{V\}\_\{I,\\nu\}\(\\cdot\)and operator//\. It holds the following,

Ij\+1=Ij/𝐯j\+1,if​∃𝐯j\+1∈Ij∖𝒱Ij\+1=Ij,otherwise\}\.\\left\.\\begin\{array\}\[\]\{l l l\}I\_\{j\+1\}&=I\_\{j\}/\\mathbf\{v\}\_\{j\+1\},&\\text\{ if \}~\\exists\\;\\mathbf\{v\}\_\{j\+1\}\\in I\_\{j\}\\setminus\\mathcal\{V\}\\\\ I\_\{j\+1\}&=I\_\{j\},&\\text\{ otherwise \}\\end\{array\}\\right\\\}\.\(8\)From eq\. \([8](https://arxiv.org/html/2606.23858#Pt0.A1.E8)\),Ij\+1⊆IiI\_\{j\+1\}\\subseteq I\_\{i\}, forj=0,…,n−1j=0,\\ldots,n\-1, and finallyI=InI=I\_\{n\}\.

Now for a point𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}assume that𝐱∈Ij\\mathbf\{x\}\\in I\_\{j\}for somejj\. If no constraint is applied,Ij\+1=IjI\_\{j\+1\}=I\_\{j\}, so𝐱∈Ij\+1\\mathbf\{x\}\\in I\_\{j\+1\}\. Otherwise,Ij\+1=Ij/𝐯j\+1I\_\{j\+1\}=I\_\{j\}/\\mathbf\{v\}\_\{j\+1\}\. By Def\.[6](https://arxiv.org/html/2606.23858#Thmdefinition6)𝐱∈Ij/𝐯j\+1\\mathbf\{x\}\\in I\_\{j\}/\\mathbf\{v\}\_\{j\+1\}, so𝐱∈Ij\+1\\mathbf\{x\}\\in I\_\{j\+1\}\. Hence, it holds𝐱∈In=I\\mathbf\{x\}\\in I\_\{n\}=I\.

Again from eq\. \([8](https://arxiv.org/html/2606.23858#Pt0.A1.E8)\), since the constrain operator only removes points,Ij\+1⊆IjI\_\{j\+1\}\\subseteq I\_\{j\}\. Therefore, for alli≤ji\\leq j,vi∉Ijv\_\{i\}\\not\\in I\_\{j\}, impliesvi∉Ij\+1v\_\{i\}\\not\\in I\_\{j\+1\}\. By induction to the number of adversarial points in𝒱\\mathcal\{V\}we takev∉Iv\\not\\in I, for allv∈𝒱v\\in\\mathcal\{V\}, henceI∩𝒱=∅I\\cap\\mathcal\{V\}=\\emptyset\.

From Def\.[6](https://arxiv.org/html/2606.23858#Thmdefinition6), for every coordinateii,−r¯i<vi−xi<r¯i\-\\underline\{r\}\_\{i\}<v\_\{i\}\-x\_\{i\}<\\overline\{r\}\_\{i\}for every𝐯∈𝒱\\mathbf\{v\}\\in\\mathcal\{V\}\. Hence no adversarial example lies inside the interval s\.t\.\(𝐱\+\[−𝐫¯,𝐫¯\]\)∪𝒱=∅\(\\mathbf\{x\}\+\[\-\\underline\{\\mathbf\{r\}\},\\overline\{\\mathbf\{r\}\}\]\)\\cup\\mathcal\{V\}=\\emptyset\. Now consider the construction ofIIfrom eq\. \([8](https://arxiv.org/html/2606.23858#Pt0.A1.E8)\) and assume that at some stepjjit holds𝒱⊥𝐱⊆Ij\\mathcal\{V\}\\bot\\mathbf\{x\}\\subseteq I\_\{j\}\. Applying the next constraint and we takeIj\+1=Ij/𝐯j\+1I\_\{j\+1\}=I\_\{j\}/\\mathbf\{v\}\_\{j\+1\}\.

Letk=arg​maxi⁡\|vj\+1,i−xi\|k=\\text\{arg\}\\max\_\{i\}\|v\_\{j\+1,i\}\-x\_\{i\}\|\. Ifvj\+1,i\>xiv\_\{j\+1,i\}\>x\_\{i\}, the new upper bound becomesuk′=max⁡\{0,vj\+1,i−xi−δ\}u^\{\\prime\}\_\{k\}=\\max\\\{0,v\_\{j\+1,i\}\-x\_\{i\}\-\\delta\\\}and by definition ofr¯k\\overline\{r\}\_\{k\}we have,r¯k≤vj\+1,i−xi−δ\\overline\{r\}\_\{k\}\\leq v\_\{j\+1,i\}\-x\_\{i\}\-\\delta\. Therefore,xk\+r¯k≤xk\+uk′x\_\{k\}\+\\overline\{r\}\_\{k\}\\leq x\_\{k\}\+u^\{\\prime\}\_\{k\}\. Since all other coordinates remain unchanged we take𝒱⊥𝐱⊆Ij\+1\\mathcal\{V\}\\bot\\mathbf\{x\}\\subseteq I\_\{j\+1\}\. By induction over all adversarial examples,𝒱⊥𝐱⊆I\\mathcal\{V\}\\bot\\mathbf\{x\}\\subseteq I\. Ifvj\+1,i<xiv\_\{j\+1,i\}<x\_\{i\}the new lower bound becomeslk′=min⁡\{0,vj\+1,i−xi\+δ\}l^\{\\prime\}\_\{k\}=\\min\\\{0,v\_\{j\+1,i\}\-x\_\{i\}\+\\delta\\\}\. We work analogously as in the previous case and we conclude that𝒱⊥𝐱⊆Ij\+1\\mathcal\{V\}\\bot\\mathbf\{x\}\\subseteq I\_\{j\+1\}\.■\\blacksquare

###### Proof

The first desideratum results immediately from Def\.[7](https://arxiv.org/html/2606.23858#Thmdefinition7)\.

For the second desideratum, we will prove that ifJ⊂\(𝒬⊤𝐱\)J\\subset\(\\mathcal\{Q\}\\top\\mathbf\{x\}\), then there is some𝐪∈Q\\mathbf\{q\}\\in Q, s\.t\.𝐪∉J\\mathbf\{q\}\\notin J\. Let𝒬⊤𝐱=𝐱\+\[−𝐫¯,𝐫¯\]\\mathcal\{Q\}\\top\\mathbf\{x\}=\\mathbf\{x\}\+\[\-\\underline\{\\mathbf\{r\}\},\\overline\{\\mathbf\{r\}\}\], with𝐫¯,𝐫¯≥𝟎\\underline\{\\mathbf\{r\}\},\\overline\{\\mathbf\{r\}\}\\geq\\mathbf\{0\}as in Def\.[7](https://arxiv.org/html/2606.23858#Thmdefinition7)\. Consider thekk\-th coordinate of the upper endpointri¯\\overline\{r\_\{i\}\}\. From Def\.[7](https://arxiv.org/html/2606.23858#Thmdefinition7)there is some𝐪∈𝒬\\mathbf\{q\}\\in\\mathcal\{Q\}, s\.t\.qk=rk¯q\_\{k\}=\\overline\{r\_\{k\}\}\. Since,𝐱∈J\\mathbf\{x\}\\in J, we writeJ=𝐱\+\[−𝐝¯,𝐝¯\]J=\\mathbf\{x\}\+\[\-\\underline\{\\mathbf\{d\}\},\\overline\{\\mathbf\{d\}\}\], with𝐝¯,𝐝¯≥𝟎\\underline\{\\mathbf\{d\}\},\\overline\{\\mathbf\{d\}\}\\geq\\mathbf\{0\}\. Since,J⊂\(𝒬⊤𝐱\)J\\subset\(\\mathcal\{Q\}\\top\\mathbf\{x\}\), then\[−𝐝¯,𝐝¯\]⊂\[−𝐫¯,𝐫¯\]\[\-\\underline\{\\mathbf\{d\}\},\\overline\{\\mathbf\{d\}\}\]\\subset\[\-\\underline\{\\mathbf\{r\}\},\\overline\{\\mathbf\{r\}\}\]\. Thus, there is a coordinate of the upper of lower endpoint ofJJ, that is dominated by the respective coordinate of𝒬⊤𝐱\\mathcal\{Q\}\\top\\mathbf\{x\}\. W\.l\.o\.g\. letdk¯<rk¯=qk\\overline\{d\_\{k\}\}<\\overline\{r\_\{k\}\}=q\_\{k\}, thusdk¯<qk\\overline\{d\_\{k\}\}<q\_\{k\}, and𝐪∉J\\mathbf\{q\}\\notin J\. A contradiction\.

For the third desideratum, we work as follows\. LetI,JI,Jbe minimal intervals that include𝒬∪𝐱\\mathcal\{Q\}\\cup\\mathbf\{x\}\. Then,I∩J=I⊓J∈𝕀​\(d\)\|𝐱𝔽I\\cap J=I\\sqcap J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\. Moreover,𝒬⊆I∩J\\mathcal\{Q\}\\subseteq I\\cap J\. Thus, the intersectionI∩JI\\cap Jsatisfies the above properties, and is included in bothI,JI,J\. A contradiction, since we assumed thatI,JI,Jare minimal\.

The fourth desideratum follows from the previous\. From*2*we established that𝒬⊤𝐱\\mathcal\{Q\}\\top\\mathbf\{x\}is minimal\. From*3*we establish that the minimal is unique\. Finally, the apothem is increasing w\.r\.t\. set inclusion\. Thus,𝒬⊤𝐱\\mathcal\{Q\}\\top\\mathbf\{x\}is minimum\.■\\blacksquare

###### Proof

W\.l\.o\.g\., we assume𝐱=𝟎\\mathbf\{x\}=\\mathbf\{0\}\. First we show that Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1), under property𝒬I,ν​\(⋅\)\\mathscr\{Q\}\_\{I,\\nu\}\(\\cdot\)and operator⊔\\sqcup, terminates after a finite number of steps\. To that end, letIj=\[−ℓj,𝒖j\]I\_\{j\}=\[\-\\boldsymbol\{\\ell\}^\{j\},\\boldsymbol\{u\}^\{j\}\], withℓj,𝒖j≥𝟎\\boldsymbol\{\\ell\}^\{j\},\\boldsymbol\{u\}^\{j\}\\geq\\mathbf\{0\},j∈ℕj\\in\\mathbb\{N\}, be the interval in thejj\-th iteration\. For the sequence of intervals holds,

Ij\+1=Ij⊔\[𝐪j\+1−δ​𝟏,𝐪j\+1\+δ​𝟏\],if​∃𝐪j\+1∈𝔽∖IjIj\+1=Ij,otherwise\}\\left\.\\begin\{array\}\[\]\{l l l\}I\_\{j\+1\}&=I\_\{j\}\\sqcup\[\\mathbf\{q\}\_\{j\+1\}\-\\delta\\mathbf\{1\},\\mathbf\{q\}\_\{j\+1\}\+\\delta\\mathbf\{1\}\],&\\text\{ if \}~\\exists\\;\\mathbf\{q\}\_\{j\+1\}\\in\\mathbb\{F\}\\setminus I\_\{j\}\\\\ I\_\{j\+1\}&=I\_\{j\},&\\text\{ otherwise \}\\end\{array\}\\right\\\}\(9\)From eq\. \([9](https://arxiv.org/html/2606.23858#Pt0.A1.E9)\)Ij⊆Ij\+1I\_\{j\}\\subseteq I\_\{j\+1\}, forj=0,…,n−1j=0,\\ldots,n\-1, and finallyI=InI=I\_\{n\}\.

Therefore,I0=𝐱I\_\{0\}=\\mathbf\{x\}andIj=𝐱\+\[−𝐚j,𝐛j\]I\_\{j\}=\\mathbf\{x\}\+\[\-\\mathbf\{a\}^\{j\},\\mathbf\{b\}^\{j\}\], with𝐚j,𝐛j≥0\\mathbf\{a\}^\{j\},\\mathbf\{b\}^\{j\}\\geq 0and𝐚0,𝐛0=𝟎\\mathbf\{a\}^\{0\},\\mathbf\{b\}^\{0\}=\\mathbf\{0\}\. For the positive point𝐪k\+1\\mathbf\{q\}\_\{k\+1\}, the minimum interval update providesaij\+1=max⁡\{aij,xi−qj\+1,i\}a\_\{i\}^\{j\+1\}=\\max\\\{a\_\{i\}^\{j\},x\_\{i\}\-q\_\{j\+1,i\}\\\}, andbij\+1=max⁡\{bij,qj\+1,i−xi\}b\_\{i\}^\{j\+1\}=\\max\\\{b\_\{i\}^\{j\},q\_\{j\+1,i\}\-x\_\{i\}\\\}\. After processing all points in𝒬\\mathcal\{Q\}we take,ain=maxj⁡\{xi−qj,i∣𝐪j∈𝒬\}a^\{n\}\_\{i\}=\\max\_\{j\}\\\{x\_\{i\}\-q\_\{j,i\}\\mid\\mathbf\{q\}\_\{j\}\\in\\mathcal\{Q\}\\\}andbin=maxj⁡\{qj\+1,i−xi∣𝐪j∈𝒬\}b^\{n\}\_\{i\}=\\max\_\{j\}\\\{q\_\{j\+1,i\}\-x\_\{i\}\\mid\\mathbf\{q\}\_\{j\}\\in\\mathcal\{Q\}\\\}\. So, we have,In=𝐱\+\[−𝐚n,𝐛n\]I\_\{n\}=\\mathbf\{x\}\+\[\-\\mathbf\{a\}^\{n\},\\mathbf\{b\}^\{n\}\]\. By Def\.[7](https://arxiv.org/html/2606.23858#Thmdefinition7),Ri¯=sup\{xi−qi∣𝐪∈𝒬\}\\underline\{R\_\{i\}\}=\\sup\\\{x\_\{i\}\-q\_\{i\}\\mid\\mathbf\{q\}\\in\\mathcal\{Q\}\\\}andRi¯=sup\{qi−xi∣𝐪∈𝒬\}\\overline\{R\_\{i\}\}=\\sup\\\{q\_\{i\}\-x\_\{i\}\\mid\\mathbf\{q\}\\in\\mathcal\{Q\}\\\}\. Since𝒬\\mathcal\{Q\}is finite, we takeRi¯=max⁡\{xi−qi∣𝐪∈𝒬\}=maxj⁡\{xi−qj,i\}=ain\\underline\{R\_\{i\}\}=\\max\\\{x\_\{i\}\-q\_\{i\}\\mid\\mathbf\{q\}\\in\\mathcal\{Q\}\\\}=\\max\_\{j\}\\\{x\_\{i\}\-q\_\{j,i\}\\\}=a\_\{i\}^\{n\}andRi¯=maxj⁡\{qj,i−xi∣𝐪∈𝒬\}=bin\\overline\{R\_\{i\}\}=\\max\_\{j\}\\\{q\_\{j,i\}\-x\_\{i\}\\mid\\mathbf\{q\}\\in\\mathcal\{Q\}\\\}=b\_\{i\}^\{n\}\. Hence,In=𝐱\+\[−𝐑¯,𝐑¯\]=𝒬⊤𝐱I\_\{n\}=\\mathbf\{x\}\+\[\-\\underline\{\\mathbf\{R\}\},\\overline\{\\mathbf\{R\}\}\]=\\mathcal\{Q\}\\top\\mathbf\{x\}\.■\\blacksquare

###### Proof

From*1\.*in Thm\.[3\.1](https://arxiv.org/html/2606.23858#S3.Thmtheorem1)we have\(𝒱⊥𝐱\)∩𝒱=∅\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathcal\{V\}=\\emptyset\. Since𝒬∩𝒱=∅\\mathcal\{Q\}\\cap\\mathcal\{V\}=\\emptyset, it holds either𝒬⊂\(𝒱⊥𝐱\)∩𝔽\\mathcal\{Q\}\\subset\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}or\(𝒱⊥𝐱\)∩𝔽⊆𝒬\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}\\subseteq\\mathcal\{Q\}\. If the first inclusion holds, then there exists some𝐱′∈\(𝒱⊥𝐱\)∩𝔽\\mathbf\{x\}^\{\\prime\}\\in\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}s\.t\.𝐱′∉𝒬\\mathbf\{x\}^\{\\prime\}\\not\\in\\mathcal\{Q\}and𝐱′∉𝒱\\mathbf\{x\}^\{\\prime\}\\not\\in\\mathcal\{V\}\. This, in turn, yields𝒬∪𝒱⊂𝔽\\mathcal\{Q\}\\cup\\mathcal\{V\}\\subset\\mathbb\{F\}, a contradiction\. Therefore, it holds\(𝒱⊥𝐱\)⊆𝒬\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\subseteq\\mathcal\{Q\}\. Now, from*1\.*in Thm\.[7](https://arxiv.org/html/2606.23858#Thmdefinition7)we have that\(𝒬⊤𝐱\)∪𝒬=\(𝒬⊤𝐱\)\(\\mathcal\{Q\}\\top\\mathbf\{x\}\)\\cup\\mathcal\{Q\}=\(\\mathcal\{Q\}\\top\\mathbf\{x\}\), meaning that𝒬⊆\(𝒬⊤𝐱\)\\mathcal\{Q\}\\subseteq\(\\mathcal\{Q\}\\top\\mathbf\{x\}\)\. Combining all together we take\(𝒱⊥𝐱\)∩𝔽⊆𝒬⊤𝐱\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}\\subseteq\\mathcal\{Q\}\\top\\mathbf\{x\}\. Finally, sinceμ\\muis an increasing measure the inequalityμ​\[\(𝒱⊥𝐱\)∩𝔽\]≤μ​\[𝒬⊤𝐱\]\\mu\[\(\\mathcal\{V\}\\bot\\mathbf\{x\}\)\\cap\\mathbb\{F\}\]\\leq\\mu\[\\mathcal\{Q\}\\top\\mathbf\{x\}\]follows\.■\\blacksquare

### 0\.A\.3Proofs of Section[4](https://arxiv.org/html/2606.23858#S4)

###### Proof

From lines 2\-3 in Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1), that updates the intervalII, we have complexityO​\(t□\+t𝒫I,ν\)O\(t\_\{\\square\}\+t\_\{\\mathscr\{P\}\_\{I,\\nu\}\}\)\. Then Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)is linear to the number of oracle calls, therefore, isO​\(n\)O\(n\)\. Hence the total time complexity becomesO​\(n⋅\(t□\+t𝒫I,ν\)\)O\(n\\cdot\(t\_\{\\square\}\+t\_\{\\mathscr\{P\}\_\{I,\\nu\}\}\)\)\.

Now, consider the potential functionΦ:𝕀​\(d\)\|𝟎𝔽→ℝ≥0\\Phi\\colon\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{0\}\}\\to\\mathbb\{R\}\_\{\\geq 0\}s\.t\.,

Φ​\(\[−ℓ,𝒖\]\)=∑i∈\[d\]ℓi\+ui,for​ℓ,𝒖≥𝟎\.\\Phi\(\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\)=\\sum\_\{i\\in\[d\]\}\\ell\_\{i\}\+u\_\{i\},\\quad\\text\{ for \}\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\\geq\\mathbf\{0\}\.\(10\)For□=⊔\\square=\\sqcup, we haveI0=\[𝟎,𝟎\]I\_\{0\}=\[\\mathbf\{0\},\\mathbf\{0\}\], andΦ​\(I0\)=0\\Phi\(I\_\{0\}\)=0\. For everyj∈\[d\]j\\in\[d\], the potential is upper\-bounded, as proved in Prop\.[3\.3](https://arxiv.org/html/2606.23858#Thmproofx3)as well, i\.e\.,Φ​\(Ij\)≤Φ​\(𝔽\)\\Phi\(I\_\{j\}\)\\leq\\Phi\(\\mathbb\{F\}\)\. Moreover, for every interval properly included in𝔽\\mathbb\{F\}, the potential function is increasing withΦ​\(Ij\+1\)≤Φ​\(Ij\)\+δ\\Phi\(I\_\{j\+1\}\)\\leq\\Phi\(I\_\{j\}\)\+\\deltafor someδ\>0\\delta\>0\. Since the potential increases by at leastδ\\deltaat each iteration while remaining bounded, the sequence generated from eq\. \([10](https://arxiv.org/html/2606.23858#Pt0.A1.E10)\) must converge\. Thus, there exists an indexk∈ℕk\\in\\mathbb\{N\}, s\.t\.Ik=Ik\+1I\_\{k\}=I\_\{k\+1\}, and the algorithm terminates after a finite number of steps, sot⊔=O​\(d\)t\_\{\\sqcup\}=O\(d\)\.

For□=/\\square=/, we haveI0=𝔽I\_\{0\}=\\mathbb\{F\}, andΦ​\(I0\)=Φ​\(𝔽\)\\Phi\(I\_\{0\}\)=\\Phi\(\\mathbb\{F\}\)\. Moreover,Φ​\(Ij\)≥0\\Phi\(I\_\{j\}\)\\geq 0for allj∈ℕj\\in\\mathbb\{N\}and for every interval not included inIjI\_\{j\}, the potential is strictly decreasing, that isΦ​\(Ij\+1\)≤Φ​\(Ij\)−δ\\Phi\(I\_\{j\+1\}\)\\leq\\Phi\(I\_\{j\}\)\-\\deltafor someδ\>0\\delta\>0\. Therefore, there exists an indexk∈ℕk\\in\\mathbb\{N\}, s\.t\.Ik=Ik\+1I\_\{k\}=I\_\{k\+1\}, and the algorithm terminates after finitely many steps\. The number of iterations is bounded byt/=O​\(d\)t\_\{/\}=O\(d\)\.

The final argument follows plugging into the total complexity of Alg\.[1](https://arxiv.org/html/2606.23858#algorithm1)the time complexity of operators\{/,⊔\}\\\{/,\\sqcup\\\}\.■\\blacksquare

###### Proof

LetG=\(V,E\)G=\(V,E\)a simple undirected graph with\|V\|=d\|V\|=d\. We fix any constantw\>0w\>0and wlog we work on\[0,1\]d\[0,1\]^\{d\}\. From Lem\. 2 in\[[1](https://arxiv.org/html/2606.23858#bib.bib1)\]ifI⊆\[0,1\]dI\\subseteq\[0,1\]^\{d\}is a maximum\-volume feasible interval, then∂I\\partial Icontains𝟎\\mathbf\{0\}and theii\-th dimension ofIIis eitherwwor11\. Therefore, the maximum\-volume intervalIIhasℓi=0\\ell\_\{i\}=0for everyii, and eachui∈\{w,1\}u\_\{i\}\\in\\\{w,1\\\}, meaning thatI=\[𝟎,𝐮\]I=\[\\mathbf\{0\},\\mathbf\{u\}\]\. The intervalIIhas volumev​\(I\)=∏i∈\[d\]\(ui−ℓi\)v\(I\)=\\prod\_\{i\\in\[d\]\}\(u\_\{i\}\-\\ell\_\{i\}\)\. Applying Th\. 2 from\[[1](https://arxiv.org/html/2606.23858#bib.bib1)\], graphGGhas an independent set of size at leastkkiff there exists an intervalI∈𝔽I\\in\\mathbb\{F\}of volume at leastwkw^\{k\}\. Consequently, deciding whether there exists any empty interval of volume at leastwkw^\{k\}isNP\-hard\. Takingγ=wk\\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\}withv​\(I\)≥γv\(I\)\\geq\\gammaisNP\-hard\. Therefore, the q\-MERdecision problem isNP\-hard, and the proof is complete\.■\\blacksquare