Interval Certifications for Multilayered Perceptrons via Lattice Traversal

# Interval Certifications for Multilayered Perceptrons via Lattice Traversal
Source: [https://arxiv.org/html/2607.08773](https://arxiv.org/html/2607.08773)
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

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

## 1Introduction

Artificial Intelligence, mostly driven by deep neural networks \(NN\), is rapidly becoming part of our everyday life, from recommendation systems in media platforms\[[39](https://arxiv.org/html/2607.08773#bib.bib88)\]to large language models chat\-bots\[[4](https://arxiv.org/html/2607.08773#bib.bib89)\]\. Despite these achievements, NNs promise even greater accomplishments by replacing humans in critical, decision\-making areas, from driving\[[18](https://arxiv.org/html/2607.08773#bib.bib90)\]to healthcare\[[21](https://arxiv.org/html/2607.08773#bib.bib91)\]or government administration\[[40](https://arxiv.org/html/2607.08773#bib.bib92)\]\. However, NNs are brittle, meaning that small, often imperceptible input perturbations can flip their predictions\. These inputs are commonly referred to as*adversarial examples*\[[9](https://arxiv.org/html/2607.08773#bib.bib58),[24](https://arxiv.org/html/2607.08773#bib.bib69),[31](https://arxiv.org/html/2607.08773#bib.bib59)\]\.

Ensuring a NN’s*robustness*to adversarial attacks remains a persisting problem for AI safety\. The first works on the field focused on exploiting the gradient information to produce adversarial examples, subsequently incorporating them into the learning process, e\.g\.,\[[9](https://arxiv.org/html/2607.08773#bib.bib58),[23](https://arxiv.org/html/2607.08773#bib.bib60)\]\. Nevertheless, these initial attempts fail to solve the problem in its generality\[[37](https://arxiv.org/html/2607.08773#bib.bib71)\]\. More sophisticated methods utilized the convex relaxation of a NN\[[6](https://arxiv.org/html/2607.08773#bib.bib72)\], reducing adversarial robustness to a convex optimization problem\. This problem was either solved directly\[[12](https://arxiv.org/html/2607.08773#bib.bib76),[17](https://arxiv.org/html/2607.08773#bib.bib75),[19](https://arxiv.org/html/2607.08773#bib.bib74)\], or in its dual form\[[33](https://arxiv.org/html/2607.08773#bib.bib73)\]\. Even so, this family of works suffers from low precision, since they rely on a relaxation of the original problem\[[25](https://arxiv.org/html/2607.08773#bib.bib77),[29](https://arxiv.org/html/2607.08773#bib.bib78)\]\.

The hardness of adversarial robustness stems from the NN representation and seems to be deeply rooted in its computational properties\. NN’s activation functions introduce nonlinearities that can only be studied using integer constraints\. Therefore, NN can only be accurately described as*mixed integer linear programs \(MILPs\)*\[[13](https://arxiv.org/html/2607.08773#bib.bib34)\]\. The MILP description of a NN made it possible to construct sound and complete NN verifiers \(e\.g\.,Marabou\[[15](https://arxiv.org/html/2607.08773#bib.bib20),[34](https://arxiv.org/html/2607.08773#bib.bib22)\]\), improving upon earlier*Satisfiability Modulo Theory \(SMT\)*techniques, e\.g\.,Reluplex\[[14](https://arxiv.org/html/2607.08773#bib.bib21)\]\. Formal NN Verifiers prove ifσ​\(X\)=Y\\sigma\(X\)=Y, for a pair of I/O\-setsX,YX,Y, and a given NNσ​\(⋅\)\\sigma\(\\cdot\)\. If the property does not hold, they provide a*counterexample*, namely some𝐱∈X\\mathbf\{x\}\\in X, s\.t\.σ​\(𝐱\)∉Y\\sigma\(\\mathbf\{x\}\)\\notin Y\. However, this precision comes at a cost\. Verifying a property on NN isNP\-hard\[[14](https://arxiv.org/html/2607.08773#bib.bib21)\]\. Moreover, verifying that a given area is free of adversarial examples does not admit an approximate algorithm\[[38](https://arxiv.org/html/2607.08773#bib.bib24)\]\.

This work aspires to provide a detailed formal analysis on robustness certification\. Our work differs from previous attempts\[[12](https://arxiv.org/html/2607.08773#bib.bib76),[17](https://arxiv.org/html/2607.08773#bib.bib75),[19](https://arxiv.org/html/2607.08773#bib.bib74),[33](https://arxiv.org/html/2607.08773#bib.bib73)\]in considering the underlying problem in its generality\. We consider the family of*interval*certifications, i\.e\., axis\-aligned hyper\-rectangles, containing a given input𝐱\\mathbf\{x\}\. To our knowledge, this is the most general family of certification considered in the literature\[[12](https://arxiv.org/html/2607.08773#bib.bib76),[17](https://arxiv.org/html/2607.08773#bib.bib75)\]\. Utilizing Sunaga’s Interval Algebra\[[30](https://arxiv.org/html/2607.08773#bib.bib82)\], we show that the space of interval certifications is organized as an*innumerable, complete lattice*\. We introduce a set of*lattice traversal operators*that enable systematic exploration of this space\. These operators are then applied to refine\-and\-verify iterative schemes for computing*maximally sound*and*minimally complete*interval certifications\. An intervalIIconstitutes*sound certification*, if𝐱∈I\\mathbf\{x\}\\in Iand𝐱\\mathbf\{x\}can vary arbitrarily withinIIwithout changing model’s prediction\. Dually,IIis a*complete certification*, if𝐱∈I\\mathbf\{x\}\\in Iand any movement of𝐱\\mathbf\{x\}outsideIIis guaranteed to change the prediction\. Minimality and maximality are defined, w\.r\.t\. set inclusion\. Existing approaches\[[12](https://arxiv.org/html/2607.08773#bib.bib76),[17](https://arxiv.org/html/2607.08773#bib.bib75),[19](https://arxiv.org/html/2607.08773#bib.bib74),[33](https://arxiv.org/html/2607.08773#bib.bib73)\]compute sound certifications,*without*guaranteeing maximality\. Moreover, complete certifications have not, to the best of our knowledge, been considered in the literature\.

Further we examine optimization problems over interval certifications, focusing on the*minimum edge length*objective, which is widely used in prior work\[[17](https://arxiv.org/html/2607.08773#bib.bib75),[19](https://arxiv.org/html/2607.08773#bib.bib74),[33](https://arxiv.org/html/2607.08773#bib.bib73)\]\. In contrast to existing methods, our approach provides*non\-triviality guarantees*for our certifications\. Namely, our algorithms can*decide*if a non\-trivial solution exists to a given optimization problem, under certain assumptions\. This core functionality is lacking in existing methods, due to their reliance on relaxation\. We provide a qualitative comparison between existing work and ours in Tbl\.[1](https://arxiv.org/html/2607.08773#S1.T1)\. Finally, we strengthen known intractability results, showing that computing optimal sound interval certifications cannot be achieved in polynomial time, w\.r\.t\. the input dimension, the number of verification calls, and the time of each verification call\.

WorkMLPRepr\.Cert\.SoundComp\.Max/MinObj\.Non\-Triv\.Wong et al\.\[[33](https://arxiv.org/html/2607.08773#bib.bib73)\]DualUnif\.✓✗✗α/𝒜\\alpha/\\mathcal\{A\}✗Liu et al\.\[[19](https://arxiv.org/html/2607.08773#bib.bib74)\]DualSym\.✓✗✗α\\alpha✗Li et al\.\[[17](https://arxiv.org/html/2607.08773#bib.bib75)\]Conv\.Gen\.✓✗✗α\\alpha✗Kabahala et al\.\[[12](https://arxiv.org/html/2607.08773#bib.bib76)\]MILP\+Conv\.Gen\.✓✗✓𝒜\\mathcal\{A\}✗This workMILPGen✓✓✓α\\alpha✓

Table 1:Comparing existing work withParallelepipedoNN\. Conv\.: the primary convex approximation\. Dual: the dual convex approximation\. Unif\.: uniform intervals, i\.e\.ℓ∞\\ell\_\{\\infty\}\-circles\. Sym\.: symmetric intervals of the form\[𝐱−𝐞,𝐱\+𝐞\]\[\\mathbf\{x\}\-\\mathbf\{e\},\\mathbf\{x\}\+\\mathbf\{e\}\]\. Gen\.: General intervals\. Finally, withα\\alpha, we denote the minimum edge length, while with𝒜\\mathcal\{A\}the maximum edge length, or*diameter*\.\[[12](https://arxiv.org/html/2607.08773#bib.bib76)\]offers maximal solutions, but for diameter optimization\.\[[33](https://arxiv.org/html/2607.08773#bib.bib73)\]examines uniform intervals, thus the min\. edge lengthα\\alphaand the diameter𝒜\\mathcal\{A\}coincide, for theℓ∞\\ell\_\{\\infty\}\-norm\.Outline\.In Sec\.[2](https://arxiv.org/html/2607.08773#S2), we introduce the necessary preliminaries\. Sec\.[3](https://arxiv.org/html/2607.08773#S3)develops the interval algebra required for our analysis, while Sec\.[4](https://arxiv.org/html/2607.08773#S4)explores the structure of the space of interval certifications\. In Sec\.[5](https://arxiv.org/html/2607.08773#S5)we review optimization problems\. Finally, Sec\.[6](https://arxiv.org/html/2607.08773#S6)presents theParallelepipedoNNsystem and discusses the practical implications of our work\.

## 2Preliminaries

In this section, we review some elementary notions and definitions that will be needed in the rest of this work\. For any natural numberd∈ℕd\\in\\mathbb\{N\}, we denote with\[d\]\[d\]the set\{1,2,…,d\}\\\{1,2,\\dots,d\\\}\. Vectors will be denoted by bold, e\.g\.,𝐱\\mathbf\{x\}, while scalar values by light, e\.g\.,xx\. For add\-dimensional vector𝐱\\mathbf\{x\}we denote withxix\_\{i\}itsii\-th coordinate\. Moreover, letf:ℝ→ℝf\\colon\\mathbb\{R\}\\to\\mathbb\{R\}be a real function that takes as input somex∈ℝx\\in\\mathbb\{R\}\. For a vector input𝐱∈ℝd\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}, we denote with𝐟​\(𝐱\)∈ℝd\\mathbf\{f\}\(\\mathbf\{x\}\)\\in\\mathbb\{R\}^\{d\}the vector function*induced byff*, i\.e\.,𝐟​\(𝐱\)=\(f​\(x1\),…,f​\(xd\)\)\\mathbf\{f\}\(\\mathbf\{x\}\)=\(f\(x\_\{1\}\),\\dots,f\(x\_\{d\}\)\)\. Thedd\-dimensional vectors𝟎\\mathbf\{0\}and𝟏\\mathbf\{1\}denote the zero and the all\-ones vectors\. For eachi∈\[d\]i\\in\[d\], we denote with𝐞i\\mathbf\{e\}^\{i\}a vector, s\.t\.eji=0e^\{i\}\_\{j\}=0, wheni≠ji\\neq j, andeii=1e^\{i\}\_\{i\}=1\. Finally, matricesA∈ℝd1×d2A\\in\\mathbb\{R\}^\{d\_\{1\}\\times d\_\{2\}\}are denoted with capital letters\.

#### Normed Vector Spaces\.

In this work, we are interested indd\-dimensional*normed vector spaces*on the*real field*ℝ\\mathbb\{R\}\. We will useℓp\\ell\_\{p\}\-norms, denoted‖𝐱‖p\\\|\\mathbf\{x\}\\\|\_\{p\}and defined as‖𝐱‖p=∑i∈\[d\]\|xi\|pp\\\|\\mathbf\{x\}\\\|\_\{p\}=\\sqrt\[p\]\{\\sum\_\{i\\in\[d\]\}\|x\_\{i\}\|^\{p\}\}\. In the limitp→∞p\\to\\inftythis reduces to the infinity norm‖𝐱‖∞=maxi∈\[d\]⁡\|xi\|\\\|\\mathbf\{x\}\\\|\_\{\\infty\}=\\max\_\{i\\in\[d\]\}\|x\_\{i\}\|\.

Withℬp​\(𝐱⋆,ρ\)⊂ℝd,ρ\>0\\mathcal\{B\}^\{p\}\(\\mathbf\{x\}^\{\\star\},\\rho\)\\subset\\mathbb\{R\}^\{d\},\\rho\>0we denote thedd\-dimensional sphere around𝐱\\mathbf\{x\}with radiusρ\\rhow\.r\.t\. the∥⋅∥p\\\|\\cdot\\\|\_\{p\}norm, i\.e\.,ℬp​\(𝐱⋆,ρ\)=\{𝐱∈ℝd∣‖𝐱−𝐱⋆‖p≤ρ\}\\mathcal\{B\}^\{p\}\(\\mathbf\{x\}^\{\\star\},\\rho\)=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}\\mid\\\|\\mathbf\{x\}\-\\mathbf\{x\}^\{\\star\}\\\|\_\{p\}\\leq\\rho\\\}\. Consider a setS⊆ℝdS\\subseteq\\mathbb\{R\}^\{d\}\. With∂S\\partial Swe denote the*boundary*ofSSw\.r\.t\. the measure∥⋅∥p\\\|\\cdot\\\|\_\{p\}, i\.e\.,∂S=\{𝐱∈S∣∀ρ\>0,ℬp​\(𝐱,ρ\)∩\(ℝd∖S\)≠∅\}\\partial S=\\\{\\mathbf\{x\}\\in S\\mid\\forall\\rho\>0,~~\\mathcal\{B\}^\{p\}\(\\mathbf\{x\},\\rho\)\\cap\(\\mathbb\{R\}^\{d\}\\setminus S\)\\neq\\emptyset\\\}\. The*interior*ofSS, denoted byS∘S^\{\\circ\}, is composed of the points ofSSnot belonging to the boundary, i\.e\.,S∘=S∖∂SS^\{\\circ\}=S\\setminus\\partial S\. A setS⊆ℝdS\\subseteq\\mathbb\{R\}^\{d\}is*open*w\.r\.t\. the measure∥⋅∥p\\\|\\cdot\\\|\_\{p\}if for every𝐱∈S\\mathbf\{x\}\\in S, there is aρ\>0\\rho\>0such thatℬp​\(𝐱,ρ\)⊆S\\mathcal\{B\}^\{p\}\(\\mathbf\{x\},\\rho\)\\subseteq S\. A setS⊆ℝdS\\subseteq\\mathbb\{R\}^\{d\}is*closed*ifℝd∖S\\mathbb\{R\}^\{d\}\\setminus Sis open\. A setS⊆ℝdS\\subseteq\\mathbb\{R\}^\{d\}is called*bounded*if there is some finiteρ\>0\\rho\>0s\.t\.ℬ∞​\(𝟎,ρ\)⊇S\\mathcal\{B\}^\{\\infty\}\(\\mathbf\{0\},\\rho\)\\supseteq S\. Finally, a closed and bounded set is*compact*\.

#### Multilayered Perceptrons\.

A MLP is a functionσ:𝔽→𝕊\\sigma\\colon\\mathbb\{F\}\\to\\mathbb\{S\}, with𝔽⊂ℝdin\\mathbb\{F\}\\subset\\mathbb\{R\}^\{\{d\_\{\\text\{in\}\}\}\},𝕊⊂ℝdout\\mathbb\{S\}\\subset\\mathbb\{R\}^\{d\_\{\\text\{out\}\}\}denoting the features \(input\) and scores \(output\) spaces, respectively\. We focus on MLPs, with*rectified linear units \(ReLU\)*\[[7](https://arxiv.org/html/2607.08773#bib.bib50)\]as activation functions\. Forx∈ℝx\\in\\mathbb\{R\}the ReLU functionr​\(x\)r\(x\)is given asr​\(x\)=max⁡\(0,x\)r\(x\)=\\max\(0,x\)\. In higher dimensions, we have𝐫​\(𝐱\)=\(r​\(x1\),…,r​\(xd\)\)\\mathbf\{r\}\(\\mathbf\{x\}\)=\(r\(x\_\{1\}\),\\dots,r\(x\_\{d\}\)\)\. We give the following formal definition\.

###### Definition 1\(Multilayered Perceptron\)

A*multilayered perceptron*σ:𝔽→𝕊\\sigma\\colon\\mathbb\{F\}\\to\\mathbb\{S\}, with𝔽⊂ℝ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,Q⟩\\sigma=\\langle L,D,W,Q\\rangle\. WithL∈ℕL\\in\\mathbb\{N\}, we denote the*number of layers*\. WithDD, we denote a sequence ofL\+1L\+1natural numbers, wheredin=d0,d1,…,dL−1,dL=dout\{d\_\{\\text\{in\}\}\}=d\_\{0\},d\_\{1\},\\dots,d\_\{L\-1\},d\_\{L\}=d\_\{\\text\{out\}\}\. WithWW, we denote a sequence ofLLreal matrices, s\.t\.W\(i\)∈ℝdi×di−1W^\{\(i\)\}\\in\\mathbb\{R\}^\{d\_\{i\}\\times d\_\{i\-1\}\}, for eachi∈\[L\]i\\in\[L\]\. Finally, withQQwe denote a sequence ofLLreal vectors, s\.t\.𝐪\(i\)∈ℝdi\\mathbf\{q\}^\{\(i\)\}\\in\\mathbb\{R\}^\{d\_\{i\}\}, for eachi∈\[L\]i\\in\[L\]\. For an input𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, the value ofσ​\(𝐱\)\\sigma\(\\mathbf\{x\}\)is given as the valueσ\(L\)\\sigma^\{\(L\)\}in the system of recursive 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\{q\}^\{\(i\)\}\],\\quad\\forall i\\in\[L\]\\end\{array\}\\right\\\}\(1\)

For*classification*problems, let𝒞⊂ℕ\\mathcal\{C\}\\subset\\mathbb\{N\}be a finite set of classes, with\|𝒞\|=dout\|\\mathcal\{C\}\|=d\_\{\\text\{out\}\}\. A classifierκ:𝔽→𝒞\\kappa\\colon\\mathbb\{F\}\\to\\mathcal\{C\}is constructed, with respect to the MLPσ​\(⋅\)\\sigma\(\\cdot\), asκ​\(𝐱\)=arg⁡maxi∈\[dout\]⁡σi​\(𝐱\)\\kappa\(\\mathbf\{x\}\)=\\arg\\max\_\{i\\in\[d\_\{\\text\{out\}\}\]\}\\sigma\_\{i\}\(\\mathbf\{x\}\)\. For a classc∈𝒞c\\in\\mathcal\{C\}, we denote with𝒟c\\mathcal\{D\}\_\{c\}the*decision surface*of the classcc\. Namely,𝒟c\\mathcal\{D\}\_\{c\}is the pre\-image ofκ​\(c\)\\kappa\(c\); consisting of all the inputs in𝔽\\mathbb\{F\}that are classified tocc, byκ​\(⋅\)\\kappa\(\\cdot\)\.

#### Formal MLP Verification\.

The MLP of Def\.[1](https://arxiv.org/html/2607.08773#Thmdefinition1)can be expressed as a set of linear inequalities, with real and integer variables\. This formalization is known in the literature as*Mixed Integer Linear Programming \(MILP\)*\.

𝐳^\(0\)=𝐱,𝐲=𝐳^\(L\)𝐳\(i\)=W\(i\)​𝐳^\(i−1\)\+𝐪\(i\),∀i∈\[L\]𝐳^\(i\)≥𝐳\(i\),𝐳^\(i\)≥𝟎,∀i∈\[L\]𝐳^\(i\)≤𝐳\(i\)\+M​𝐭\(i\),∀i∈\[L\]𝐳^\(i\)≤M​\(𝟏−𝐭\(i\)\),∀i∈\[L\]𝐱∈ℝdin,𝐲∈ℝdout𝐭\(i\)∈\{0,1\}douti,𝐳\(i\)∈ℝdouti∀i∈\[L\]\}\\left\.\\begin\{array\}\[\]\{l l l\}\\lx@intercol\\widehat\{\\mathbf\{z\}\}^\{\(0\)\}=\\mathbf\{x\},~\\mathbf\{y\}=\\widehat\{\\mathbf\{z\}\}^\{\(L\)\}\\hfil\\lx@intercol\\\\ \\mathbf\{z\}^\{\(i\)\}&=W^\{\(i\)\}\\widehat\{\\mathbf\{z\}\}^\{\(i\-1\)\}\+\\mathbf\{q\}^\{\(i\)\},&\\forall i\\in\[L\]\\\\ \\lx@intercol\\widehat\{\\mathbf\{z\}\}^\{\(i\)\}\\geq\\mathbf\{z\}^\{\(i\)\},~\\widehat\{\\mathbf\{z\}\}^\{\(i\)\}\\geq\\mathbf\{0\},\\hfil\\lx@intercol&\\forall i\\in\[L\]\\\\ \\widehat\{\\mathbf\{z\}\}^\{\(i\)\}&\\leq\\mathbf\{z\}^\{\(i\)\}\+M\\mathbf\{t\}^\{\(i\)\},&\\forall i\\in\[L\]\\\\ \\widehat\{\\mathbf\{z\}\}^\{\(i\)\}&\\leq M\(\\mathbf\{1\}\-\\mathbf\{t\}^\{\(i\)\}\),&\\forall i\\in\[L\]\\\\ \\\\ \\lx@intercol\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\_\{\\text\{in\}\}\},~\\mathbf\{y\}\\in\\mathbb\{R\}^\{d\_\{\\text\{out\}\}\}\\hfil\\lx@intercol\\\\ \\lx@intercol\\mathbf\{t\}^\{\(i\)\}\\in\\\{0,1\\\}^\{d^\{i\}\_\{\\text\{out\}\}\},~\\mathbf\{z\}^\{\(i\)\}\\in\\mathbb\{R\}^\{d^\{i\}\_\{\\text\{out\}\}\}\\hfil\\lx@intercol&\\forall i\\in\[L\]\\\\ \\end\{array\}\\right\\\}\(2\)In eq\. \([2](https://arxiv.org/html/2607.08773#S2.E2)\), we denote with𝐳\\mathbf\{z\}the value of the neuron*before*the ReLU activation, while with𝐳^\\widehat\{\\mathbf\{z\}\}the value of the neuron*after*the activation is applied\. We use the constantMM222Here we use the big\-M formalization of\[[20](https://arxiv.org/html/2607.08773#bib.bib35)\]\. Other formalizations have also been proposed, see the survey of\[[24](https://arxiv.org/html/2607.08773#bib.bib69)\]\.representing a high value, practically treated as infinity\. The variables𝐭\\mathbf\{t\}model ReLU’s behaviour\. For thejj\-th neuron of theii\-th layer,tj\(i\+1\)=0t^\{\(i\+1\)\}\_\{j\}=0*iff*z^j\(i\+1\)=zj\(i\+1\)\\widehat\{z\}^\{\(i\+1\)\}\_\{j\}=z^\{\(i\+1\)\}\_\{j\}, i\.e\., ReLU is activated; otherwise,tj\(i\+1\)=1t^\{\(i\+1\)\}\_\{j\}=1\.

The MILP formalization allows us to*rigorously*reason about the MLP’s behaviour\. In particular, eq\. \([2](https://arxiv.org/html/2607.08773#S2.E2)\) formally defines a relation𝒩⊆𝔽×𝕊\\mathcal\{N\}\\subseteq\\mathbb\{F\}\\times\\mathbb\{S\}, s\.t\. for an I/O\-pair⟨𝐱,𝐲⟩∈𝔽×𝕊\\langle\\mathbf\{x\},\\mathbf\{y\}\\rangle\\in\\mathbb\{F\}\\times\\mathbb\{S\}, we have⟨𝐱,𝐲⟩∈𝒩\\langle\\mathbf\{x\},\\mathbf\{y\}\\rangle\\in\\mathcal\{N\},*iff*σ​\(𝐱\)=𝐲\\sigma\(\\mathbf\{x\}\)=\\mathbf\{y\}\. A verifier is essentially another relation𝒱⊆𝔽×𝕊\\mathcal\{V\}\\subseteq\\mathbb\{F\}\\times\\mathbb\{S\}\. We call the verifier𝒱\\mathcal\{V\}*sound*if𝒱⊆𝒩\\mathcal\{V\}\\subseteq\\mathcal\{N\}\. We call the verifier𝒱\\mathcal\{V\}*complete*if𝒩⊆𝒱\\mathcal\{N\}\\subseteq\\mathcal\{V\}\. Sound and complete verifiers such as Marabou\[[15](https://arxiv.org/html/2607.08773#bib.bib20)\]make heavy use of cutting\-edge MILP solvers, e\.g\., Gurobi333[https://www\.gurobi\.com](https://www.gurobi.com/), while utilizing sophisticated heuristics tailored for MILPs modeling MLPs\. This allows them to analyse much larger networks, whose size would be otherwise prohibiting\. Still, note that verifying a MLP is anNP\-complete problem\[[13](https://arxiv.org/html/2607.08773#bib.bib34)\]\.

## 3Intervals in Higher Dimensions

In this section, we present some foundational results from*Interval Algebra*\[[30](https://arxiv.org/html/2607.08773#bib.bib82),[26](https://arxiv.org/html/2607.08773#bib.bib81)\]\. Firstly, we generalize the≤⊆ℝ×ℝ\\leq~\\subseteq\\mathbb\{R\}\\times\\mathbb\{R\}relation to high\-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\]\. Similarly, we writeℓ<𝒖\\boldsymbol\{\\ell\}<\\boldsymbol\{u\}*iff*ℓi<ui\\ell\_\{i\}<u\_\{i\}for eachi∈\[d\]i\\in\[d\]444Note that it does*not*hold thatℓ<𝒖\\boldsymbol\{\\ell\}<\\boldsymbol\{u\}wheneverℓ≤𝒖\\boldsymbol\{\\ell\}\\leq\\boldsymbol\{u\}andℓ≠𝒖\\boldsymbol\{\\ell\}\\neq\\boldsymbol\{u\}\.\. Below, we describe a generalization of real intervals for high\-dimensional spaces\.

###### Definition 2\(High Dimensional Intervals\)

Letℓ,𝒖∈ℝd\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\\in\\mathbb\{R\}^\{d\}, withℓ≤𝒖\\boldsymbol\{\\ell\}\\leq\\boldsymbol\{u\}\. A*closed 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\}\. An*open interval*\(ℓ,𝒖\)\(\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\)is the interior of the respective closed interval, i\.e\.,\(ℓ,𝒖\)=\[ℓ,𝒖\]∘\(\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\)=\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]^\{\\circ\}\. We denote with𝕀​\(d\)\\mathbb\{I\}\(d\)the space of thedd–dimensional*closed*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\}\]\\\}\.

From the above definition, it is easy to see that𝐱∈\(ℓ,𝒖\)\\mathbf\{x\}\\in\(\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\)*iff*ℓ<𝐱<𝒖\\boldsymbol\{\\ell\}<\\mathbf\{x\}<\\boldsymbol\{u\}\. Note that for any𝐱∈ℝd\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}the closed interval\[𝐱,𝐱\]\[\\mathbf\{x\},\\mathbf\{x\}\]is a*trivial interval*, corresponding to the singleton\{𝐱\}\\\{\\mathbf\{x\}\\\}\. Additionally, the trivial open interval\(𝐱,𝐱\)\(\\mathbf\{x\},\\mathbf\{x\}\)corresponds to the empty set∅\\varnothing\. Observe that the sphereℬ∞​\(𝐱,ρ\)\\mathcal\{B\}^\{\\infty\}\(\\mathbf\{x\},\\rho\)corresponds to the*uniform*interval\[𝐱−ρ​𝟏,𝐱\+ρ​𝟏\]\[\\mathbf\{x\}\-\\rho\\mathbf\{1\},\\mathbf\{x\}\+\\rho\\mathbf\{1\}\]\. Geometrically, an interval\[ℓ,𝒖\]\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]corresponds to a*hyper\-rectangle*inℝd\\mathbb\{R\}^\{d\}\. In particular, a uniform interval centered at𝐱\\mathbf\{x\}corresponds to a*hyper\-cube*with𝐱\\mathbf\{x\}as its barycenter\. We extend the notation of Definition[2](https://arxiv.org/html/2607.08773#Thmdefinition2), denoting with𝕀​\(d\)\|𝐱⊆𝕀​\(d\)\\mathbb\{I\}\(d\)\|\_\{\\mathbf\{x\}\}\\subseteq\\mathbb\{I\}\(d\)*the set of all intervals including the point𝐱∈ℝd\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}*\. Naturally, for every𝐱∈ℝd\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}, and everyρ\>0\\rho\>0,ℬ∞​\(𝐱,ρ\)∈𝕀​\(d\)\|𝐱\\mathcal\{B\}^\{\\infty\}\(\\mathbf\{x\},\\rho\)\\in\\mathbb\{I\}\(d\)\|\_\{\\mathbf\{x\}\}\. We often consider an*interval universe*𝔽=\[𝐔¯,𝐔¯\]\\mathbb\{F\}=\[\\underline\{\\mathbf\{U\}\},\\overline\{\\mathbf\{U\}\}\], for specific𝐔¯,𝐔¯\\underline\{\\mathbf\{U\}\},\\overline\{\\mathbf\{U\}\}\. We denote with𝕀​\(d\)\|𝐱𝔽⊆𝕀​\(d\)\|𝐱\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\\subseteq\\mathbb\{I\}\(d\)\|\_\{\\mathbf\{x\}\}*all the intervals that include the point𝐱\\mathbf\{x\}and are included in𝔽\\mathbb\{F\}*\.

### 3\.1Operations on Intervals & the Interval Lattice

Below we give some elementary operations on the interval space𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\.\{restatable\}propositionintervalops Let\[ℓ,𝒖\],\[𝒎,𝒏\]∈𝕀​\(d\)\|𝐱𝔽\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\],\[\\boldsymbol\{m\},\\boldsymbol\{n\}\]\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}twodd–dimensional intervals, and the operations:

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

For any□∈\{\+,⊔,⊓\}\\square\\in\\\{\+,\\sqcup,\\sqcap\\\}andI,J∈𝕀​\(d\)\|𝐱𝔽I,J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\},I​□​J∈𝕀​\(d\)\|𝐱𝔽I~\\square~J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\. Observe that the⊓\\sqcapoperator coincides with the set\-theoretic intersection∩\\cap\. However, it holds thatI⊔J⊋I∪JI~\\sqcup~J\\supsetneq I\\cup J\. In general, the union of two intervals is not an interval\. Below, we review how the⊔,⊓\\sqcup,\\sqcapoperations reveal the underlying structure of the interval space𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\.

###### Theorem 3\.1\(Interval Lattice,\[[30](https://arxiv.org/html/2607.08773#bib.bib82)\]\)

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

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

###### Definition 3

LetI=\[ℓ,𝒖\]∈𝕀​\(d\)\|𝐱𝔽I=\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}be an interval and𝐱′∈I\\mathbf\{x\}^\{\\prime\}\\in Ia point included in the intervalII\. Letk=arg⁡max⁡\{\|xi−xi′\|∣i∈\[d\]∧𝐱∈𝕀​\(d\)\|𝐱𝔽\}k=\\arg\\max\\\{\|x\_\{i\}\-x^\{\\prime\}\_\{i\}\|\\mid i\\in\[d\]\\wedge\\mathbf\{x\}\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\\\}555In general, thearg⁡max⁡\{\|xi−xi′\|∣i∈\[d\]∧𝐱∈𝕀​\(d\)\|𝐱𝔽\}\\arg\\max\\\{\|x\_\{i\}\-x^\{\\prime\}\_\{i\}\|\\mid i\\in\[d\]\\wedge\\mathbf\{x\}\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\\\}may provide a set of indices, meaning that there are ties w\.r\.t\. the smallest changes we can impose in the interval\. Since, in any interval, any change in any dimension is orthogonal to any changes in any other dimension, we can apply any tie\-breaking rule, e\.g\., lexicographic ordering\.\. Ifxi−xi′\>0x\_\{i\}\-x^\{\\prime\}\_\{i\}\>0, thenI​/δ​𝐱′=\[ℓ′,𝒖\]I\\\!\\sideset\{\}\{\{\}\_\{\\delta\}\}\{\\mathop\{\\scalebox\{1\.0\}\[1\.3\]\{/\}\}\}\\mathbf\{x\}^\{\\prime\}=\[\\boldsymbol\{\\ell\}^\{\\prime\},\\boldsymbol\{u\}\], whereℓi′=ℓi\\ell^\{\\prime\}\_\{i\}=\\ell\_\{i\}, for everyi≠ki\\neq kandℓk=xk′\+δ\\ell\_\{k\}=x^\{\\prime\}\_\{k\}\+\\delta, for someδ\>0\\delta\>0\. Ifxi−xi′<0x\_\{i\}\-x^\{\\prime\}\_\{i\}<0, thenI​/δ​𝐱′=\[ℓ,𝒖′\]I\\\!\\sideset\{\}\{\{\}\_\{\\delta\}\}\{\\mathop\{\\scalebox\{1\.0\}\[1\.3\]\{/\}\}\}\\mathbf\{x\}^\{\\prime\}=\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}^\{\\prime\}\], whereui′=uiu^\{\\prime\}\_\{i\}=u\_\{i\}, for everyi≠ki\\neq kanduk=xk′−δu\_\{k\}=x^\{\\prime\}\_\{k\}\-\\delta, for someδ\>0\\delta\>0\.

Despite its subtleties, we will see in Sec\.[4](https://arxiv.org/html/2607.08773#S4)that operator/δ\\\!\\sideset\{\}\{\{\}\_\{\\delta\}\}\{\\mathop\{\\scalebox\{1\.0\}\[1\.3\]\{/\}\}\}is natural\.I​/δ​𝐱′I\\\!\\sideset\{\}\{\{\}\_\{\\delta\}\}\{\\mathop\{\\scalebox\{1\.0\}\[1\.3\]\{/\}\}\}\\mathbf\{x\}^\{\\prime\}chooses a*maximum*refinement ofIIthat excludes𝐱′\\mathbf\{x\}^\{\\prime\}\. Further, to simplify notation, we will drop theδ\\deltafrom the notation of/δ\\\!\\sideset\{\}\{\{\}\_\{\\delta\}\}\{\\mathop\{\\scalebox\{1\.0\}\[1\.3\]\{/\}\}\}when it’s clear from the context\.

### 3\.2Interval Objectives

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

###### Definition 4\(Interval Objectives\)

Consider an intervalI=\[ℓ,𝒖\]∈𝕀​\(d\)\|𝐱𝔽I=\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, withℓ≤𝒖\\boldsymbol\{\\ell\}\\leq\\boldsymbol\{u\}\. Then we define the following measures:

Minimum Edge Length:α​\(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\}

These objectives are related through the arithmetic\-geometric means inequality\.\{restatable\}propositionnumericalgeometricmean For an intervalI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}and the measures of Def\.[4](https://arxiv.org/html/2607.08773#Thmdefinition4)we have,

𝒜​\(I\)≥1d⋅π​\(I\)≥v​\(I\)d≥α​\(I\)\\mathcal\{A\}\(I\)\\geq\\frac\{1\}\{d\}\\cdot\\pi\(I\)\\geq\\sqrt\[d\]\{v\(I\)\}\\geq\\alpha\(I\)\(3\)Eq\. \([3](https://arxiv.org/html/2607.08773#S3.E3)\) highlights the significance of the minimum edge length measure within the family of interval measures defined in Def\.[4](https://arxiv.org/html/2607.08773#Thmdefinition4), since it provides an explicit lower bound on all other measures\. Thus, it*suffices*to ensure the non\-triviality, i\.e\., strict positivity, ofα​\(I\)\\alpha\(I\), to ensure the non\-triviality of all the remaining objectives\. This fact supports the choice of the exclusion operation of Def\.[3](https://arxiv.org/html/2607.08773#Thmdefinition3), since it computes the*optimal*exclusion w\.r\.t\. the minimum edge length objective\.\{restatable\}theoremintervalexclusion Consider an intervalI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}and a point𝐱′∈I\\mathbf\{x\}^\{\\prime\}\\in I\. For any intervalJ∈𝕀​\(d\)\|𝐱𝔽J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, with𝐱′∉J\\mathbf\{x\}^\{\\prime\}\\notin JandJ⊆IJ\\subseteq I, we haveα​\(J\)≤α​\(I/𝐱′\)\\alpha\(J\)\\leq\\alpha\(I/\\mathbf\{x\}^\{\\prime\}\)\.

## 4Sound & Complete Interval Certifications

![Refer to caption](https://arxiv.org/html/2607.08773v1/figures/demo-black-bw-balanced.png)Figure 1:A sound interval certification\[𝐥𝐛,𝐮𝐛\]\[\\mathbf\{lb\},\\mathbf\{ub\}\], and a complete interval certification\[𝐋𝐁,𝐔𝐁\]\[\\mathbf\{LB\},\\mathbf\{UB\}\], for a MNIST image of “7”\. The sound interval certification has been computed using the Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1), while its complete counterpart was computed by Algorithm[3](https://arxiv.org/html/2607.08773#algorithm3)inℓ∞\\ell\_\{\\infty\}\-spheres\.###### Definition 5

Consider a classifierκ:𝔽→𝒞\\kappa\\colon\\mathbb\{F\}\\to\\mathcal\{C\}, with𝔽⊂ℝd\\mathbb\{F\}\\subset\\mathbb\{R\}^\{d\}, and𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}an input, s\.t\.κ​\(𝐱\)=c\\kappa\(\\mathbf\{x\}\)=c\. Moreover, letI,J∈𝕀​\(d\)I,J\\in\\mathbb\{I\}\(d\)two intervals, s\.t\.

𝐱∈I∧\[∀𝐱′∈𝔽:𝐱′∈I→κ\(𝐱′\)=c\],𝐱∈J∧\[∀𝐱′∈𝔽:𝐱′∉J→κ\(𝐱′\)≠c\],\\mathbf\{x\}\\in I\\land\\left\[\\forall\\mathbf\{x\}^\{\\prime\}\\in\\mathbb\{F\}\\colon\\ \\mathbf\{x\}^\{\\prime\}\\in I\\to\\kappa\(\\mathbf\{x\}^\{\\prime\}\)=c\\right\],\\kern 5\.0pt\\mathbf\{x\}\\in J\\land\\left\[\\forall\\mathbf\{x\}^\{\\prime\}\\in\\mathbb\{F\}\\colon\\ \\mathbf\{x\}^\{\\prime\}\\notin J\\to\\kappa\(\\mathbf\{x\}^\{\\prime\}\)\\neq c\\right\],

\(4\)then we callIIa*sound*andJJa complete*certification*\.

Intuitively, a sound certificationIIassures that any perturbation of the input𝐱\\mathbf\{x\}insideIIwill*not*change its prediction\. On the other hand, a complete certificationJJasserts that if𝐱\\mathbf\{x\}is moved outside ofJJ, then its prediction is*guaranteed*to change \(see Fig\.[1](https://arxiv.org/html/2607.08773#S4.F1)\)\. Naturally, a*trivial*sound certification is the input itself, expressed as an interval, i\.e\.,I=\[𝐱,𝐱\]I=\[\\mathbf\{x\},\\mathbf\{x\}\]\. Similarly, a trivial complete certification will be the entire input space𝔽\\mathbb\{F\}itself\. Therefore, we are interested in*maximally*sound and*minimally*complete certifications\. SinceI,JI,Jare subsets of𝔽\\mathbb\{F\}, maximality and minimality are considered w\.r\.t\. set inclusion\.

### 4\.1Verification Oracles

In our algorithms, we will utilize two oracles that either verify the truth of a property on a given interval, or return a*counterexample*, witnessing its falsehood\. In particular, we are interested in*soundness*and*completeness*oracles, verifying an interval’s respective property\. These oracles can be constructed using a sound and complete MLP verifier666Note that soundness and completeness of a MLP verifier, w\.r\.t\. Sec\.[2](https://arxiv.org/html/2607.08773#S2)differ from soundness and completeness of an interval certification w\.r\.t\. Def\.[5](https://arxiv.org/html/2607.08773#Thmdefinition5)\.\. Indeed, we make use of the Marabou verifier\[[15](https://arxiv.org/html/2607.08773#bib.bib20)\], where we*extend*the set of constraints fed to the verifier\. To that end, let𝒩​\(𝐱,𝐲\)\\mathcal\{N\}\(\\mathbf\{x\},\\mathbf\{y\}\)be the I/O\-relation describing a MLP, as in eq\. \([2](https://arxiv.org/html/2607.08773#S2.E2)\)\.

For a given MLP, described by the relation𝒩​\(⋅,⋅\)\\mathcal\{N\}\(\\cdot,\\cdot\)and an intervalI=\[ℓ,𝒖\]⊆𝔽I=\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\subseteq\\mathbb\{F\}, the*soundness oracle*is given by the predicate𝒮I,𝒩\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}, where,

𝒮I,𝒩​\(𝐱′\)≡∃𝐲\.\(ℓ≤𝐱′≤𝒖\)∧𝒩​\(𝐱′,𝐲\)∧\(⋁j∈\[dout\]∖cyj−yc\>ϵ\)\.\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\)\\equiv\\exists\\mathbf\{y\}\.~\(\\boldsymbol\{\\ell\}\\leq\\mathbf\{x\}^\{\\prime\}\\leq\\boldsymbol\{u\}\)~\\land~\\mathcal\{N\}\(\\mathbf\{x\}^\{\\prime\},\\mathbf\{y\}\)~\\land~\\left\(\\bigvee\_\{j\\in\[d\_\{\\text\{out\}\}\]\\setminus c\}y\_\{j\}\-y\_\{c\}\>\\epsilon\\right\)\.

\(5\)If the predicate𝒮I,𝒩​\(𝐱′\)\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\)is a*contradiction*, i\.e\.,⊧¬𝒮I,𝒩​\(𝐱′\)\\models\\lnot\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\), the intervalIIis a sound certification\. However, any𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, s\.t\.𝐱′⊧𝒮I,𝒩​\(𝐱′\)\\mathbf\{x\}^\{\\prime\}\\models\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\)is a*counterexample*\. In the literature, such an input is also called*adversarial example*or*adversarial attack*\. Such a counterexample𝐱′\\mathbf\{x\}^\{\\prime\}can*“fool”*the MLP, since it will be relatively close to a given input𝐱\\mathbf\{x\}, but is classified to a different class fromc=κ​\(𝐱\)c=\\kappa\(\\mathbf\{x\}\)\. The latter is ensured by the last clause in eq\. \([5](https://arxiv.org/html/2607.08773#S4.E5)\), by asserting that a score different thanccis the highest in the output scores vector, w\.r\.t\. a constantϵ\>0\\epsilon\>0\.

Conversely, the*completeness oracle*is provided by predicate𝒞I,𝒩\\mathscr\{C\}\_\{I,\\mathcal\{N\}\}, where,

𝒞I,𝒩​\(𝐱′\)≡\(⋁i∈\[din\]xi′<ℓi∨ui<xi′\)∧𝒩​\(𝐱′,𝐲\)∧\(⋀j∈\[dout\]∖cyc−yj\>ϵ\)\.\\mathscr\{C\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\)\\equiv\\left\(\\bigvee\_\{i\\in\[\{d\_\{\\text\{in\}\}\}\]\}x\_\{i\}^\{\\prime\}<\\ell\_\{i\}\\lor u\_\{i\}<x\_\{i\}^\{\\prime\}\\right\)~\\land~\\mathcal\{N\}\(\\mathbf\{x\}^\{\\prime\},\\mathbf\{y\}\)~\\land~\\left\(\\bigwedge\_\{j\\in\[d\_\{\\text\{out\}\}\]\\setminus c\}y\_\{c\}\-y\_\{j\}\>\\epsilon\\right\)\.

\(6\)If the predicate𝒞I,𝒩​\(𝐱′\)\\mathscr\{C\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\)is a*contradiction*, i\.e\.,⊧¬𝒞I,𝒩​\(𝐱′\)\\models\\lnot\\mathscr\{C\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\), then the intervalIIis a complete certification\. However, any𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, s\.t\.𝐱′⊧𝒞I,𝒩​\(𝐱′\)\\mathbf\{x\}^\{\\prime\}\\models\\mathscr\{C\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\)is a*counterexample*\. Essentially, the completeness predicate is the dual of𝒮I,𝒩\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}\. Notably, since we use a sound and complete verification system, invoking both the oracles𝒮I,𝒩\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}and𝒞I,𝒩\\mathscr\{C\}\_\{I,\\mathcal\{N\}\}inherits the computational hardness of MLP verification\[[13](https://arxiv.org/html/2607.08773#bib.bib34)\]\.

Finally, observe that the formulas in eq\. \([5](https://arxiv.org/html/2607.08773#S4.E5)\) and \([6](https://arxiv.org/html/2607.08773#S4.E6)\) can be use to*“locally”*describe the MLP\. Consider a sound certificationIIand a complete verificationJJ, then it holds¬ℐI,𝒩​\(𝐱\)⊧κ​\(𝐱\)=c⊧¬𝒞J,𝒩​\(𝐱\)\\lnot\\mathscr\{I\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}\)\\models\\kappa\(\\mathbf\{x\}\)=c\\models\\lnot\\mathscr\{C\}\_\{J,\\mathcal\{N\}\}\(\\mathbf\{x\}\), sinceJ⊇𝒟c⊇IJ\\supseteq\\mathcal\{D\}\_\{c\}\\supseteq I\. Ensuring completeness minimality and soundness maximality minimizes the gap betweenJ,IJ,Iand provides a*tighter*local approximation of the underlying MLP\.

### 4\.2The Generic Traversal Algorithm

In Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)we present a simple traversal algorithm that explores the interval lattice𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}introduced in Sec\.[3](https://arxiv.org/html/2607.08773#S3)\. Our algorithm is generic in the sense that it can compute interval certifications with different properties depending on the parameters passed as arguments\. In the sequel, we show how to implement three*big\-step*777Borrowing static analysis terminology\.operators on intervals\. Each big step operator is the result of iteratively applying one of the*small\-step*operators introduced in Sec\.[3](https://arxiv.org/html/2607.08773#S3), i\.e\.,\{\+,⊔,⊓,/\}\\\{\+,\\sqcup,\\sqcap,/\\\}\.

Input:

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

φI,𝒩\\varphi\_\{I,\\mathcal\{N\}\}, a property to be falsified, and

□:𝕀​\(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\\varphi\_\{I,\\mathcal\{N\}\}
I←I0I\\leftarrow I\_\{0\}

while*∃𝐱′\\exists\\mathbf\{x\}^\{\\prime\}, s\.t\.𝐱′⊧φI,𝒩\\mathbf\{x\}^\{\\prime\}\\models\\varphi\_\{I,\\mathcal\{N\}\}*do

I←I​□​𝐱′I\\leftarrow I~\\square~\\mathbf\{x\}^\{\\prime\}
end while

Algorithm 1GenericTraversal
### 4\.3Minimally Complete Certifications via the⊤\\top–Operator

We begin our discussion on*maximally complete certifications*by defining the⊤\\top\-operator \(see Def\.[6](https://arxiv.org/html/2607.08773#Thmdefinition6)\), between a*compact*decision surface𝒟c⊆𝔽\\mathcal\{D\}\_\{c\}\\subseteq\\mathbb\{F\}and an input point𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, s\.t\.κ​\(𝐱\)=c\\kappa\(\\mathbf\{x\}\)=c\. We see that we can obtain a maximally complete interval certification, w\.r\.t\.𝒟c\\mathcal\{D\}\_\{c\}and𝐱\\mathbf\{x\}as a result of the⊤\\top\-operator\. Moreover, the complete interval certification is*unique*for a particular class, and independent from the choice of the input𝐱\\mathbf\{x\}\. We show this fact in Th\.[6](https://arxiv.org/html/2607.08773#Thmdefinition6)\.

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

Consider a classifierκ:𝔽→𝒞\\kappa\\colon\\mathbb\{F\}\\to\\mathcal\{C\}, an input point𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, s\.t\.κ​\(𝐱\)=c\\kappa\(\\mathbf\{x\}\)=c, and the compact decision surface𝒟c\\mathcal\{D\}\_\{c\}\. With𝒟c⊤𝐱\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}we denote the interval\[−𝐑¯,𝐑¯\]\[\-\\underline\{\\mathbf\{R\}\},\\overline\{\\mathbf\{R\}\}\], s\.t\.,

R¯i=max⁡\{xi−xi′∣xi′≤xi,𝐱′∈𝒟c\},R¯i=max⁡\{xi′−xi​∣xi′\>​xi,𝐱′∈𝒟c\}\.\\underline\{R\}\_\{i\}=\\max\\\{x\_\{i\}\-x^\{\\prime\}\_\{i\}\\mid x\_\{i\}^\{\\prime\}\\leq x\_\{i\},\\ \\mathbf\{x\}^\{\\prime\}\\in\\mathcal\{D\}\_\{c\}\\\},\\ \\overline\{R\}\_\{i\}=\\max\\\{x^\{\\prime\}\_\{i\}\-x\_\{i\}\\mid x\_\{i\}^\{\\prime\}\>x\_\{i\},\\ \\mathbf\{x\}^\{\\prime\}\\in\\mathcal\{D\}\_\{c\}\\\}\.

\(7\)

\{restatable\}

theoremcompletecertification The interval𝒟c⊤𝐱\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}is the*unique*complete certification\. Moreover, for any two𝐱1,𝐱2∈𝒟c\\mathbf\{x\}\_\{1\},\\mathbf\{x\}\_\{2\}\\in\\mathcal\{D\}\_\{c\}, we have𝒟c⊤𝐱1=𝒟c⊤𝐱2\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\_\{1\}=\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\_\{2\}\.

The interval𝒟c⊤𝐱\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}can be computed using Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1), with the parametersI0=\[𝐱,𝐱\]I\_\{0\}=\[\\mathbf\{x\},\\mathbf\{x\}\],φI,𝒩=𝒞I,𝒩\\varphi\_\{I,\\mathcal\{N\}\}=\\mathscr\{C\}\_\{I,\\mathcal\{N\}\}, andI​□​𝐱′=I⊔\[𝐱′−δ​𝟏,𝐱′\+δ​𝟏\]I~\\square~\\mathbf\{x\}^\{\\prime\}=I\\sqcup\[\\mathbf\{x\}^\{\\prime\}\-\\delta\\mathbf\{1\},\\mathbf\{x\}^\{\\prime\}\+\\delta\\mathbf\{1\}\], whereδ\>0\\delta\>0is a precision constant\. Intuitively, with these parameters Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)implements a*bottom\-up*search policy \(BUS\), beginning from the trivial interval\[𝐱,𝐱\]\[\\mathbf\{x\},\\mathbf\{x\}\], proceeding to greater intervals, by including members of the surface𝒟c\\mathcal\{D\}\_\{c\}\. The precision parameterδ\>0\\delta\>0regulates both the outcome’s accuracy and the convergence rate of our algorithm\.\{restatable\}theoremalgomincomplete Consider a compact decision surface𝒟c⊂𝔽\\mathcal\{D\}\_\{c\}\\subset\\mathbb\{F\}\. LetI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}the interval returned by Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)\. It holds that𝒟c⊤𝐱⊆I⊆𝒟c⊤𝐱\+\[−δ​𝟏,δ​𝟏\]\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\\subseteq I\\subseteq\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\+\[\-\\delta\\mathbf\{1\},\\delta\\mathbf\{1\}\]\. Moreover, Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)terminates afterO​\(d⋅𝒜​\(𝒟c⊤𝐱\)/δ\)O\(d\\cdot\\mathcal\{A\}\(\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\)/\\delta\)steps\.

### 4\.4Edge Length Non\-Triviality in Sound Certifications via the⊥\\bot\-Operator

Before we proceed to maximally sound certifications, we present the⊥\\bot\-operator that returns a special kind of sound certifications\. These certifications are guaranteed \(under certain assumptions\) to have strictly positive minimum edge length\. Let𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}be an input point\. We consider the sequence of polyhedral cones888A polyhedral cone is a set of the formC=\{𝐱∈ℝn∣A​𝐱≤𝟎\}C=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{n\}\\mid A\\mathbf\{x\}\\leq\\mathbf\{0\}\\\}, whereA∈ℝm×nA\\in\\mathbb\{R\}^\{m\\times n\}\. We briefly explore the geometry of the cones and their intersections in Appendix[0\.B](https://arxiv.org/html/2607.08773#Pt0.A2)\.⟨V¯i,V¯i⟩\\langle\\underline\{V\}\_\{i\},\\overline\{V\}\_\{i\}\\ranglefor eachi∈\[d\]i\\in\[d\], in eq\. \([8](https://arxiv.org/html/2607.08773#S4.E8)\)\. We haveV¯i∩V¯i=\{𝟎\}\\underline\{V\}\_\{i\}\\cap\\overline\{V\}\_\{i\}=\\\{\\mathbf\{0\}\\\}, for everyi∈\[d\]i\\in\[d\], and\(∪i∈\[d\]V¯i\)∪\(∪i∈\[d\]V¯i\)=ℝd\(\\cup\_\{i\\in\[d\]\}\\underline\{V\}\_\{i\}\)\\cup\(\\cup\_\{i\\in\[d\]\}\\overline\{V\}\_\{i\}\)=\\mathbb\{R\}^\{d\}\. Using the cone partition of eq\. \([8](https://arxiv.org/html/2607.08773#S4.E8)\) we define the⊥\\bot\-operator\.

V¯i=\{𝐱′∈𝔽\|xi′≤xi,∀j∈\[d\]​\|xi′\|≥\|xj′\|\},V¯i=\{𝐱′∈𝔽\|xi′≥xi,∀j∈\[d\]​\|xi′\|≥\|xj′\|\}\.\\begin\{split\}&\\underline\{V\}\_\{i\}=\\left\\\{\\mathbf\{x\}^\{\\prime\}\\in\\mathbb\{F\}~\\big\|~x^\{\\prime\}\_\{i\}\\leq x\_\{i\},\\forall j\\in\[d\]~\|x^\{\\prime\}\_\{i\}\|\\geq\|x^\{\\prime\}\_\{j\}\|\\right\\\},\\\\ &\\overline\{V\}\_\{i\}=\\left\\\{\\mathbf\{x\}^\{\\prime\}\\in\\mathbb\{F\}~\\big\|~x^\{\\prime\}\_\{i\}\\geq x\_\{i\},\\forall j\\in\[d\]~\|x^\{\\prime\}\_\{i\}\|\\geq\|x^\{\\prime\}\_\{j\}\|\\right\\\}\.\\end\{split\}\(8\)
###### Definition 7\(⊥\\bot\-Operator\)

Consider a classifierκ:𝔽→𝒞\\kappa\\colon\\mathbb\{F\}\\to\\mathcal\{C\}, an input point𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, s\.t\.κ​\(𝐱\)=c\\kappa\(\\mathbf\{x\}\)=c, and the compact decision surface𝒟c\\mathcal\{D\}\_\{c\}\. With𝒟c⊥𝐱\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}we denote the interval\[−𝐫¯,𝐫¯\]\[\-\\underline\{\\mathbf\{r\}\},\\overline\{\\mathbf\{r\}\}\], s\.t\.,

r¯i=inf\{xi−xi′∣𝐱′∈Vi¯∖𝒟c\},r¯i=inf\{xi′−xi∣𝐱′∈Vi¯∖𝒟c\}\.\\underline\{r\}\_\{i\}=\\inf\\\{x\_\{i\}\-x^\{\\prime\}\_\{i\}\\mid\\mathbf\{x\}^\{\\prime\}\\in\\underline\{V\_\{i\}\}\\setminus\\mathcal\{D\}\_\{c\}\\\},\\quad\\overline\{r\}\_\{i\}=\\inf\\\{x^\{\\prime\}\_\{i\}\-x\_\{i\}\\mid\\mathbf\{x\}^\{\\prime\}\\in\\overline\{V\_\{i\}\}\\setminus\\mathcal\{D\}\_\{c\}\\\}\.\(9\)

In Prop\.[7](https://arxiv.org/html/2607.08773#Thmdefinition7)we establish the soundness of𝒟c⊥𝐱\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\.

\{restatable\}

propositionpropmaximalsoundapprox Let𝒟c⊆𝔽\\mathcal\{D\}\_\{c\}\\subseteq\\mathbb\{F\}be a compact decision surface, s\.t\.𝐱∈𝒟c\\mathbf\{x\}\\in\\mathcal\{D\}\_\{c\}\. It holds𝒟c⊥𝐱⊆𝒟c\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\\subseteq\\mathcal\{D\}\_\{c\}\.

The interval𝒟c⊥𝐱\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}can be computed using Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1), with the parametersI0=𝔽I\_\{0\}=\\mathbb\{F\},φI,𝒩=𝒮I,𝒩\\varphi\_\{I,\\mathcal\{N\}\}=\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}, andI​□​𝐱′=I​/δ​𝐱′I~\\square~\\mathbf\{x\}^\{\\prime\}=I\\\!\\sideset\{\}\{\{\}\_\{\\delta\}\}\{\\mathop\{\\scalebox\{1\.0\}\[1\.3\]\{/\}\}\}\\mathbf\{x\}^\{\\prime\}, as in Def\.[3](https://arxiv.org/html/2607.08773#Thmdefinition3)\. Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)implements a*top\-down*search policy \(TDS\), beginning from the whole input space𝔽\\mathbb\{F\}, proceeding to smaller intervals, by excluding counterexamples𝐱′∈𝔽∖𝒟c\\mathbf\{x\}^\{\\prime\}\\in\\mathbb\{F\}\\setminus\\mathcal\{D\}\_\{c\}\. Similar to Subsec\.[4\.3](https://arxiv.org/html/2607.08773#S4.SS3), the precision parameterδ\\deltaregulates both the outcome’s accuracy and the convergence rate of our algorithm\.

\{restatable\}

theoremtheoalgomaxsound Consider a compact decision surface𝒟c⊂𝔽\\mathcal\{D\}\_\{c\}\\subset\\mathbb\{F\}\. LetI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}the interval returned by Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)\. It holds that𝒟c⊥𝐱−\[−δ​𝟏,δ​𝟏\]⊆I⊆𝒟c\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\-\[\-\\delta\\mathbf\{1\},\\delta\\mathbf\{1\}\]\\subseteq I\\subseteq\\mathcal\{D\}\_\{c\}\. Moreover, the algorithm terminates afterO​\(d​\[𝒜​\(𝔽\)−𝒜​\(𝒟c⊥𝐱\)\]/δ\)O\(d\[\\mathcal\{A\}\(\\mathbb\{F\}\)\-\\mathcal\{A\}\(\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\)\]/\\delta\)steps\.

The following result guarantees a computed certification with non\-trivial edge lengths, provided that the input belongs to the interior of the decision surface\.\{restatable\}propositionnontrivialitylb If𝐱∈𝒟c∘\\mathbf\{x\}\\in\\mathcal\{D\}^\{\\circ\}\_\{c\}, thenα​\(𝒟c⊥𝐱\)\>0\\alpha\(\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\)\>0\. Recall that, from Prop\.[4](https://arxiv.org/html/2607.08773#Thmdefinition4), several objectives are lower bounded by the minimum edge length\. Thus, the interval𝒟c⊥𝐱\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}provides a non\-trivial lower bound to these quantities, as well\. Notably, Prop\.[7](https://arxiv.org/html/2607.08773#Thmdefinition7)suggests that we can verify a minimum coordinate\-wise perturbation tolerance\. Our experiments in Sec\.[6](https://arxiv.org/html/2607.08773#S6)show that this also holds in practice\. We discuss optimization aspects of interval certifications at the end of this section\.

### 4\.5The Maximal Closure Operator\[I\]\[I\]

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

###### Definition 8\(Maximal Closure Operator\)

Consider a classifierκ:𝔽→𝒞\\kappa\\colon\\mathbb\{F\}\\to\\mathcal\{C\}, an input point𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, s\.t\.κ​\(𝐱\)=c\\kappa\(\\mathbf\{x\}\)=c, and the compact decision surface𝒟c\\mathcal\{D\}\_\{c\}\. LetI⊆𝒟cI\\subseteq\\mathcal\{D\}\_\{c\}be a sound interval certification, s\.t\.𝐱∈I\\mathbf\{x\}\\in I\. With\[I\]\[I\]we denote the*maximal closure*ofII, where,\[I\]=\{J∈𝕀​\(d\)\|𝐱𝔽∣I⊆J⊆𝒟c\}\.\[I\]=\\\{J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\\mid I\\subseteq J\\subseteq\\mathcal\{D\}\_\{c\}\\\}\.

Lem\.[8](https://arxiv.org/html/2607.08773#Thmdefinition8)characterises all the maximally sound interval certifications\. Intuitively, an interval certification is maximally sound if expanding unilaterally any of its coordinates results in the inclusion of a counterexample\. Based on Lem\.[8](https://arxiv.org/html/2607.08773#Thmdefinition8), we present a non\-deterministic algorithm, which*chooses*a coordinate of each of the two interval’s endpoints to expand in each step\. If the expansion leads to a non\-sound certification, the coordinate is discarded, not to be expanded any further\. The pseudocode of the algorithm is presented in App\.[0\.C](https://arxiv.org/html/2607.08773#Pt0.A3), while its correctness is established in Th\.[8](https://arxiv.org/html/2607.08773#Thmdefinition8)\.

\{restatable\}

lemmalemmaximalsoundness Consider a classifierκ:𝔽→𝒞\\kappa\\colon\\mathbb\{F\}\\to\\mathcal\{C\}, an input point𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, s\.t\.κ​\(𝐱\)=c\\kappa\(\\mathbf\{x\}\)=c, and the compact decision surface𝒟c\\mathcal\{D\}\_\{c\}\. Moreover, letI=\[ℓ,𝒖\]⊆𝒟cI=\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\subseteq\\mathcal\{D\}\_\{c\}\. The intervalIIis*maximally sound*, iff for everyi∈\[d\]i\\in\[d\], and everyδ\>0\\delta\>0, we have\[ℓ−δ​𝐞i,𝒖\]∖𝒟c≠∅\[\\boldsymbol\{\\ell\}\-\\delta\\mathbf\{e\}\_\{i\},\\boldsymbol\{u\}\]\\setminus\\mathcal\{D\}\_\{c\}\\neq\\varnothingand\[ℓ,𝒖\+δ​𝐞i\]∖𝒟c≠∅\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\+\\delta\\mathbf\{e\}\_\{i\}\]\\setminus\\mathcal\{D\}\_\{c\}\\neq\\varnothing\.

\{restatable\}

theoremnondetexpand Consider a compact decision surface𝒟c⊂𝔽\\mathcal\{D\}\_\{c\}\\subset\\mathbb\{F\}, and𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}an input\. LetX∈𝕀​\(d\)\|𝐱𝔽X\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}be the trivial sound certificationX=\[𝐱,𝐱\]X=\[\\mathbf\{x\},\\mathbf\{x\}\]\. For every maximally sound intervalI∈\[X\]I\\in\[X\]there is a choice of indices in the operation of Algorithm[3](https://arxiv.org/html/2607.08773#algorithm3), resulting to an intervalJJ, s\.t\.I−\[−δ​𝟏,δ​𝟏\]⊆J⊆II\-\[\-\\delta\\mathbf\{1\},\\delta\\mathbf\{1\}\]\\subseteq J\\subseteq I\. Moreover, suchJJis computed inO​\(d⋅𝒜​\(𝔽\)/δ\)O\(d\\cdot\\mathcal\{A\}\(\\mathbb\{F\}\)/\\delta\)*non\-deterministic*steps\.

### 4\.6The Space of Interval Certifications

We close our study on interval certifications by examining the structure of the interval certifications’ space and how our earlier discussion is reflected in that space\. As we saw in Sec\.[3](https://arxiv.org/html/2607.08773#S3), the structure⟨𝕀​\(d\)\|𝐱𝔽,⊆⟩\\langle\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\},\\subseteq\\rangleforms an*innumerably infinite*lattice\[[30](https://arxiv.org/html/2607.08773#bib.bib82)\], with⊔,⊓\\sqcup,\\sqcapas the join and meet operators respectively\. The*bottom element*of this space is the trivial interval\[𝐱,𝐱\]\[\\mathbf\{x\},\\mathbf\{x\}\]and the top element is the universe𝔽\\mathbb\{F\}\. Consider a compact decision surface𝒟c⊂𝔽\\mathcal\{D\}\_\{c\}\\subset\\mathbb\{F\}, s\.t\.𝐱∈𝒟c\\mathbf\{x\}\\in\\mathcal\{D\}\_\{c\}, i\.e\.κ​\(𝐱\)=c\\kappa\(\\mathbf\{x\}\)=c\. The following \(set\-theoretic\) inequality holds:\[𝐱,𝐱\]⊆𝒟c⊥𝐱⊆𝒟c⊆𝒟c⊤𝐱⊆𝔽\[\\mathbf\{x\},\\mathbf\{x\}\]\\subseteq\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\\subseteq\\mathcal\{D\}\_\{c\}\\subseteq\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\\subseteq\\mathbb\{F\}\. Naturally, every subset of𝒟c⊥𝐱\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}is a sound certification\. The interval𝒟c⊥𝐱\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}is not maximal, but every set in its maximal closure\[𝒟c⊥𝐱\]\[\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\]is\. Moreover,*every*complete certification includes𝒟c⊤𝐱\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\. Fig\.[2](https://arxiv.org/html/2607.08773#S4.F2)illustrates the structure of the⟨𝕀​\(d\)\|𝐱𝔽,⊆⟩\\langle\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\},\\subseteq\\ranglelattice\. Observe that the hierarchy in Fig\.[2](https://arxiv.org/html/2607.08773#S4.F2)collapses when𝒟c\\mathcal\{D\}\_\{c\}is an interval, i\.e\., when𝒟c∈𝕀​\(d\)\|𝐱𝔽\\mathcal\{D\}\_\{c\}\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\. This fact follows from Th\.s[6](https://arxiv.org/html/2607.08773#Thmdefinition6)and[8](https://arxiv.org/html/2607.08773#Thmdefinition8)\.

###### Corollary 1

\[𝒟c⊥𝐱\]=\{𝒟c⊤𝐱\}\[\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\]=\\\{\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\\\}*iff*𝒟c∈𝕀​\(d\)\|𝐱𝔽\\mathcal\{D\}\_\{c\}\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\.

![Refer to caption](https://arxiv.org/html/2607.08773v1/figures/intervals-structure-bw.png)Figure 2:The structure of𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\. We adopt the Hasse diagram convention depicting each element higher from the elements it dominates\.𝒟c\\mathcal\{D\}\_\{c\}is shown in the image with a dashed line, because, in general,𝒟c∉𝕀​\(d\)\|𝐱𝔽\\mathcal\{D\}\_\{c\}\\notin\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, and thus, technically,𝒟\\mathcal\{D\}is not part of the diagram\. Moreover,ω​\(𝒟c⊥𝐱\)≤ω​\(𝒟c\)≤ω​\(𝒟c⊤𝐱\)\\omega\(\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\)\\leq\\omega\(\\mathcal\{D\}\_\{c\}\)\\leq\\omega\(\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\), for an increasing objectiveω​\(⋅\)\\omega\(\\cdot\)\.

## 5Optimization over Interval Certifications

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

1. 1\.ω​\(\[𝐱,𝐱\]\)=0\\omega\(\[\\mathbf\{x\},\\mathbf\{x\}\]\)=0
2. 2\.For everyI1,I2∈𝕀​\(d\)\|𝐱𝔽I\_\{1\},I\_\{2\}\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, ifI1⊆I2I\_\{1\}\\subseteq I\_\{2\}, thenω​\(I1\)≤ω​\(I2\)\\omega\(I\_\{1\}\)\\leq\\omega\(I\_\{2\}\)\.

Note that the objectives of Sec\.[3](https://arxiv.org/html/2607.08773#S3)follow these properties\. In the sequel, we implicitly assume thatω∈\{α,π,v,𝒜\}\\omega\\in\\\{\\alpha,\\pi,v,\\mathcal\{A\}\\\}\. Consider the interval certificationsI,J∈𝕀​\(d\)\|𝐱𝔽I,J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, whereIIis sound, andJJis complete, w\.r\.t\. a decision surfaceDcD\_\{c\}\. For an objective satisfying the above properties, it holdsω​\(I\)≤ω​\(𝒟c\)≤ω​\(J\)\\omega\(I\)\\leq\\omega\(\\mathcal\{D\}\_\{c\}\)\\leq\\omega\(J\)\. Now, consider the following*dual*optimization problems\.

ω¯=max⁡\{ω​\(I\)∣I⊆𝒟c∧I∈𝕀​\(d\)\|𝐱𝔽\},\\displaystyle\\underline\{\\omega\}=\\max\\left\\\{\\omega\(I\)\\mid I\\subseteq\\mathcal\{D\}\_\{c\}\\wedge I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\\right\\\},\(10a\)ω¯=min⁡\{ω​\(I\)∣I⊇𝒟c∧I∈𝕀​\(d\)\|𝐱𝔽\}\.\\displaystyle\\overline\{\\omega\}=\\min\\left\\\{\\omega\(I\)\\mid I\\supseteq\\mathcal\{D\}\_\{c\}\\wedge I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\\right\\\}\.\(10b\)We call eq\. \([10a](https://arxiv.org/html/2607.08773#S5.E10.1)\), theSound Interval Maximization \(SIM\)problem, while eq\. \([10b](https://arxiv.org/html/2607.08773#S5.E10.2)\)Complete Interval Minimization \(CIM\)problem\. Using the⊤\\top\-operator we can*exactly*compute the*optimal*solutionω¯\\overline\{\\omega\}of the complete minimization problem, i\.e\.ω¯=ω​\(𝒟c⊤𝐱\)\\overline\{\\omega\}=\\omega\(\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\), for*any*𝐱∈𝒟c\\mathbf\{x\}\\in\\mathcal\{D\}\_\{c\}\. However, the⊥\\bot\-operator only provides a lower bound to the solution of sound maximization, i\.e\.,ω¯≥ω​\(𝒟c⊥𝐱\)\\underline\{\\omega\}\\geq\\omega\(\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\)\. A better lower bound can be obtained by taking the maximal closure\[𝒟c⊥𝐱\]\[\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\]\. Nevertheless, finding the maximum sound interval certification is computationally intractable\. Subsequently, we discuss the computational hardness of the sound maximization problem\.

### 5\.1On the Intractability of Sound Maximization

Recent results provide evidence on the intractability of sound maximization\. In particular, recall that\[[13](https://arxiv.org/html/2607.08773#bib.bib34)\]establishes the*NP\-completeness*of the MLP verification problem\. Since we use verification oracles, this hardness is inherited to our problem\. Moreover,\[[38](https://arxiv.org/html/2607.08773#bib.bib24)\]demonstrates the*in\-approximability*of sound maximization, even when restricted to uniform interval certifications, i\.e\.,ℓ∞\\ell\_\{\\infty\}\-spheres\. Building on these existing results, we further show that the decision version of theSIMproblem isNP\-hard\. Specifically, even when the verification oracle cost is ignored, the problem admits no polynomial\-time algorithm, unless𝐏=𝐍𝐏\\mathbf\{P\}=\\mathbf\{NP\}\.

\{restatable\}

theoremtheosoundmaxhard Consider a compact decision surface𝒟c\\mathcal\{D\}\_\{c\}and an input point𝐱∈𝒟c\\mathbf\{x\}\\in\\mathcal\{D\}\_\{c\}\. Then, the existence of a sound intervalI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, withI⊆𝒟cI\\subseteq\\mathcal\{D\}\_\{c\}andv​\(I\)≥γv\(I\)\\geq\\gamma,γ\>0\\gamma\>0*cannot*be decided in𝗉𝗈𝗅𝗒​\(d,n,toracle\)\\mathsf\{poly\}\(d,n,t\_\{\\text\{oracle\}\}\)time, unlessP=NP\. In Th\.[5\.1](https://arxiv.org/html/2607.08773#S5.SS1), with𝗉𝗈𝗅𝗒​\(d,n,toracle\)\\mathsf\{poly\}\(d,n,t\_\{\\text\{oracle\}\}\)we denote the set of all polynomials ond,n,toracled,n,t\_\{\\text\{oracle\}\}, wherennis the number of oracle calls, andtoraclet\_\{\\text\{oracle\}\}is the worst\-case time consumed by the soundness verification oracle\. Note that Th\.[5\.1](https://arxiv.org/html/2607.08773#S5.SS1)constitutes a strong intractability result, since it states that the complexity\-significant parameters*cannot*be related polynomially\. In other words, it does not suffice to keep the number of dimensionsddsmall, make few oracle calls \(i\.e\., keepnnsmall\), or implement faster verifiers \(i\.e\., keeptoraclet\_\{\\text\{oracle\}\}small\); to efficiently and optimally solve maximum soundness\. All three parameters must be kept bounded for an optimal sound certification, to be computationally possible\. Thusly, we chose to examine a more efficient*greedy*variant in Sec\.[4](https://arxiv.org/html/2607.08773#S4), based on the exclusion operator in Def\.[3](https://arxiv.org/html/2607.08773#Thmdefinition3)\. Unfortunately, making the optimal decision in every \(small\) step does not imply overall \(big\-step\) optimality\.

The intractability of the maximum soundness problem follows from the intractability of theMaximum Empty Rectangle \(MER\)problem\[[2](https://arxiv.org/html/2607.08773#bib.bib86),[1](https://arxiv.org/html/2607.08773#bib.bib83),[3](https://arxiv.org/html/2607.08773#bib.bib85),[27](https://arxiv.org/html/2607.08773#bib.bib84)\]\. In this problem, we assume a bounding interval𝔽\\mathbb\{F\}and a finite set of*forbidden*pointsℱ⊂𝔽\\mathcal\{F\}\\subset\\mathbb\{F\}\. Our goal is to find an intervalI⊆𝔽I\\subseteq\\mathbb\{F\}, s\.t\.I∩ℱ=∅I\\cap\\mathcal\{F\}=\\varnothing\. Namely, the intervalIIwill exclude all the forbidden points\. Moreover, we requireIIto be the maximum, w\.r\.t\. the volumev​\(⋅\)v\(\\cdot\)\.\[[1](https://arxiv.org/html/2607.08773#bib.bib83)\]prove that this problem isNP\-hard for arbitrary number of dimensions\. However,MERcannot be*directly*reduced toSIM\. Note that inSIM, we require the given input𝐱\\mathbf\{x\}to be*included*in the returned intervalII\. In literature, the latter problem is known as q\-MER\[[10](https://arxiv.org/html/2607.08773#bib.bib87)\], where we demand the maximum empty rectangle to include a query point\. Nevertheless,\[[10](https://arxiv.org/html/2607.08773#bib.bib87)\]does not provide any intractability result\.\[[1](https://arxiv.org/html/2607.08773#bib.bib83)\]proveMER’s intractability, by reducing from theIndependent Set \(IS\)\. The*same*reduction can be applied to show, in Lem\.[5\.1](https://arxiv.org/html/2607.08773#S5.SS1), thatISis*also*reduced to q\-MER, by setting𝐪=𝟎\\mathbf\{q\}=\\mathbf\{0\}\.\{restatable\}lemmalemsoundmaxhard Consider an interval universe𝔽=\[𝐔¯,𝐔¯\]\\mathbb\{F\}=\[\\underline\{\\mathbf\{U\}\},\\overline\{\\mathbf\{U\}\}\]\. Moreover assume a finite set of forbidden pointsℱ⊂𝔽\\mathcal\{F\}\\subset\\mathbb\{F\}, and a query point𝐪∈𝔽∖ℱ\\mathbf\{q\}\\in\\mathbb\{F\}\\setminus\\mathcal\{F\}\. The existence of an intervalI⊆𝔽I\\subseteq\\mathbb\{F\}, s\.t\.𝐪∈I\\mathbf\{q\}\\in I,I∩ℱ=∅I\\cap\\mathcal\{F\}=\\varnothing, andv​\(I\)≥γv\(I\)\\geq\\gamma, for givenγ\>0\\gamma\>0,*cannot*be decided in polynomial time, unlessP=NP\. Th\.[5\.1](https://arxiv.org/html/2607.08773#S5.SS1)is derived from Lem\.[5\.1](https://arxiv.org/html/2607.08773#S5.SS1)by considering asℱ\\mathcal\{F\}the set of*counterexamples*returned by the soundness verification oracle𝒮I,𝒩\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}\. Finally, from Prop\.[4](https://arxiv.org/html/2607.08773#Thmdefinition4)for each interval it holdsv​\(I\)d≥α​\(I\)\\sqrt\[d\]\{v\(I\)\}\\geq\\alpha\(I\), therefore Lem\.[5\.1](https://arxiv.org/html/2607.08773#S5.SS1)and Th\.[5\.1](https://arxiv.org/html/2607.08773#S5.SS1)can be modified to useα​\(⋅\)\\alpha\(\\cdot\), as the desired targeted objective\.

### 5\.2Sound Maximization on Uniform Intervals

We call theSIMproblem, when constrained to uniform intervals \(ℓ∞\\ell\_\{\\infty\}\-spheres\)𝔹\\mathbb\{B\}\-SIM\. For disambiguation, we call𝕀\\mathbb\{I\}\-SIM, theSIMproblem for general intervals\. As we mentioned earlier,𝔹\\mathbb\{B\}\-SIM’s intractability persists, even if constrained to uniform intervals,\[[13](https://arxiv.org/html/2607.08773#bib.bib34),[38](https://arxiv.org/html/2607.08773#bib.bib24)\]\. However, we*can*compute an optimal solution in𝗉𝗈𝗅𝗒​\(d,n,toracle\)\\mathsf\{poly\}\(d,n,t\_\{\\text\{oracle\}\}\)time\. In particular, we can compute a maximum sound uniform intervalB=\[𝐱−ρ​𝟏,𝐱\+ρ​𝟏\]B=\[\\mathbf\{x\}\-\\rho\\mathbf\{1\},\\mathbf\{x\}\+\\rho\\mathbf\{1\}\], s\.t\.v​\(B\)≥γ,γ\>0v\(B\)\\geq\\gamma,\\gamma\>0, inlog⁡\(𝒜​\(𝔽/δ\)\)⋅toracle\\log\(\\mathcal\{A\}\(\\mathbb\{F\}/\\delta\)\)\\cdot t\_\{\\text\{oracle\}\}time\. We find the uniform interval’s radiusρ\>0\\rho\>0, by applying*dichotomic search*on the real interval\[0,𝒜​\(𝔽\)\]\[0,\\mathcal\{A\}\(\\mathbb\{F\}\)\]\. Formally, this is provided by the following result\.\{restatable\}theoremsoundmaxcyclic Consider a compact decision surface𝒟c\\mathcal\{D\}\_\{c\}and an input point𝐱∈𝒟c\\mathbf\{x\}\\in\\mathcal\{D\}\_\{c\}\. Then, the existence of a sound uniform intervalB=\[𝐱−ρ​𝟏,𝐱\+ρ​𝟏\]B=\[\\mathbf\{x\}\-\\rho\\mathbf\{1\},\\mathbf\{x\}\+\\rho\\mathbf\{1\}\], with𝐱∈B\\mathbf\{x\}\\in B,B⊆𝒟cB\\subseteq\\mathcal\{D\}\_\{c\}andv​\(B\)≥γv\(B\)\\geq\\gamma,γ\>0\\gamma\>0*can*be decided in polynomial verification oracle calls\. We close our discussion on𝔹\\mathbb\{B\}\-SIM’s complexity, with some remarks on its relation withMER\. In particular,\[[1](https://arxiv.org/html/2607.08773#bib.bib83)\]discusses a variant ofMER, restricted to axis\-aligned*hyper\-cubes*, calledMaximum Empty Square \(MES\)\. They also show thatMESisNP\-hard, for an arbitrary number of dimensions\. However, in𝔹\\mathbb\{B\}\-SIM, we are*given*the center of theℓ∞\\ell\_\{\\infty\}\-sphere\. Following our terminology thus far, we would call the latter problem q\-MES\. Observe that despiteMERand q\-MERbeing computationally equal \(bothNP\-hard\), q\-MESis*properly*easier thanMES\. Indeed, the dichotomic search method we described in Th\.[5\.2](https://arxiv.org/html/2607.08773#S5.SS2)would also work for q\-MES\.

### 5\.3The Space of Uniform Interval Certifications

Let𝔹​\(d\)\|𝐱𝔽\\mathbb\{B\}\(d\)\|\_\{\\mathbf\{x\}\}^\{\\mathbb\{F\}\}be the set of all uniform intervals centered at𝐱\\mathbf\{x\}\. First we observe that𝔹​\(d\)\|𝐱𝔽⊂𝕀​\(d\)\|𝐱𝔽\\mathbb\{B\}\(d\)\|\_\{\\mathbf\{x\}\}^\{\\mathbb\{F\}\}\\subset\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, since every uniform interval, is also an interval containing𝐱\\mathbf\{x\}\. However, the opposite does*not*hold\. Moreover,𝔹​\(d\)\|𝐱𝔽\\mathbb\{B\}\(d\)\|\_\{\\mathbf\{x\}\}^\{\\mathbb\{F\}\}exhibits a more straightforward structure than𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\. Indeed,𝔹​\(d\)\|𝐱𝔽\\mathbb\{B\}\(d\)\|\_\{\\mathbf\{x\}\}^\{\\mathbb\{F\}\}form a*totally ordered set*, under set inclusion\. Namely, for everyB1,B2∈𝔹​\(d\)\|𝐱𝔽B\_\{1\},B\_\{2\}\\in\\mathbb\{B\}\(d\)\|\_\{\\mathbf\{x\}\}^\{\\mathbb\{F\}\}, we haveB1⊆B2B\_\{1\}\\subseteq B\_\{2\}, iffρ1≤ρ2\\rho\_\{1\}\\leq\\rho\_\{2\}, whereρ1,ρ2\\rho\_\{1\},\\rho\_\{2\}the radii ofB1,B2B\_\{1\},B\_\{2\}, respectively\. Intuitively, this simpler structure is the reason for the differences in computational hardness between the two problems\. Nevertheless, the richer solution space of𝕀​\(d\)\|𝐱𝔽\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}provides non\-trivial certifications to a*strictly*larger class of inputs\.

For uniform intervals we can define⊥𝔹,⊤𝔹\\bot\_\{\\mathbb\{B\}\},\\top\_\{\\mathbb\{B\}\}\-operations for𝔹​\(d\)\|𝐱𝔽\\mathbb\{B\}\(d\)\|\_\{\\mathbf\{x\}\}^\{\\mathbb\{F\}\}, analogous to Sec\.[4](https://arxiv.org/html/2607.08773#S4)\. To that end, consider a compact decision surface𝒟c⊆𝔽\\mathcal\{D\}\_\{c\}\\subseteq\\mathbb\{F\}and an input𝐱∈𝒟c\\mathbf\{x\}\\in\\mathcal\{D\}\_\{c\}\. Letρ¯\>0\\underline\{\\rho\}\>0be the*smaller*distance between𝐱\\mathbf\{x\}and a counterexample𝐱′∉𝒟c\\mathbf\{x\}^\{\\prime\}\\notin\\mathcal\{D\}\_\{c\}, andρ¯\>0\\overline\{\\rho\}\>0the*greatest*distance between𝐱\\mathbf\{x\}and another point𝐱′′∈𝒟c\\mathbf\{x\}^\{\\prime\\prime\}\\in\\mathcal\{D\}\_\{c\}\. Namely,

ρ¯=inf\{‖𝐱−𝐱′‖∞∣𝐱′∉𝒟c\},ρ¯=sup\{‖𝐱−𝐱′′‖∞∣𝐱′′∈𝒟c\}\\underline\{\\rho\}=\\inf\\\{\\\|\\mathbf\{x\}\-\\mathbf\{x\}^\{\\prime\}\\\|\_\{\\infty\}\\mid\\mathbf\{x\}^\{\\prime\}\\notin\\mathcal\{D\}\_\{c\}\\\},~~\\overline\{\\rho\}=\\sup\\\{\\\|\\mathbf\{x\}\-\\mathbf\{x\}^\{\\prime\\prime\}\\\|\_\{\\infty\}\\mid\\mathbf\{x\}^\{\\prime\\prime\}\\in\\mathcal\{D\}\_\{c\}\\\}\(11\)We define𝒟c⊥𝔹𝐱=\[𝐱−ρ¯​𝟏,𝐱\+ρ¯​𝟏\]\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{B\}\}\\mathbf\{x\}=\[\\mathbf\{x\}\-\\underline\{\\rho\}\\mathbf\{1\},\\mathbf\{x\}\+\\underline\{\\rho\}\\mathbf\{1\}\]and𝒟c⊤𝔹𝐱=\[𝐱−ρ¯​𝟏,𝐱\+ρ¯​𝟏\]\\mathcal\{D\}\_\{c\}\\top\_\{\\mathbb\{B\}\}\\mathbf\{x\}=\[\\mathbf\{x\}\-\\overline\{\\rho\}\\mathbf\{1\},\\mathbf\{x\}\+\\overline\{\\rho\}\\mathbf\{1\}\]\. The following \(set\-theoretic\) inequality relates the⊥,⊤\\bot,\\top\-operators in uniform and general intervals\. For disambiguation, here we denote these operations with⊥𝕀,⊤𝕀\\bot\_\{\\mathbb\{I\}\},\\top\_\{\\mathbb\{I\}\}for general intervals\.

𝒟c⊥𝔹𝐱⊆𝒟c⊥𝕀𝐱⊆𝒟c⊆𝒟c⊤𝕀𝐱⊆𝒟⊤𝔹𝐱\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{B\}\}\\mathbf\{x\}\\subseteq\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{I\}\}\\mathbf\{x\}\\subseteq\\mathcal\{D\}\_\{c\}\\subseteq\\mathcal\{D\}\_\{c\}\\top\_\{\\mathbb\{I\}\}\\mathbf\{x\}\\subseteq\\mathcal\{D\}\\top\_\{\\mathbb\{B\}\}\\mathbf\{x\}\(12\)Noteworthy, for uniform intervals we have𝒟c⊥𝔹𝐱=\[𝒟c⊥𝔹𝐱\]\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{B\}\}\\mathbf\{x\}=\[\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{B\}\}\\mathbf\{x\}\]\. Since an objectiveω​\(⋅\)\\omega\(\\cdot\)respects set inclusion,ω​\(𝒟c⊥𝔹𝐱\)≤ω​\(𝒟c⊥𝕀𝐱\)≤ω​\(𝒟c\)≤ω​\(𝒟c⊤𝕀𝐱\)≤ω​\(𝒟⊤𝔹𝐱\)\\omega\(\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{B\}\}\\mathbf\{x\}\)\\leq\\omega\(\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{I\}\}\\mathbf\{x\}\)\\leq\\omega\(\\mathcal\{D\}\_\{c\}\)\\leq\\omega\(\\mathcal\{D\}\_\{c\}\\top\_\{\\mathbb\{I\}\}\\mathbf\{x\}\)\\leq\\omega\(\\mathcal\{D\}\\top\_\{\\mathbb\{B\}\}\\mathbf\{x\}\)\. In Sec\.[6](https://arxiv.org/html/2607.08773#S6), we implement the⊥,⊤\\bot,\\top\-operators both for uniform and general interval certifications\. We observe that the minimum edge length of a general interval certification is, on average, about twice greater than the same objective in uniform intervals\.

## 6Implementation

Here, we examine the implementation and practical implications of the theoretical framework discussed earlier\. We developed the open source systemParallele\- pipedoNN\. This system implements the operators discussed in Sec\.[3](https://arxiv.org/html/2607.08773#S3),[4](https://arxiv.org/html/2607.08773#S4), and Appendix[0\.C](https://arxiv.org/html/2607.08773#Pt0.A3)\. In particular, Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)withBUSpolicy implements the⊤\\top\-operator, while the⊥\\bot\-operator is implemented in the Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)withTDSpolicy method\. Recall thatBUSpolicy is obtained by applying the parametersI0=\[𝐱,𝐱\]I\_\{0\}=\[\\mathbf\{x\},\\mathbf\{x\}\],φI,𝒩=𝒞I,N\\varphi\_\{I,\\mathcal\{N\}\}=\\mathscr\{C\}\_\{I,N\}, and□=⊔\\square=\\sqcup\. On the other hand,TDSis obtained for the parametersI0=𝔽I\_\{0\}=\\mathbb\{F\},φI,𝒩=𝒮I,N\\varphi\_\{I,\\mathcal\{N\}\}=\\mathscr\{S\}\_\{I,N\}, and□=/\\square=/\. Moreover, since Algorithm[3](https://arxiv.org/html/2607.08773#algorithm3)is non\-deterministic, we implemented a deterministicSequential Dichotomic Expansion \(SDE\)method, presented in Appendix[0\.C](https://arxiv.org/html/2607.08773#Pt0.A3)\.SDEensures maximality\. Additionally, we include in our analysis evaluations regarding Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)with eitherBUSorTDSpolicies for the case of uniform intervals\. We denote these special cases of the algorithms as𝔹\\mathbb\{B\}\-BUSand𝔹\\mathbb\{B\}\-TDS, respectively\.

In Tbl\.[2](https://arxiv.org/html/2607.08773#S6.T2), we overview the presented algorithms\. For minimal complete certifications, we presented two algorithms,BUSand𝔹\\mathbb\{B\}\-BUS, for general and uniform intervals, respectively\. Recall that the minimal complete uniform interval certification is*not*complete\.SDEcomputes maximally sound interval certifications\.TDSensures voluminosity, under the assumption of Prop\.[7](https://arxiv.org/html/2607.08773#Thmdefinition7)\. Combining these two practices, we have a voluminous and maximally sound certification\. Finally,𝔹\\mathbb\{B\}\-TDScomputes maximally complete certifications for uniform intervals\. Naturally,𝔹\\mathbb\{B\}\-TDSalso ensures voluminosity, under the same conditions of Prop\.[7](https://arxiv.org/html/2607.08773#Thmdefinition7)\. For complete certifications, voluminosity is irrelevant\. A complete interval will always have volume if𝒟c\\mathcal\{D\}\_\{c\}has volume\. Our experiments provide counterexamples for voluminosity inSDE\.

AlgorithmOperatorSound/CompleteMin\./Max\.Vol\.ComplexityTheoryBUS𝒟c⊤𝕀𝐱\\mathcal\{D\}\_\{c\}\\top\_\{\\mathbb\{I\}\}\\mathbf\{x\}CMin\.–O​\[d⋅𝒜​\(𝔽\)/δ\]O\[d\\cdot\\mathcal\{A\}\(\\mathbb\{F\}\)/\\delta\]Th\.[6](https://arxiv.org/html/2607.08773#Thmdefinition6)TDS𝒟c⊥𝕀𝐱\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{I\}\}\\mathbf\{x\}S–\(✓\)O​\[d⋅𝒜​\(𝔽\)/δ\]O\[d\\cdot\\mathcal\{A\}\(\\mathbb\{F\}\)/\\delta\]Th\.[7](https://arxiv.org/html/2607.08773#Thmdefinition7)SDE\[I\]\[I\]SMax\.✗O​\[d⋅log⁡\(𝒜​\(𝔽\)\)\]O\[d\\cdot\\log\(\\mathcal\{A\}\(\\mathbb\{F\}\)\)\]Prop\.[1](https://arxiv.org/html/2607.08773#Thmproposition1)TDS\+SDE\[𝒟c⊥𝕀𝐱\]\[\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{I\}\}\\mathbf\{x\}\]SMax\.\(✓\)O​\[d⋅𝒜​\(𝔽\)/δ\]O\[d\\cdot\\mathcal\{A\}\(\\mathbb\{F\}\)/\\delta\]Th\.[7](https://arxiv.org/html/2607.08773#Thmdefinition7), Prop\.[1](https://arxiv.org/html/2607.08773#Thmproposition1)𝔹\\mathbb\{B\}–BUS𝒟c⊤𝔹𝐱\\mathcal\{D\}\_\{c\}\\top\_\{\\mathbb\{B\}\}\\mathbf\{x\}CMin\.–O​\[log⁡\(𝒜​\(𝔽\)\)\]O\[\\log\(\\mathcal\{A\}\(\\mathbb\{F\}\)\)\]Th\.[5\.2](https://arxiv.org/html/2607.08773#S5.SS2)𝔹\\mathbb\{B\}–TDS𝒟c⊥𝔹𝐱\\mathcal\{D\}\_\{c\}\\bot\_\{\\mathbb\{B\}\}\\mathbf\{x\}SMax\.\(✓\)O​\[log⁡\(𝒜​\(𝔽\)\)\]O\[\\log\(\\mathcal\{A\}\(\\mathbb\{F\}\)\)\]Th\.[5\.2](https://arxiv.org/html/2607.08773#S5.SS2)

Table 2:Algorithms & Properties\. With “\(✓\)” we denote a property that is proven to hold \(under the assumption𝐱∈𝒟c∘\\mathbf\{x\}\\in\\mathcal\{D\}\_\{c\}^\{\\circ\}\)\. With “✗” we denote a disproved property\. With “–” we denote irrelevant properties\. In the rightmost column, we refer to the theoretical result \(theorem or proposition\) proving the algorithm’s properties\. In𝔹\\mathbb\{B\}\-BUS, we support our claim using the*proof*of Th\.[5\.2](https://arxiv.org/html/2607.08773#S5.SS2)\. The complexity/correctness proofs of𝔹\\mathbb\{B\}\-BUSand𝔹\\mathbb\{B\}\-TDSare practically identical\. For𝔹\\mathbb\{B\}\-BUS,𝔹\\mathbb\{B\}\-TDSmaximality/minimality is examined for uniform intervals\.### 6\.1Experimental Evaluation

Below we describe our experimental setup\.

Hardware\.The experiments were performed in*parallel*on an Ubuntu 18\.04 machine, with Intel Xeon E5\-2640 v4 CPU, at 2\.394GHz, with 38 cores, with 128GB RAM\. The experiments ran in parallel, utilizing 35 cores\.

Software Dependencies\.Algorithms’ Parameters\.We evaluated all the algorithms of Tbl\.[2](https://arxiv.org/html/2607.08773#S6.T2)using the same parameters\. We set the precision constantδ\\deltato0\.10\.1\. We also set a*timeout*variable to 1 hour\. For TDS\+SDE the timeout is 2 hours, 1 hour for each component\. The maximum number of iterations was set to 10,000\.

Training Dataset\.We use 2 datasets, namely MNIST\[[5](https://arxiv.org/html/2607.08773#bib.bib41)\]and Fashion MNIST\[[35](https://arxiv.org/html/2607.08773#bib.bib42)\]\. Both datasets consist of 28×\\times28, grayscale images, belonging to 10 classes\. However, Fashion MNIST images are*significantly*more complex than MNIST\.

Neural Networks\.We consider the following MLP architecture\. applied our algorithms to 2 MLPs, of the same architecture, trained on the MNIST and Fashion MNIST datasets, respectively\. Including the input and output layers, we have the architecture⟨784,32,10,10⟩\\langle 784,32,10,10\\rangle, w\.r\.t\. Def\.[1](https://arxiv.org/html/2607.08773#Thmdefinition1)\. This corresponds to 25,450 trainable parameters\. For training, we used the Adam\[[16](https://arxiv.org/html/2607.08773#bib.bib33)\]algorithm, Glorot\[[8](https://arxiv.org/html/2607.08773#bib.bib32)\]weight initialization, and the Categorical Crossentropy loss\. By training on the 2 datasets above, this results in two MLPs, achieving94%94\\%and82%82\\%test\-set accuracy for the MNIST and Fashion MNIST, respectively\.

Inputs\.For each MLP, we randomly choose 5 images of the 10 classes of the test set \(a total of 50 images per MLP\)\.

DatasetAlgorithmAverageTimesec\./min\.\# Verif\. CallsMin\. EdgeLen\.α​\(⋅\)\\alpha\(\\cdot\)TimeoutsMNISTBUS38\.5438\.54m2085\.730\.990TDS51\.1351\.13m3753\.020\.132828SDE32\.7832\.78m2963\.860\.01313TDS\+SDE\+42\.04\+42\.04m\+1030\.550\.1325𝔹\\mathbb\{B\}–BUS3\.923\.92s40\.940𝔹\\mathbb\{B\}–TDS21\.0621\.06s40\.070FashionMNISTBUS22\.92m1235\.260\.10TDS50\.17m3272\.760\.1832SDE22\.82m3469\.480\.03TDS\+SDE\+23\.91m\+1374\.450\.181𝔹\\mathbb\{B\}–BUS3\.5s40\.940𝔹\\mathbb\{B\}–TDS5\.15s40\.120

Table 3:Experimental evaluation on the MNIST and Fashion MNIST datasets\.Tbl\.[3](https://arxiv.org/html/2607.08773#S6.T3)reports descriptive statistics on the CPU time, the number of verification oracle calls, and the interval’s minimum edge lengthα​\(⋅\)\\alpha\(\\cdot\)\. We evaluate all six algorithms presented in this paper on both datasets\. Overall, the empirical results align with our theoretical analysis\. In particular,𝔹\\mathbb\{B\}\-BUSand𝔹\\mathbb\{B\}\-TDSare approximately an order of magnitude faster than their general\-intervals counterpart, as expected, since they do*not*scale with the input dimension\. This speed\-up, however, comes at a cost, namely,𝔹\\mathbb\{B\}\-TDSattains only about half of the minimum edge length achieved byTDS\(or roughly two\-thirds on Fashion\-MNIST\)\. Finally, we observe that the Fashion MNIST MLP appears, on average, more robust that the MNIST MLP, despite achieving lower classification accuracy\. This is consistent with prior findings, obtained via different methodologies, on the robustness\-accuracy trade\-off\[[22](https://arxiv.org/html/2607.08773#bib.bib25),[36](https://arxiv.org/html/2607.08773#bib.bib26),[32](https://arxiv.org/html/2607.08773#bib.bib27),[28](https://arxiv.org/html/2607.08773#bib.bib28)\]\. More detailed statistical results are provided in Appendix[0\.D](https://arxiv.org/html/2607.08773#Pt0.A4)\.

## 7Conclusions & Future Work

This work develops a framework for computing maximally sound and minimally complete interval certifications for MLPs\. In Sec\.[4](https://arxiv.org/html/2607.08773#S4), we explore the interval certifications lattice, defining the⊤,⊥,\[⋅\]\\top,\\bot,\[\\cdot\]operators\. We develop algorithms that guarantee minimum completeness \(Th\.[6](https://arxiv.org/html/2607.08773#Thmdefinition6)\) and maximal soundness \(Th\.[7](https://arxiv.org/html/2607.08773#Thmdefinition7),[8](https://arxiv.org/html/2607.08773#Thmdefinition8)\)\. In Sec\.[5](https://arxiv.org/html/2607.08773#S5), we study optimization on interval certifications\. We observe intriguing asymmetries\. The minimum complete certification can be computed in polynomial oracle calls\. However, we extend previous results, by showing a stronger intractability result for sound maximization \(Th\.[5\.1](https://arxiv.org/html/2607.08773#S5.SS1)\)\. Nevertheless, when optimization problems, are restricted to uniform intervals \(ℓ∞\\ell\_\{\\infty\}–spheres\) become solvable in*logarithmic*number of oracle calls\. Finally, we implement our theoretical insights in theParallelelpipedoNNsystem, \(Sec\.[6](https://arxiv.org/html/2607.08773#S6)\), which we evaluate on MNIST and Fashion MNIST\. As future work, we plan to extend our analysis to more general*polyhedral*certifications\.

## References

- \[1\]J\. Backer and J\. M\. Keil\(2010\)The mono\- and bichromatic empty rectangle and square problems in all dimensions\.InLATIN,A\. López\-Ortiz \(Ed\.\),Cited by:[§5\.1](https://arxiv.org/html/2607.08773#S5.SS1.p3.22),[§5\.2](https://arxiv.org/html/2607.08773#S5.SS2.p1.20),[§0\.A\.3](https://arxiv.org/html/2607.08773#Thmproofx11.p1.29)\.
- \[2\]T\. M\. Chan\(2023\)Faster algorithms for largest empty rectangles and boxes\.Discret\. Comput\. Geom\.\.Cited by:[§5\.1](https://arxiv.org/html/2607.08773#S5.SS1.p3.22)\.
- \[3\]B\. Chazelle, R\. L\. \(\. D\. III, and D\. T\. Lee\(1986\)Computing the largest empty rectangle\.SIAM J\. Comput\.\.Cited by:[§5\.1](https://arxiv.org/html/2607.08773#S5.SS1.p3.22)\.
- \[4\]DeepSeek\-AI, :, X\. Bi, D\. Chen, G\. Chen, S\. Chen, D\. Dai, C\. Deng, H\. Ding, K\. Dong, Q\. Du, Z\. Fu, H\. Gao, K\. Gao, W\. Gao, R\. Ge, K\. Guan, D\. Guo, J\. Guo, G\. Hao, Z\. Hao, Y\. He, W\. Hu, P\. Huang, E\. Li, G\. Li, J\. Li, Y\. Li, Y\. K\. Li, W\. Liang, F\. Lin, A\. X\. Liu, B\. Liu, W\. Liu, X\. Liu, X\. Liu, Y\. Liu, H\. Lu, S\. Lu, F\. Luo, S\. Ma, X\. Nie, T\. Pei, Y\. Piao, J\. Qiu, H\. Qu, T\. Ren, Z\. Ren, C\. Ruan, Z\. Sha, Z\. Shao, J\. Song, X\. Su, J\. Sun, Y\. Sun, M\. Tang, B\. Wang, P\. Wang, S\. Wang, Y\. Wang, Y\. Wang, T\. Wu, Y\. Wu, X\. Xie, Z\. Xie, Z\. Xie, Y\. Xiong, H\. Xu, R\. X\. Xu, Y\. Xu, D\. Yang, Y\. You, S\. Yu, X\. Yu, B\. Zhang, H\. Zhang, L\. Zhang, L\. Zhang, M\. Zhang, M\. Zhang, W\. Zhang, Y\. Zhang, C\. Zhao, Y\. Zhao, S\. Zhou, S\. Zhou, Q\. Zhu, and Y\. Zou\(2024\)DeepSeek llm: scaling open\-source language models with longtermism\.Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p1.1)\.
- \[5\]L\. Deng\(2012\)The mnist database of handwritten digit images for machine learning research\.IEEE Signal Processing Magazine\.Cited by:[item Training Dataset\.](https://arxiv.org/html/2607.08773#S6.I1.ix4.p1.1)\.
- \[6\]R\. Ehlers\(2017\)Formal verification of piece\-wise linear feed\-forward neural networks\.InATVA,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p2.1)\.
- \[7\]K\. Fukushima\(1969\)Visual feature extraction by a multilayered network of analog threshold elements\.IEEE TSSC\.Cited by:[§2](https://arxiv.org/html/2607.08773#S2.SS0.SSS0.Px2.p1.7)\.
- \[8\]X\. Glorot and Y\. Bengio\(2010\)Understanding the difficulty of training deep feedforward neural networks\.InAISTATS,JMLR Proceedings\.Cited by:[item Neural Networks\.](https://arxiv.org/html/2607.08773#S6.I1.ix5.p1.3)\.
- \[9\]I\. J\. Goodfellow, J\. Shlens, and C\. Szegedy\(2015\)Explaining and harnessing adversarial examples\.InICLR,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p1.1),[§1](https://arxiv.org/html/2607.08773#S1.p2.1)\.
- \[10\]G\. Gutiérrez and J\. R\. Paramá\(2012\)Finding the largest empty rectangle containing only a query point in large multidimensional databases\.InSSDBM,A\. Ailamaki and S\. Bowers \(Eds\.\),Lecture Notes in Computer Science\.Cited by:[§5\.1](https://arxiv.org/html/2607.08773#S5.SS1.p3.22)\.
- \[11\]Y\. Izza, A\. Ignatiev, P\. J\. Stuckey, and J\. Marques\-Silva\(2024\)Delivering inflated explanations\.InAAAI,Cited by:[footnote 14](https://arxiv.org/html/2607.08773#footnote14)\.
- \[12\]A\. Kabaha and D\. Drachsler\-Cohen\(2023\)Maximal robust neural network specifications via oracle\-guided numerical optimization\.InVMCAI,C\. Dragoi, M\. Emmi, and J\. Wang \(Eds\.\),Cited by:[Table 1](https://arxiv.org/html/2607.08773#S1.T1),[Table 1](https://arxiv.org/html/2607.08773#S1.T1.4.4.4.4.4.2),[§1](https://arxiv.org/html/2607.08773#S1.p2.1),[§1](https://arxiv.org/html/2607.08773#S1.p4.9)\.
- \[13\]G\. Katz, C\. W\. Barrett, D\. L\. Dill, K\. Julian, and M\. J\. Kochenderfer\(2017\)Reluplex: an efficient SMT solver for verifying deep neural networks\.InCAV,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p3.5),[§2](https://arxiv.org/html/2607.08773#S2.SS0.SSS0.Px3.p2.9),[§4\.1](https://arxiv.org/html/2607.08773#S4.SS1.p3.9),[§5\.1](https://arxiv.org/html/2607.08773#S5.SS1.p1.2),[§5\.2](https://arxiv.org/html/2607.08773#S5.SS2.p1.20)\.
- \[14\]G\. Katz, C\. W\. Barrett, D\. L\. Dill, K\. Julian, and M\. J\. Kochenderfer\(2022\)Reluplex: a calculus for reasoning about deep neural networks\.Formal Methods Syst\. Des\.\.Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p3.5)\.
- \[15\]G\. Katz, D\. A\. Huang, D\. Ibeling, K\. Julian, C\. Lazarus, R\. Lim, P\. Shah, S\. Thakoor, H\. Wu, A\. Zeljic, D\. L\. Dill, M\. J\. Kochenderfer, and C\. W\. Barrett\(2019\)The marabou framework for verification and analysis of deep neural networks\.InCAV,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p3.5),[§2](https://arxiv.org/html/2607.08773#S2.SS0.SSS0.Px3.p2.9),[§4\.1](https://arxiv.org/html/2607.08773#S4.SS1.p1.1)\.
- \[16\]D\. P\. Kingma and J\. Ba\(2015\)Adam: A method for stochastic optimization\.InICLR,Cited by:[item Neural Networks\.](https://arxiv.org/html/2607.08773#S6.I1.ix5.p1.3)\.
- \[17\]C\. Li, S\. Ji, H\. Weng, B\. Li, J\. Shi, R\. Beyah, S\. Guo, Z\. Wang, and T\. Wang\(2022\)Towards certifying the asymmetric robustness for neural networks: quantification and applications\.IEEE TDSC\.Cited by:[Table 1](https://arxiv.org/html/2607.08773#S1.T1.3.3.3.3.3.2),[§1](https://arxiv.org/html/2607.08773#S1.p2.1),[§1](https://arxiv.org/html/2607.08773#S1.p4.9),[§1](https://arxiv.org/html/2607.08773#S1.p5.1)\.
- \[18\]D\. Li, P\. Auerbach, and O\. Okhrin\(2025\)Autonomous driving small\-scale cars: a survey of recent development\.IEEE Transactions on Intelligent Transportation Systems\.Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p1.1)\.
- \[19\]C\. Liu, R\. Tomioka, and V\. Cevher\(2019\)On certifying non\-uniform bounds against adversarial attacks\.InICML,Cited by:[Table 1](https://arxiv.org/html/2607.08773#S1.T1.2.2.2.2.2.2),[§1](https://arxiv.org/html/2607.08773#S1.p2.1),[§1](https://arxiv.org/html/2607.08773#S1.p4.9),[§1](https://arxiv.org/html/2607.08773#S1.p5.1)\.
- \[20\]A\. Lomuscio and L\. Maganti\(2017\)An approach to reachability analysis for feed\-forward relu neural networks\.CoRR\.Cited by:[footnote 2](https://arxiv.org/html/2607.08773#footnote2)\.
- \[21\]F\. Ma, R\. Chitta, J\. Zhou, Q\. You, T\. Sun, and J\. Gao\(2017\)Dipole: diagnosis prediction in healthcare via attention\-based bidirectional recurrent neural networks\.InICKDDM,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p1.1)\.
- \[22\]A\. Madry, A\. Makelov, L\. Schmidt, D\. Tsipras, and A\. Vladu\(2018\)Towards deep learning models resistant to adversarial attacks\.InICLR,Cited by:[§6\.1](https://arxiv.org/html/2607.08773#S6.SS1.p3.4)\.
- \[23\]A\. Madry, A\. Makelov, L\. Schmidt, D\. Tsipras, and A\. Vladu\(2018\)Towards deep learning models resistant to adversarial attacks\.InICLR,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p2.1)\.
- \[24\]M\. H\. Meng, G\. Bai, S\. G\. Teo, Z\. Hou, Y\. Xiao, Y\. Lin, and J\. S\. Dong\(2022\)Adversarial robustness of deep neural networks: a survey from a formal verification perspective\.IEEE TDSC\.Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p1.1),[footnote 2](https://arxiv.org/html/2607.08773#footnote2)\.
- \[25\]M\. Mirman, M\. Baader, and M\. T\. Vechev\(2022\)The fundamental limits of neural networks for interval certified robustness\.Trans\. Mach\. Learn\. Res\.\.Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p2.1)\.
- \[26\]R\. E\. Moore, R\. B\. Kearfott, and M\. J\. Cloud\(2009\)Introduction to interval analysis\.SIAM\.Cited by:[§3](https://arxiv.org/html/2607.08773#S3.p1.8)\.
- \[27\]A\. Naamad, D\. T\. Lee, and W\. Hsu\(1984\)On the maximum empty rectangle problem\.Discrete Applied Mathematics\.Cited by:[§5\.1](https://arxiv.org/html/2607.08773#S5.SS1.p3.22)\.
- \[28\]A\. Raghunathan, S\. M\. Xie, F\. Yang, J\. C\. Duchi, and P\. Liang\(2020\)Understanding and mitigating the tradeoff between robustness and accuracy\.InICML,Proceedings of Machine Learning Research\.Cited by:[§6\.1](https://arxiv.org/html/2607.08773#S6.SS1.p3.4)\.
- \[29\]H\. Salman, G\. Yang, H\. Zhang, C\. Hsieh, and P\. Zhang\(2019\)A convex relaxation barrier to tight robustness verification of neural networks\.InNeurIPS,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p2.1)\.
- \[30\]T\. Sunaga\(1958\)Theory of an interval algebra and its application to numerical analysis\.Research Association of Applied Geometry\.Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p4.9),[Theorem 3\.1](https://arxiv.org/html/2607.08773#S3.Thmtheorem1),[§3](https://arxiv.org/html/2607.08773#S3.p1.8),[§4\.6](https://arxiv.org/html/2607.08773#S4.SS6.p1.15)\.
- \[31\]C\. Szegedy, W\. Zaremba, I\. Sutskever, J\. Bruna, D\. Erhan, I\. J\. Goodfellow, and R\. Fergus\(2014\)Intriguing properties of neural networks\.InICLR,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p1.1)\.
- \[32\]D\. Tsipras, S\. Santurkar, L\. Engstrom, A\. Turner, and A\. Madry\(2019\)Robustness may be at odds with accuracy\.InICLR,Cited by:[§6\.1](https://arxiv.org/html/2607.08773#S6.SS1.p3.4)\.
- \[33\]E\. Wong and J\. Z\. Kolter\(2018\)Provable defenses against adversarial examples via the convex outer adversarial polytope\.InICML,Cited by:[Table 1](https://arxiv.org/html/2607.08773#S1.T1),[Table 1](https://arxiv.org/html/2607.08773#S1.T1.1.1.1.1.1.2),[§1](https://arxiv.org/html/2607.08773#S1.p2.1),[§1](https://arxiv.org/html/2607.08773#S1.p4.9),[§1](https://arxiv.org/html/2607.08773#S1.p5.1)\.
- \[34\]H\. Wu, O\. Isac, A\. Zeljic, T\. Tagomori, M\. L\. Daggitt, W\. Kokke, I\. Refaeli, G\. Amir, K\. Julian, S\. Bassan, P\. Huang, O\. Lahav, M\. Wu, M\. Zhang, E\. Komendantskaya, G\. Katz, and C\. W\. Barrett\(2024\)Marabou 2\.0: A versatile formal analyzer of neural networks\.InCAV,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p3.5),[footnote 9](https://arxiv.org/html/2607.08773#footnote9)\.
- \[35\]H\. Xiao, K\. Rasul, and R\. Vollgraf\(2017\)Fashion\-mnist: a novel image dataset for benchmarking machine learning algorithms\.CoRR\.External Links:[Link](http://arxiv.org/abs/1708.07747)Cited by:[item Training Dataset\.](https://arxiv.org/html/2607.08773#S6.I1.ix4.p1.1)\.
- \[36\]H\. Zhang, Y\. Yu, J\. Jiao, E\. P\. Xing, L\. E\. Ghaoui, and M\. I\. Jordan\(2019\)Theoretically principled trade\-off between robustness and accuracy\.InICML,K\. Chaudhuri and R\. Salakhutdinov \(Eds\.\),Cited by:[§6\.1](https://arxiv.org/html/2607.08773#S6.SS1.p3.4)\.
- \[37\]H\. Zhang, H\. Chen, C\. Xiao, S\. Gowal, R\. Stanforth, B\. Li, D\. S\. Boning, and C\. Hsieh\(2020\)Towards stable and efficient training of verifiably robust neural networks\.InICLR,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p2.1)\.
- \[38\]H\. Zhang, T\. Weng, P\. Chen, C\. Hsieh, and L\. Daniel\(2018\)Efficient neural network robustness certification with general activation functions\.InNeurIPS 2018,Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p3.5),[§5\.1](https://arxiv.org/html/2607.08773#S5.SS1.p1.2),[§5\.2](https://arxiv.org/html/2607.08773#S5.SS2.p1.20)\.
- \[39\]Y\. Zhu, C\. Wan, H\. Steck, D\. Liang, Y\. Feng, N\. Kallus, and J\. Li\(2025\)Collaborative retrieval for large language model\-based conversational recommender systems\.Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p1.1)\.
- \[40\]A\. Zuiderwijk, Y\. Chen, and F\. Salem\(2021\)Implications of the use of artificial intelligence in public governance: a systematic literature review and a research agenda\.Government Information Quarterly\.Cited by:[§1](https://arxiv.org/html/2607.08773#S1.p1.1)\.

## Appendix 0\.AOmitted proofs

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

###### Proof

Applying straightforward computations we take,

𝒜​\(I\)\\displaystyle\\mathcal\{A\}\(I\)=‖bi−ℓi‖∞=1d​∑i∈\[d\]maxi∈\[d\]⁡\{ui−ℓi\}\\displaystyle=\\\|b\_\{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\]\.
□\\hfill\\Box

###### Proof

Consider any intervalJ=\[ℓ′,𝒖′\]⊆IJ=\[\\boldsymbol\{\\ell\}^\{\\prime\},\\boldsymbol\{u\}^\{\\prime\}\]\\subseteq Isuch that𝐱′∉J\\mathbf\{x\}^\{\\prime\}\\notin J\. Since𝐱′∉J\\mathbf\{x\}^\{\\prime\}\\notin J, there exists at least one coordinatei∈\[d\]i\\in\[d\]such that eitherui′<xi′u^\{\\prime\}\_\{i\}<x^\{\\prime\}\_\{i\}orℓi′\>xi′\\ell^\{\\prime\}\_\{i\}\>x^\{\\prime\}\_\{i\}\. In either case, the length ofJJalong coordinateiisatisfiesui′−ℓi′≤max⁡\{xi′−ℓi,ui−xi′\}u^\{\\prime\}\_\{i\}\-\\ell^\{\\prime\}\_\{i\}\\leq\\max\\\{x^\{\\prime\}\_\{i\}\-\\ell\_\{i\},\\ u\_\{i\}\-x^\{\\prime\}\_\{i\}\\\}\.

Letk∈\[d\]k\\in\[d\]be the coordinate selected in Definition[3](https://arxiv.org/html/2607.08773#Thmdefinition3), that isk=arg⁡maxi∈\[d\]⁡\|xi−xi′\|k=\\arg\\max\_\{i\\in\[d\]\}\|x\_\{i\}\-x^\{\\prime\}\_\{i\}\|\. By construction, the intervalI/𝐱′I/\\mathbf\{x\}^\{\\prime\}is obtained by shrinkingIIonly along coordinatekk\. Therefore, we have

α​\(I/𝐱′\)=min⁡\{mini≠k⁡\(ui−ℓi\),max⁡\{xk′−ℓk,uk−xk′\}\}\.\\alpha\(I/\\mathbf\{x\}^\{\\prime\}\)=\\min\\left\\\{\\min\_\{i\\neq k\}\(u\_\{i\}\-\\ell\_\{i\}\),\\ \\max\\\{x^\{\\prime\}\_\{k\}\-\\ell\_\{k\},\\ u\_\{k\}\-x^\{\\prime\}\_\{k\}\\\}\\right\\\}\.SinceJ⊆IJ\\subseteq I, we haveui′−ℓi′≤ui−ℓiu^\{\\prime\}\_\{i\}\-\\ell^\{\\prime\}\_\{i\}\\leq u\_\{i\}\-\\ell\_\{i\}for alli∈\[d\]i\\in\[d\], and sinceJJexcludes𝐱′\\mathbf\{x\}^\{\\prime\}, at least one coordinate must satisfy

ui′−ℓi′≤maxi∈\[d\]⁡\{xi′−ℓk,uk−xi′\}≤max⁡\{xk′−ℓk,uk−xk′\}\.u^\{\\prime\}\_\{i\}\-\\ell^\{\\prime\}\_\{i\}\\leq\\max\_\{i\\in\[d\]\}\\\{x^\{\\prime\}\_\{i\}\-\\ell\_\{k\},\\ u\_\{k\}\-x^\{\\prime\}\_\{i\}\\\}\\leq\\max\\\{x^\{\\prime\}\_\{k\}\-\\ell\_\{k\},\\ u\_\{k\}\-x^\{\\prime\}\_\{k\}\\\}\.Therefore, we haveα​\(J\)=mini∈\[d\]⁡\{ui′−ℓi′\}≤α​\(I/𝐱′\)\\alpha\(J\)=\\min\_\{i\\in\[d\]\}\\\{u^\{\\prime\}\_\{i\}\-\\ell^\{\\prime\}\_\{i\}\\\}\\leq\\alpha\(I/\\mathbf\{x\}^\{\\prime\}\), and the proof is complete\.

□\\Box

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

###### Proof

Let𝐲∉I\\mathbf\{y\}\\not\\in I\. Then there exists a coordinationiisuch that eitheryi<xi−R¯iy\_\{i\}<x\_\{i\}\-\\underline\{R\}\_\{i\}oryi\>xi\+R¯iy\_\{i\}\>x\_\{i\}\+\\overline\{R\}\_\{i\}\. By formulas \([6](https://arxiv.org/html/2607.08773#Thmdefinition6)\), no point of𝒟c\\mathcal\{D\}\_\{c\}extends further in that direction\. Hence,𝐲∉𝒟c\\mathbf\{y\}\\not\\in\\mathcal\{D\}\_\{c\}, and thereforeκ​\(𝐲\)≠c\\kappa\(\\mathbf\{y\}\)\\neq c\. Since exiting the interval necessarily the prediction changes, we establish completeness\.

LetJ=\[ℓ,𝒖\]J=\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]be any complete certification containing𝐱\\mathbf\{x\}, implying that for each coordinateii, we have

ℓi≤min⁡\{xi′∣𝐱′∈𝒟c\},ui≥max⁡\{xi′∣𝐱′∈𝒟c\}\.\\ell\_\{i\}\\leq\\min\\\{x^\{\\prime\}\_\{i\}\\mid\\mathbf\{x\}^\{\\prime\}\\in\\mathcal\{D\}\_\{c\}\\\},\\quad u\_\{i\}\\geq\\max\\\{x^\{\\prime\}\_\{i\}\\mid\\mathbf\{x\}^\{\\prime\}\\in\\mathcal\{D\}\_\{c\}\\\}\.Thus, it holds𝒟c⊤𝐱⊆J\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\\subseteq J\. If the inclusion were strict, then there would exist a point outside𝒟c\\mathcal\{D\}\_\{c\}still insideJJ, violating completeness\. Therefore, we conclude thatJ=𝒟c⊤𝐱J=\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\.

Let𝐱1,𝐱2∈𝒟c\\mathbf\{x\}\_\{1\},\\mathbf\{x\}\_\{2\}\\in\\mathcal\{D\}\_\{c\}\. Observe that the radii𝐑¯\\underline\{\\mathbf\{R\}\}and𝐑¯\\overline\{\\mathbf\{R\}\}depend only on the extremal coordinates of𝒟c\\mathcal\{D\}\_\{c\}, not on the choice of𝐱\\mathbf\{x\}\. Changing the reference point𝐱\\mathbf\{x\}shifts both endpoints equally, leaving the interval invariant\. Hence, it holds𝒟c⊤𝐱1=𝒟c⊤𝐱2\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\_\{1\}=\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\_\{2\}, and the proof is complete\.

□\\hfill\\Box

###### Proof

LetIj=\[−ℓj,𝒖j\]I\_\{j\}=\[\-\\boldsymbol\{\\ell\}^\{j\},\\boldsymbol\{u\}^\{j\}\],ℓj,𝒖j≥𝟎\\boldsymbol\{\\ell\}^\{j\},\\boldsymbol\{u\}^\{j\}\\geq\\mathbf\{0\},j∈ℕj\\in\\mathbb\{N\}, be the interval in thejj\-th iteration of the Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1), when we apply the property𝒞𝒩,I​\(𝐱′\)\\mathscr\{C\}\_\{\\mathcal\{N\},I\}\(\\mathbf\{x\}^\{\\prime\}\)and the operator⊔\\sqcup\. Consider somek∈ℕk\\in\\mathbb\{N\}, s\.t\.Ik=Ik\+1I\_\{k\}=I\_\{k\+1\}\. W\.l\.o\.g\., letkkbe the smallest natural with the latter property\. ForIkI\_\{k\}holds thatIk⊇𝒟I\_\{k\}\\supseteq\\mathcal\{D\}, otherwise the𝒞𝒩,I​\(𝐱′\)\\mathscr\{C\}\_\{\\mathcal\{N\},I\}\(\\mathbf\{x\}^\{\\prime\}\)oracle would find a counterexample𝐱a\\mathbf\{x\}^\{a\}, andIk≠Ik⊔𝐱aI\_\{k\}\\neq I\_\{k\}\\sqcup\\mathbf\{x\}^\{a\}, for each𝐱a∈Ik\\mathbf\{x\}^\{a\}\\in I\_\{k\}\. Under this configuration, the Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)terminates after a finite number of steps, withIk⊇𝒟I\_\{k\}\\supseteq\\mathcal\{D\}\. Moreover, since𝒟c⊤𝐱\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}is the unique complete certification it holdsIk⊇𝒟c⊤𝐱I\_\{k\}\\supseteq\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\.

Moreover, for eachj∈\[k\]j\\in\[k\], let𝐱j\\mathbf\{x\}^\{j\}be thejj\-th counterexample returned from the𝒞I,𝒩​\(𝐱′\)\\mathscr\{C\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\)oracle, s\.t\.Ij−1⊔𝐱j=IjI\_\{j\-1\}\\sqcup\\mathbf\{x\}^\{j\}=I\_\{j\}, andI0=\[𝟎,𝟎\]I\_\{0\}=\[\\mathbf\{0\},\\mathbf\{0\}\]\. For eachj∈\[k\]j\\in\[k\], we have a strictly increasing sequence of intervalsI0⊂I1⊂⋯⊂IkI\_\{0\}\\subset I\_\{1\}\\subset\\cdots\\subset I\_\{k\}, sinceIj−1⊂Ij−1⊔𝐱j=IjI\_\{j\-1\}\\subset I\_\{j\-1\}\\sqcup\\mathbf\{x\}^\{j\}=I\_\{j\}\. Consider the set of the firstjjwitnesses returned by the oracle,𝒳j=\{𝐱i∣i∈\[j\]\}\\mathcal\{X\}\_\{j\}=\\\{\\mathbf\{x\}^\{i\}\\mid i\\in\[j\]\\\}\. Naturally,𝒳1⊂𝒳2⊂⋯⊂𝒳k\\mathcal\{X\}\_\{1\}\\subset\\mathcal\{X\}\_\{2\}\\subset\\cdots\\subset\\mathcal\{X\}\_\{k\}\. For thejj\-th iteration, and theii\-th coordinate, consider the values

θ¯ij=max⁡\{−xia∣𝐱a∈𝒳j\},θ¯ij=max⁡\{xia∣𝐱a∈𝒳j\}\.\\underline\{\\theta\}^\{j\}\_\{i\}=\\max\\\{\-x^\{a\}\_\{i\}\\mid\\mathbf\{x\}^\{a\}\\in\\mathcal\{X\}\_\{j\}\\\},\\quad\\overline\{\\theta\}^\{j\}\_\{i\}=\\max\\\{x^\{a\}\_\{i\}\\mid\\mathbf\{x\}^\{a\}\\in\\mathcal\{X\}\_\{j\}\\\}\.\(13\)Clearly, it holdsθ¯ij,θ¯ij≥0\\underline\{\\theta\}^\{j\}\_\{i\},\\overline\{\\theta\}^\{j\}\_\{i\}\\geq 0\. Since,𝒳j⊂𝒟\\mathcal\{X\}\_\{j\}\\subset\\mathcal\{D\}, for eachj∈\[k\]j\\in\[k\], there exist at least one indexi∈\[d\]i\\in\[d\], s\.t\.R¯i≤θ¯ij\\underline\{R\}\_\{i\}\\leq\\underline\{\\theta\}^\{j\}\_\{i\}andθ¯ij≤R¯i\\overline\{\\theta\}^\{j\}\_\{i\}\\leq\\overline\{R\}\_\{i\}\. Next, for thejj\-th iteration, and for everyi∈\[d\]i\\in\[d\], the⊔\\sqcupimplies thatℓij=θ¯ij\+δ\\ell^\{j\}\_\{i\}=\\underline\{\\theta\}^\{j\}\_\{i\}\+\\deltaanduij=θ¯ij\+δu^\{j\}\_\{i\}=\\overline\{\\theta\}^\{j\}\_\{i\}\+\\delta\. Therefore, for eachj∈\[k\]j\\in\[k\]we haveℓij≥R¯i\+δ\\ell^\{j\}\_\{i\}\\geq\\underline\{R\}\_\{i\}\+\\deltaanduij=R¯i\+δu^\{j\}\_\{i\}=\\overline\{R\}\_\{i\}\+\\delta, concluding thatIk⊆𝒟c⊤𝐱\+\[−δ​𝟏,δ​𝟏\]I\_\{k\}\\subseteq\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\+\[\-\\delta\\mathbf\{1\},\\delta\\mathbf\{1\}\]\.

Finally, we show the complexity of the Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1), when we apply the property𝒞I,𝒩​\(𝐱′\)\\mathscr\{C\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\)and the operator⊔\\sqcup\. Consider the potential functionΦ​\(\[−ℓ,𝒖\]\)=∑i∈\[d\]ℓi\+ui\\Phi\(\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\)=\\sum\_\{i\\in\[d\]\}\\ell\_\{i\}\+u\_\{i\}, forℓ,𝒖≥𝟎\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\\geq\\mathbf\{0\}\. For eachj∈\[k\]j\\in\[k\], the coordinateii, s\.t\.ℓij≤ℓij−1\+δ\\ell^\{j\}\_\{i\}\\leq\\ell^\{j\-1\}\_\{i\}\+\\deltaoruij≤uij−1\+δu^\{j\}\_\{i\}\\leq u^\{j\-1\}\_\{i\}\+\\delta\. Thus,Φ​\(Ij\)≤Φ​\(Ij−1\)\+δ\\Phi\(I\_\{j\}\)\\leq\\Phi\(I\_\{j\-1\}\)\+\\delta, andΦ​\(I0\)=Φ​\(\[𝟎,𝟎\]\)=0\\Phi\(I\_\{0\}\)=\\Phi\(\[\\mathbf\{0\},\\mathbf\{0\}\]\)=0\. Now, from Prop\.[4](https://arxiv.org/html/2607.08773#Thmdefinition4)it holds,Φ​\(Ik\)=∑i∈\[d\]ℓik\+uik≤d⋅𝒜​\(Ik\)\\Phi\(I\_\{k\}\)=\\sum\_\{i\\in\[d\]\}\\ell^\{k\}\_\{i\}\+u^\{k\}\_\{i\}\\leq d\\cdot\\mathcal\{A\}\(I\_\{k\}\)\. Hence, we takeΦ​\(Ik\)≤d⋅𝒜​\(𝒟c⊤𝐱\+\[−δ​𝟏,δ​𝟏\]\)≤d⋅\(𝒜​\(𝒟c⊤𝐱\)\+2​δ\)\\Phi\(I\_\{k\}\)\\leq d\\cdot\\mathcal\{A\}\(\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\+\[\-\\delta\\mathbf\{1\},\\delta\\mathbf\{1\}\]\)\\leq d\\cdot\\left\(\\mathcal\{A\}\(\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\)\+2\\delta\\right\)\. So, we haveT=\[Φ​\(Ik\)−Φ​\(I0\)\]/δ=O​\(d⋅\(𝒜​\(𝒟c⊤𝐱\)\+2​δ−0\)/δ\)=O​\(d⋅\(𝒜​\(𝒟c⊤𝐱\)\)/δ\)T=\[\\Phi\(I\_\{k\}\)\-\\Phi\(I\_\{0\}\)\]/\\delta=O\(d\\cdot\\left\(\\mathcal\{A\}\(\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\)\+2\\delta\-0\\right\)/\\delta\)=O\(d\\cdot\\left\(\\mathcal\{A\}\(\\mathcal\{D\}\_\{c\}\\top\\mathbf\{x\}\)\\right\)/\\delta\)\.

□\\hfill\\Box

###### Proof

For sake of contradiction, let𝐱a∈𝒟⊥𝟎∖𝒟\\mathbf\{x\}^\{a\}\\in\\mathcal\{D\}\\bot\\mathbf\{0\}\\setminus\\mathcal\{D\}\. Since𝐱a∈𝒟⊥𝟎\\mathbf\{x\}^\{a\}\\in\\mathcal\{D\}\\bot\\mathbf\{0\}, for eachi∈\[d\]i\\in\[d\], it holds that−r¯i≤xia≤r¯i\-\\underline\{r\}\_\{i\}\\leq x^\{a\}\_\{i\}\\leq\\overline\{r\}\_\{i\}\. Consider somej∈\[d\]j\\in\[d\], s\.t\.𝐱a∈V¯j\\mathbf\{x\}^\{a\}\\in\\underline\{V\}\_\{j\}or𝐱a∈V¯j\\mathbf\{x\}^\{a\}\\in\\overline\{V\}\_\{j\}\(but not both, since𝐱a≠𝟎\\mathbf\{x\}^\{a\}\\neq\\mathbf\{0\}\)\. Let𝐱a∈V¯j\\mathbf\{x\}^\{a\}\\in\\underline\{V\}\_\{j\}\. Then,r¯j<−xja\\underline\{r\}\_\{j\}<\-x^\{a\}\_\{j\}, or−r¯j\>xja\-\\underline\{r\}\_\{j\}\>x^\{a\}\_\{j\}\. A contradiction\. When𝐱a∈V¯j\\mathbf\{x\}^\{a\}\\in\\overline\{V\}\_\{j\}, we work similarly\.

□\\hfill\\Box

###### Proof

LetIj=\[−ℓj,𝒖j\]I\_\{j\}=\[\-\\boldsymbol\{\\ell\}^\{j\},\\boldsymbol\{u\}^\{j\}\],ℓj,𝒖j≥𝟎\\boldsymbol\{\\ell\}^\{j\},\\boldsymbol\{u\}^\{j\}\\geq\\mathbf\{0\},j∈ℕj\\in\\mathbb\{N\}, be the interval in thejj\-th iteration of the Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1), when we apply the property𝒮𝒩,I​\(𝐱′\)\\mathscr\{S\}\_\{\\mathcal\{N\},I\}\(\\mathbf\{x\}^\{\\prime\}\)and the operator⊓\\sqcap\. W\.l\.o\.g\., letkkbe the smallest natural with the latter property\. ForIkI\_\{k\}holds thatIk⊆𝒟I\_\{k\}\\subseteq\\mathcal\{D\}\. Otherwise, the soundness oracle𝒮𝒩,I​\(𝐱′\)\\mathscr\{S\}\_\{\\mathcal\{N\},I\}\(\\mathbf\{x\}^\{\\prime\}\)would find a counterexample𝐱a\\mathbf\{x\}^\{a\}\. AndIk≠Ik⊓𝐱aI\_\{k\}\\neq I\_\{k\}\\sqcap\\mathbf\{x\}^\{a\}, for each𝐱a∈Ik\\mathbf\{x\}^\{a\}\\in I\_\{k\}\. Therefore, Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1)terminates after a finite number of steps, withIk⊆𝒟I\_\{k\}\\subseteq\\mathcal\{D\}\.

Moreover, for eachj∈\[k\]j\\in\[k\], let𝐱j\\mathbf\{x\}^\{j\}be thejj\-th counterexample returned by the𝒮I,𝒩​\(𝐱′\)\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\)oracle, s\.t\.Ij−1⊓𝐱j=IjI\_\{j\-1\}\\sqcap\\mathbf\{x\}^\{j\}=I\_\{j\}, andI0=𝔽I\_\{0\}=\\mathbb\{F\}\. For eachj∈\[k\]j\\in\[k\], we have a strictly decreasing sequence of intervalsI0⊃I1⊃⋯⊃IkI\_\{0\}\\supset I\_\{1\}\\supset\\cdots\\supset I\_\{k\}, sinceIj−1⊃Ij−1⊓𝐱j=IjI\_\{j\-1\}\\supset I\_\{j\-1\}\\sqcap\\mathbf\{x\}^\{j\}=I\_\{j\}\. Consider the set of the firstjjwitnesses returned by the oracle,𝒳j=\{𝐱i∣i∈\[j\]\}\\mathcal\{X\}\_\{j\}=\\\{\\mathbf\{x\}^\{i\}\\mid i\\in\[j\]\\\}\. Naturally,𝒳1⊂X2⊂⋯⊂𝒳k\\mathcal\{X\}\_\{1\}\\subset X\_\{2\}\\subset\\cdots\\subset\\mathcal\{X\}\_\{k\}\. For thejj–th iteration, and theii–th coordinate, consider the values

τ¯ij=min⁡\{xia∣𝐱a∈V¯i∩𝒳j\},τ¯ij=min⁡\{xia∣𝐱a∈V¯i∩𝒳j\}\\underline\{\\tau\}^\{j\}\_\{i\}=\\min\\\{x^\{a\}\_\{i\}\\mid\\mathbf\{x\}^\{a\}\\in\\underline\{V\}\_\{i\}\\cap\\mathcal\{X\}\_\{j\}\\\},\\quad\\overline\{\\tau\}^\{j\}\_\{i\}=\\min\\\{x^\{a\}\_\{i\}\\mid\\mathbf\{x\}^\{a\}\\in\\overline\{V\}\_\{i\}\\cap\\mathcal\{X\}\_\{j\}\\\}\(14\)Now, applying the operator⊓\\sqcapto intervals\[−ℓ,𝒖\]\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]and\[𝐱a,𝐱a\]\[\\mathbf\{x\}^\{a\},\\mathbf\{x\}^\{a\}\], for any𝐱a∈ℝd\\mathbf\{x\}^\{a\}\\in\\mathbb\{R\}^\{d\}, we have

\{ℓi′=xia−δ,if​𝐱a∈V¯i∩\[−ℓ,𝒖\],ui′=xia−δ,if​𝐱a∈V¯i∩\[−ℓ,𝒖\]\.\\begin\{cases\}\\ell^\{\\prime\}\_\{i\}=x^\{a\}\_\{i\}\-\\delta,&\\text\{if\}~~\\mathbf\{x\}^\{a\}\\in\\underline\{V\}\_\{i\}\\cap\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\],\\\\ u^\{\\prime\}\_\{i\}=x^\{a\}\_\{i\}\-\\delta,&\\text\{if\}~~\\mathbf\{x\}^\{a\}\\in\\overline\{V\}\_\{i\}\\cap\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\.\\end\{cases\}\(15\)Otherwise,\[−ℓ,𝒖\]=\[−ℓ,𝒖\]⊓𝐱a\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]=\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\sqcap\\mathbf\{x\}^\{a\}, when𝐱a∉\[−ℓ,𝒖\]\\mathbf\{x\}^\{a\}\\notin\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\. If𝐱a∈V¯i\\mathbf\{x\}^\{a\}\\in\\underline\{V\}\_\{i\}, we update theii\-th value ofℓ\\boldsymbol\{\\ell\}to bexia−δx^\{a\}\_\{i\}\-\\delta\. Symmetrically, if𝐱a∈V¯i\\mathbf\{x\}^\{a\}\\in\\overline\{V\}\_\{i\}, we update theii\-th value of𝒖\\boldsymbol\{u\}to bexia−δx^\{a\}\_\{i\}\-\\delta\.

Since,𝒳j⊂𝔽∖𝒟\\mathcal\{X\}\_\{j\}\\subset\\mathbb\{F\}\\setminus\\mathcal\{D\}, we haver¯i≤τ¯ij\\underline\{r\}\_\{i\}\\leq\\underline\{\\tau\}\_\{i\}^\{j\}andr¯i≤τ¯ij\\overline\{r\}\_\{i\}\\leq\\overline\{\\tau\}\_\{i\}^\{j\}, for eachj∈\[k\]j\\in\[k\]\. From eq\. \([15](https://arxiv.org/html/2607.08773#Pt0.A1.E15)\), for thejj\-th iteration, and theii\-th coordinate, we haveℓij=τ¯ij−δ\\ell^\{j\}\_\{i\}=\\underline\{\\tau\}^\{j\}\_\{i\}\-\\deltaanduij=τ¯ij−δu^\{j\}\_\{i\}=\\overline\{\\tau\}^\{j\}\_\{i\}\-\\delta\. Thus, for eachj∈\[k\]j\\in\[k\]we haveℓij≥r¯i−δ\\ell^\{j\}\_\{i\}\\geq\\underline\{r\}\_\{i\}\-\\deltaanduij≥r¯i−δu^\{j\}\_\{i\}\\geq\\overline\{r\}\_\{i\}\-\\delta\. Therefore,Ik⊇𝒟⊥𝐱−δ​𝟏I\_\{k\}\\supseteq\\mathcal\{D\}\\bot\\mathbf\{x\}\-\\delta\\mathbf\{1\}\.

Finally, we show theGenericTraversalalgorithm’s complexity\. Consider the potential functionΦ​\(\[−ℓ,𝒖\]\)=∑i∈\[d\]ℓi\+ui\\Phi\(\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\)=\\sum\_\{i\\in\[d\]\}\\ell\_\{i\}\+u\_\{i\}, forℓ,𝒖≥𝟎\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\\geq\\mathbf\{0\}\. For eachj∈\[k\]j\\in\[k\], there is a coordinateii, s\.t\.ℓij≤ℓij−1−δ\\ell^\{j\}\_\{i\}\\leq\\ell^\{j\-1\}\_\{i\}\-\\deltaoruij≤uij−1−δu^\{j\}\_\{i\}\\leq u^\{j\-1\}\_\{i\}\-\\delta\. Thus,Φ​\(Ij\)≤Φ​\(Ij−1\)−δ\\Phi\(I\_\{j\}\)\\leq\\Phi\(I\_\{j\-1\}\)\-\\delta\. Additionally,Φ​\(I0\)=d⋅𝒜​\(𝔽\)\\Phi\(I\_\{0\}\)=d\\cdot\\mathcal\{A\}\(\\mathbb\{F\}\), andΦ​\(Ik\)≥d⋅𝒜​\(𝒟⊥𝐱\)−δ\\Phi\(I\_\{k\}\)\\geq d\\cdot\\mathcal\{A\}\(\\mathcal\{D\}\\bot\\mathbf\{x\}\)\-\\delta\. Hence, for the complexity of the Algorithm[1](https://arxiv.org/html/2607.08773#algorithm1), we haveT=\[Φ\(I0\)−Φ\(Ik\)\]/δ=O\(d\[𝒜\(𝔽\)−𝒜\(\(𝒟⊥𝐱\)\+δ\]/δ\)=O\(d\[𝒜\(𝔽\)−𝒜\(𝒟⊥𝐱\)\]/δ\)T=\[\\Phi\(I\_\{0\}\)\-\\Phi\(I\_\{k\}\)\]/\\delta=O\(d\[\\mathcal\{A\}\(\\mathbb\{F\}\)\-\\mathcal\{A\}\(\(\\mathcal\{D\}\\bot\\mathbf\{x\}\)\+\\delta\]/\\delta\)=O\(d\[\\mathcal\{A\}\(\\mathbb\{F\}\)\-\\mathcal\{A\}\(\\mathcal\{D\}\\bot\\mathbf\{x\}\)\]/\\delta\)\.

□\\hfill\\Box

###### Proof

If𝐱∈𝒟c∘\\mathbf\{x\}\\in\\mathcal\{D\}^\{\\circ\}\_\{c\}, then there is someρ\>0\\rho\>0, s\.t\.ℬ∞​\(𝐱,ρ\)⊆𝒟\\mathcal\{B\}^\{\\infty\}\(\\mathbf\{x\},\\rho\)\\subseteq\\mathcal\{D\}\. Chooseρ\\rhoto be the greatest real number s\.t\. the previous statement holds\. Then, for eachi∈\[d\]i\\in\[d\]holdsr¯i,r¯i≥ρ\>0\\underline\{r\}\_\{i\},\\overline\{r\}\_\{i\}\\geq\\rho\>0\. Thus,α​\(𝒟c⊥𝐱\)\>0\\alpha\(\\mathcal\{D\}\_\{c\}\\bot\\mathbf\{x\}\)\>0\.

□\\hfill\\Box

###### Proof

\[⇒\]\[\\Rightarrow\]We prove the contrapositive\. Let somei∈\[d\]i\\in\[d\]and someδ\>0\\delta\>0, s\.t\. either\[−\(ℓ\+δ​𝐞i\),𝒖\]∖𝒟c=∅\[\-\(\\boldsymbol\{\\ell\}\+\\delta\\mathbf\{e\}^\{i\}\),\\boldsymbol\{u\}\]\\setminus\\mathcal\{D\}\_\{c\}=\\varnothing*or*\[−ℓ,𝒖\+δ​𝐞i\]∖𝒟c=∅\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\+\\delta\\mathbf\{e\}^\{i\}\]\\setminus\\mathcal\{D\}\_\{c\}=\\varnothing\(or both\)\. W\.l\.o\.g\. let\[−\(ℓ\+δ​𝐞i\),𝒖\]∖𝒟c=∅\[\-\(\\boldsymbol\{\\ell\}\+\\delta\\mathbf\{e\}^\{i\}\),\\boldsymbol\{u\}\]\\setminus\\mathcal\{D\}\_\{c\}=\\varnothing\. Since\[−\(ℓ\+δ​𝐞i\),𝒖\]⊃\[−ℓ,𝒖\]\[\-\(\\boldsymbol\{\\ell\}\+\\delta\\mathbf\{e\}^\{i\}\),\\boldsymbol\{u\}\]\\supset\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\], then\[−ℓ,𝒖\]\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]is not maximal\.

\[⇐\]\[\\Leftarrow\]Let for everyi∈\[d\]i\\in\[d\], and everyδ\>0\\delta\>0, we assume that holds,\[−\(ℓ\+δ​𝐞i\),𝒖\]∖𝒟c≠∅\[\-\(\\boldsymbol\{\\ell\}\+\\delta\\mathbf\{e\}^\{i\}\),\\boldsymbol\{u\}\]\\setminus\\mathcal\{D\}\_\{c\}\\neq\\varnothing*and*\[−ℓ,𝒖\+δ​𝐞i\]∖𝒟c≠∅\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\+\\delta\\mathbf\{e\}^\{i\}\]\\setminus\\mathcal\{D\}\_\{c\}\\neq\\varnothing\. Now assume someI′⊃I=\[−ℓ,𝒖\]I^\{\\prime\}\\supset I=\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\. There arei∈\[d\]i\\in\[d\]andδ\>0\\delta\>0, s\.t\.I′⊇\[−\(ℓ\+δ​𝐞i\),𝒖\]I^\{\\prime\}\\supseteq\[\-\(\\boldsymbol\{\\ell\}\+\\delta\\mathbf\{e\}^\{i\}\),\\boldsymbol\{u\}\]orI′⊇\[−ℓ,𝒖\+δ​𝐞i\]I^\{\\prime\}\\supseteq\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\+\\delta\\mathbf\{e\}^\{i\}\]\(or both\)\. Therefore,I′∖𝒟c≠∅I^\{\\prime\}\\setminus\\mathcal\{D\}\_\{c\}\\neq\\varnothing\. Hence,IIis maximal\.

□\\hfill\\Box

###### Proof

We start from the trivial sound certificationX=\[𝐱,𝐱\]∈𝕀​\(d\)\|𝐱𝔽X=\[\\mathbf\{x\},\\mathbf\{x\}\]\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}\. Let,I∗=\[ℓ∗,𝒖∗\]∈\[X\]I^\{\\ast\}=\[\\boldsymbol\{\\ell\}^\{\\ast\},\\boldsymbol\{u\}^\{\\ast\}\]\\in\[X\]be an arbitrary maximally sound interval\. Observe that Algorithm[3](https://arxiv.org/html/2607.08773#algorithm3), at each iteration, expands exactly one coordinate of either the lower or upper endpoint byδ\\delta\. Therefore, it performs monotone expansions of the current intervalII\. Thus, the algorithm defines a monotone path in the interval lattice⟨𝕀​\(d\)\|𝐱𝔽,⊆⟩\\langle\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\},\\subseteq\\rangle, starting fromXX\.

Next, we consider the following non\-deterministic strategy: i\) if the algorithm expands a coordinatekkof the lower endpoint, then it chooseskks\.t\.ℓk<ℓk∗\\ell\_\{k\}<\\ell^\{\\ast\}\_\{k\}, and ii\) if the algorithm expands a coordinatekkof the upper endpoint, then it chooseskks\.t\.uk<uk∗u\_\{k\}<u^\{\\ast\}\_\{k\}\. As long as the current intervalIIsatisfiesI⊆I∗I\\subseteq I^\{\\ast\}, all expansions are sound\. Since each coordinate is expanded in increments of sizeδ\\delta, after at most

⌈u∗−xkδ⌉or⌈xk−ℓ∗δ⌉\\left\\lceil\\frac\{u^\{\\ast\}\-x\_\{k\}\}\{\\delta\}\\right\\rceil\\quad\\text\{ or \}\\quad\\left\\lceil\\frac\{x\_\{k\}\-\\ell^\{\\ast\}\}\{\\delta\}\\right\\rceilsteps per coordinate, the algorithm reaches an intervalJJs\.t\.I−\[−δ​𝟏,δ​𝟏\]⊆J⊆II\-\[\-\\delta\\mathbf\{1\},\\delta\\mathbf\{1\}\]\\subseteq J\\subseteq I\. Observe that, by Lem\.[8](https://arxiv.org/html/2607.08773#Thmdefinition8), for every coordinateiiand everyδ\>0\\delta\>0, any further unilateral expansion beyondI∗I^\{\\ast\}results in a counterexample\.

Finally, for the complexity, there are2​d2dcoordinates of all endpoints, and they can be expanded at mostO​\(1/δ\)O\(1/\\delta\)times\. Each expansion requires one call in the soundness oracle𝒮I,𝒩​\(𝐱′\)\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{x\}^\{\\prime\}\), costing𝒜​\(𝔽\)\\mathcal\{A\}\(\\mathbb\{F\}\)\. Therefore, the total number of non\-deterministic steps is

O​\(d⋅𝒜​\(𝔽\)δ\),O\\left\(d\\cdot\\frac\{\\mathcal\{A\}\(\\mathbb\{F\}\)\}\{\\delta\}\\right\),and the proof is complete\.

□\\hfill\\Box

### 0\.A\.3Proofs of Section[5](https://arxiv.org/html/2607.08773#S5)

###### Proof

The proof relies on a reduction from q\-MERtoSIM\. Given an instanceℐ\\mathcal\{I\}in q\-MER, we can construct an instanceℐ′\\mathcal\{I\}^\{\\prime\}inSIMas follows\. Let𝐱:=𝐪\\mathbf\{x\}:=\\mathbf\{q\}, we define the decision surface𝒟c:=𝔽∖ℱ\\mathcal\{D\}\_\{c\}:=\\mathbb\{F\}\\setminus\\mathcal\{F\}\. Since the setℱ\\mathcal\{F\}is finite and𝔽\\mathbb\{F\}is compact, the set𝒟c\\mathcal\{D\}\_\{c\}is compact as well\. Next, we interpret every forbidden point𝐟∈ℱ\\mathbf\{f\}\\in\\mathcal\{F\}as a counterexample, that is, given the classifierκ​\(⋅\)\\kappa\(\\cdot\), it holdsκ​\(𝐟\)≠c\\kappa\(\\mathbf\{f\}\)\\neq c\. Using the terminology of the soundness oracle, eq\. \([5](https://arxiv.org/html/2607.08773#S4.E5)\), we have that𝐟⊧ℐI,𝒩​\(𝐟\)\\mathbf\{f\}\\models\\mathscr\{I\}\_\{I,\\mathcal\{N\}\}\(\\mathbf\{f\}\)for all points inℱ\\mathcal\{F\}\. Contrarily, sound intervals are precisely those that excludeℱ\\mathcal\{F\}\. Therefore, an intervalI∈𝕀​\(d\)\|𝐱𝔽I\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, withI⊆𝒟cI\\subseteq\\mathcal\{D\}\_\{c\}, is sound iffI∩ℱ=∅I\\cap\\mathcal\{F\}=\\emptyset\. Since we have set𝐱:=𝐪\\mathbf\{x\}:=\\mathbf\{q\}, and the objective constraintv​\(I\)≥γv\(I\)\\geq\\gamma, forγ\>0\\gamma\>0, is identical in both problems, the reduction is established\. Hence, theℐ\\mathcal\{I\}is feasible iff theℐ′\\mathcal\{I\}^\{\\prime\}is feasible\. Since the problem q\-MERcan not be decided in polynomial time, the problemSIMcan not be decided in polynomial time, as well, and the proof is complete\.

□\\hfill\\Box

###### 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/2607.08773#bib.bib83)\]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/2607.08773#bib.bib83)\], 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\.

□\\hfill\\Box

###### Proof

We present an algorithm with executed in a logarithmic number of oracle calls in Algorithm[2](https://arxiv.org/html/2607.08773#algorithm2)\. Essentially, we do a*dichotomic*search in the real interval\[0,𝒜​\(𝔽\)\]\[0,\\mathcal\{A\}\(\\mathbb\{F\}\)\]\.

Input:

𝐱∈𝔽\\mathbf\{x\}\\in\\mathbb\{F\}, the center of the uniform interval certification, and a percision constant

δ\>0\\delta\>0\.

Output:A maximally sound uniform interval certification

𝚕𝚘𝚠←0\\mathtt\{low\}\\leftarrow 0;

𝚑𝚒𝚐𝚑←𝒜​\(𝔽\)\\mathtt\{high\}\\leftarrow\\mathcal\{A\}\(\\mathbb\{F\}\);

while*𝚑𝚒𝚐𝚑−𝚕𝚘𝚠\>δ\\mathtt\{high\}\-\\mathtt\{low\}\>\\delta*do

ρ←\(𝚑𝚒𝚐𝚑−𝚕𝚘𝚠\)/2\\rho\\leftarrow\(\\mathtt\{high\}\-\\mathtt\{low\}\)/2
B←ℬ​\(𝐱,ρ\)B\\leftarrow\\mathcal\{B\}\(\\mathbf\{x\},\\rho\)
if*∃𝐱′\\exists\\mathbf\{x\}^\{\\prime\}, s\.t\.𝐱′⊧𝒮B,𝒩\\mathbf\{x\}^\{\\prime\}\\models\\mathscr\{S\}\_\{B,\\mathcal\{N\}\}*then

𝚑𝚒𝚐𝚑←ρ\\mathtt\{high\}\\leftarrow\\rho
else

𝚕𝚘𝚠←ρ\\mathtt\{low\}\\leftarrow\\rho
end if

end while

return*BB*

Algorithm 2𝔹\\mathbb\{B\}–TopDown Search□\\hfill\\Box

Note that Algorithm[2](https://arxiv.org/html/2607.08773#algorithm2)can easily be modified to compute complete uniform certifications\. We simply use the𝒞B,𝒩\\mathscr\{C\}\_\{B,\\mathcal\{N\}\}predicate, instead of𝒮B,𝒩\\mathscr\{S\}\_\{B,\\mathcal\{N\}\}, and switching steps 6, 8\.

## Appendix 0\.BGeometry of theℝd\\mathbb\{R\}^\{d\}Cone Partition

In this section, we briefly discuss the geometry involved in the cone decomposition ofℝd\\mathbb\{R\}^\{d\}, introduced in eq\. \([8](https://arxiv.org/html/2607.08773#S4.E8)\) of Sec\.[4](https://arxiv.org/html/2607.08773#S4)\. To that end, we firstly introduce some elementary concepts of affine geometry\. Then we proceed to examine the intersections of these cones\.

### 0\.B\.1Elements of Affine Geometry

We begin with convex bodies\. Forℓ,𝒖∈ℝd\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\\in\\mathbb\{R\}^\{d\}, the line segment with endpointsℓ\\boldsymbol\{\\ell\}and𝒖\\boldsymbol\{u\}is defined asL​\(ℓ,𝒖\)=\{𝐱∈ℝd∣x=ℓ\+t⋅\(𝒖−ℓ\),t∈\[0,1\]\}\\text\{L\}\(\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\)=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}\\mid x=\\boldsymbol\{\\ell\}\+t\\cdot\(\\boldsymbol\{u\}\-\\boldsymbol\{\\ell\}\),~t\\in\[0,1\]\\\}\. A setS⊆ℝdS\\subseteq\\mathbb\{R\}^\{d\}is said to be convex ifL​\(ℓ,𝒖\)⊆SL\(\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\)\\subseteq Sfor everyℓ,𝒖∈S\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\\in S\. A convex body is a convex and compact subset ofℝd\\mathbb\{R\}^\{d\}with nonempty interior\. An important class of convex sets is the*polyhedra*\. LetA∈ℝm×nA\\in\\mathbb\{R\}^\{m\\times n\}and𝒖∈ℝm\\boldsymbol\{u\}\\in\\mathbb\{R\}^\{m\}\. The setP=\{𝐱∈ℝn∣A​𝐱≤𝒖\}P=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{n\}\\mid A\\mathbf\{x\}\\leq\\boldsymbol\{u\}\\\}is called a \(convex\) polyhedron\. If𝒖=𝟎\\boldsymbol\{u\}=\\mathbf\{0\}, we obtain a polyhedral coneC=\{𝐱∈ℝm∣A​𝐱≤𝟎\}C=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{m\}\\mid A\\mathbf\{x\}\\leq\\mathbf\{0\}\\\}\.

A set of vectors𝐯1,…,𝐯n∈ℝd\\mathbf\{v\}\_\{1\},\\dots,\\mathbf\{v\}\_\{n\}\\in\\mathbb\{R\}^\{d\}is*affinely independent*if the vectors\[𝐯11\]\\left\[\\mathbf\{v\}\_\{1\}\\atop 1\\right\],…\\dots,\[𝐯n1\]\\left\[\\mathbf\{v\}\_\{n\}\\atop 1\\right\]are*linearly independent*\. The*dimension*of a polyhedronPP, denoted𝖽𝗂𝗆​\(P\)\\mathsf\{dim\}\(P\), is the cardinality of the largest affinely independent subset ofPP*minus one*\. Given a polyhedronP=\{𝐱∈ℝm∣A​𝐱≤𝒖\}P=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{m\}\\mid A\\mathbf\{x\}\\leq\\boldsymbol\{u\}\\\}a*face*FFis another polyhedronF=\{𝐱∈ℝn∣A′​𝐱≤𝒖′\}F=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{n\}\\mid A^\{\\prime\}\\mathbf\{x\}\\leq\\boldsymbol\{u\}^\{\\prime\}\\\}, whereA′A^\{\\prime\}is a submatrix ofAAand𝒖′\\boldsymbol\{u\}^\{\\prime\}is the respective subvector of𝒖\\boldsymbol\{u\}\. A*facet*is a face ofPPwith dimention𝖽𝗂𝗆​\(P\)−1\\mathsf\{dim\}\(P\)\-1\.

### 0\.B\.2Intersections of Cones

![Refer to caption](https://arxiv.org/html/2607.08773v1/figures/cones-3D-1-axes-cropped.png)

![Refer to caption](https://arxiv.org/html/2607.08773v1/figures/cones-3D-2.1-cropped.png)

Figure 3:Cone Decomposition ofℝ3\\mathbb\{R\}^\{3\}\. The polyhedral cones of eq\. \([8](https://arxiv.org/html/2607.08773#S4.E8)\), correspond to*pyramids*isℝ3\\mathbb\{R\}^\{3\}\. Left: TheV¯1,V¯1\\underline\{V\}\_\{1\},\\overline\{V\}\_\{1\}cones of thex1x\_\{1\}–axis\. Observe thatV¯1∩V¯1=\{𝟎\}\\underline\{V\}\_\{1\}\\cap\\overline\{V\}\_\{1\}=\\\{\\mathbf\{0\}\\\}\. Right: The cone decomposition , of the entireℝ3\\mathbb\{R\}^\{3\}\.To gain intuition about the underlying problem, we present the cone decomposition ofℝ3\\mathbb\{R\}^\{3\}in Fig\.[3](https://arxiv.org/html/2607.08773#Pt0.A2.F3)\. Our focus is on the intersection of a collection of cones\. We express the cones of eq\. \([8](https://arxiv.org/html/2607.08773#S4.E8)\) as a set of inequalities\. For eachi∈\[d\]i\\in\[d\], letU¯i,U¯i∈ℝd×d\\underline\{U\}\_\{i\},\\overline\{U\}\_\{i\}\\in\\mathbb\{R\}^\{d\\times d\}denote two associated matrices\. For the matrixU¯i\\underline\{U\}\_\{i\}, every element of theii\-th column is−1\-1\. For allm≠nm\\neq nthe entry, we have\(u¯i\)m​n=0\(\\underline\{u\}\_\{i\}\)\_\{mn\}=0\. Finally, forn≠in\\neq i, the diagonal entries satisfy\(u¯i\)n​n=−1\(\\underline\{u\}\_\{i\}\)\_\{nn\}=\-1\. ForU¯i\\overline\{U\}\_\{i\}, the construction is identical, except that every element in theii\-th column equals\+1\+1\. All other entries coincide with those ofU¯i\\underline\{U\}\_\{i\}\. In Fig\.[4](https://arxiv.org/html/2607.08773#Pt0.A2.F4), we give an example whend=4d=4\. With this notation in place, the cones from eq\. \([8](https://arxiv.org/html/2607.08773#S4.E8)\) can now be written equivalently in the form,

V¯i=\{𝐱∈ℝd∣U¯i​𝐱≥𝟎\},V¯i=\{𝐱∈ℝd∣U¯i​𝐱≥𝟎\}\.\\underline\{V\}\_\{i\}=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}\\mid\\underline\{U\}\_\{i\}\\mathbf\{x\}\\geq\\mathbf\{0\}\\\},\\quad\\overline\{V\}\_\{i\}=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}\\mid\\overline\{U\}\_\{i\}\\mathbf\{x\}\\geq\\mathbf\{0\}\\\}\.\(16\)
U¯2=\[−1−1000−1000−1−100−10−1\]\\underline\{U\}\_\{2\}=\\left\[\\begin\{array\}\[\]\{c c c c \}\-1&\-1&0&0\\\\ 0&\-1&0&0\\\\ 0&\-1&\-1&0\\\\ 0&\-1&0&\-1\\\\ \\end\{array\}\\right\]
U¯3=\[−10100−1100010001−1\]\\overline\{U\}\_\{3\}=\\left\[\\begin\{array\}\[\]\{c c c c \}\-1&0&1&0\\\\ 0&\-1&1&0\\\\ 0&0&1&0\\\\ 0&0&1&\-1\\\\ \\end\{array\}\\right\]
U¯¯23=\[−1−1100−1100−1100−11−1\]\\underline\{\\overline\{U\}\}\_\{23\}=\\left\[\\begin\{array\}\[\]\{c c c c \}\-1&\-1&1&0\\\\ 0&\-1&1&0\\\\ 0&\-1&1&0\\\\ 0&\-1&1&\-1\\\\ \\end\{array\}\\right\]

Figure 4:Left, Middle: The matricesU¯2,U¯3∈ℝ4×4\\underline\{U\}\_\{2\},\\overline\{U\}\_\{3\}\\in\\mathbb\{R\}^\{4\\times 4\}, for the conesV¯2,V¯2\\underline\{V\}\_\{2\},\\overline\{V\}\_\{2\}\. It holds thatV¯2∩V¯3=\{𝐱∈ℝd∣U¯¯23​𝐱≥𝟎\}\\underline\{V\}\_\{2\}\\cap\\overline\{V\}\_\{3\}=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}\\mid\\underline\{\\overline\{U\}\}\_\{23\}\\mathbf\{x\}\\geq\\mathbf\{0\}\\\}\.Eq\. \([16](https://arxiv.org/html/2607.08773#Pt0.A2.E16)\) is equivalent to eq\. \([8](https://arxiv.org/html/2607.08773#S4.E8)\)\. Note that for eachi∈\[d\]i\\in\[d\], the conesV¯i\\underline\{V\}\_\{i\}andV¯i\\overline\{V\}\_\{i\}both have full dimension, that is𝖽𝗂𝗆​\(V¯i\)=𝖽𝗂𝗆​\(V¯i\)=d\\mathsf\{dim\}\(\\underline\{V\}\_\{i\}\)=\\mathsf\{dim\}\(\\overline\{V\}\_\{i\}\)=d\. Indeed, the rows ofU¯i\\underline\{U\}\_\{i\}form a set ofddlinearly independent vectors\. Together with the origin, these yieldd\+1d\+1affinely independent vectors, confirming thatV¯i\\underline\{V\}\_\{i\}has dimensiondd\. An identical argument applies toV¯i\\overline\{V\}\_\{i\}\.

Next, consider the intersectionV¯i∩V¯j\\overline\{V\}\_\{i\}\\cap\\overline\{V\}\_\{j\}for distinct indicesi≠ji\\neq j\. For any𝐱∈V¯i∩V¯j\\mathbf\{x\}\\in\\overline\{V\}\_\{i\}\\cap\\overline\{V\}\_\{j\}it must holdsU¯i​𝐱≥𝟎\\overline\{U\}\_\{i\}\\mathbf\{x\}\\geq\\mathbf\{0\}*and*U¯j​𝐱≥𝟎\\overline\{U\}\_\{j\}\\mathbf\{x\}\\geq\\mathbf\{0\}\. Thusly, we can define a matrixU¯i​j\\overline\{U\}\_\{ij\}, s\.t\. holdsU¯i​j​𝐱≥𝟎\\overline\{U\}\_\{ij\}\\mathbf\{x\}\\geq\\mathbf\{0\},*iff*U¯i​𝐱≥𝟎\\overline\{U\}\_\{i\}\\mathbf\{x\}\\geq\\mathbf\{0\}*and*U¯j​𝐱≥𝟎\\overline\{U\}\_\{j\}\\mathbf\{x\}\\geq\\mathbf\{0\}\. Concretely,U¯i​j\\overline\{U\}\_\{ij\}is obtained fromU¯i\\overline\{U\}\_\{i\}by replacing thejj\-th column with all ones, while leaving all other entries unchanged\. Hence,V¯i∩V¯j=\{𝐱∈ℝd∣U¯i​j​𝐱≥𝟎\}\\overline\{V\}\_\{i\}\\cap\\overline\{V\}\_\{j\}=\\\{\\mathbf\{x\}\\in\\mathbb\{R\}^\{d\}\\mid\\overline\{U\}\_\{ij\}\\mathbf\{x\}\\geq\\mathbf\{0\}\\\}\. An example ford=4d=4is shown in Fig\.[4](https://arxiv.org/html/2607.08773#Pt0.A2.F4)\. Geometrically, this intersection reduces the dimension by one,𝖽𝗂𝗆​\(V¯i∩V¯j\)=d−1\\mathsf\{dim\}\(\\overline\{V\}\_\{i\}\\cap\\overline\{V\}\_\{j\}\)=d\-1\. Analogous constructions hold for the intersectionsV¯i∩V¯j\\underline\{V\}\_\{i\}\\cap\\overline\{V\}\_\{j\}andV¯i∩V¯j\\underline\{V\}\_\{i\}\\cap\\underline\{V\}\_\{j\}\. This agrees with the geometric intuition from Fig\.[3](https://arxiv.org/html/2607.08773#Pt0.A2.F3), since the intersection of two different pyramids inℝ3\\mathbb\{R\}^\{3\}is a facet\.

## Appendix 0\.CImplementing the Maximal Closure Operator

In this section, we examine a*deterministic*expansion method for computing maximally sound interval certifications\. Essentially, theNon–deterministic Expansionmethod, introduced in Sec\.[4](https://arxiv.org/html/2607.08773#S4), and described in Algorithm[3](https://arxiv.org/html/2607.08773#algorithm3), defines a*collection*of deterministic algorithms, each making different choices on the coordinate to expand next\. In Algorithm[4](https://arxiv.org/html/2607.08773#algorithm4), we describe a simple, novel141414The authors in\[[11](https://arxiv.org/html/2607.08773#bib.bib2)\]mention a dichotomic expansion as an alternative to their linear expansion algorithm\. However, they do not give any details\.and deterministic method, that expands each coordinate sequentially\. At each step, we make a dichotomic \(or binary\) search to expand theii\-th coordinate\. Below, we establish the correctness and computational complexity of the above algorithm\.

Input:

I0∈𝕀​\(d\)\|𝐱𝔽I\_\{0\}\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, an initial sound interval certification, and

δ\>0\\delta\>0, a percision constant\.

Output:

J∈𝕀​\(d\)\|𝐱𝔽J\\in\\mathbb\{I\}\(d\)\|^\{\\mathbb\{F\}\}\_\{\\mathbf\{x\}\}, a expanded interval s\.t\.

J⊇IJ\\supseteq I\.

I←I0I\\leftarrow I\_\{0\};

ℐ¯←∅\\underline\{\\mathcal\{I\}\}\\leftarrow\\varnothing;

ℐ¯←∅\\overline\{\\mathcal\{I\}\}\\leftarrow\\varnothing
while*ℐ¯≠\[d\]∨ℐ¯≠\[d\]\\underline\{\\mathcal\{I\}\}\\neq\[d\]\\lor\\overline\{\\mathcal\{I\}\}\\neq\[d\]*do

choose

𝚎𝚗𝚍𝚙𝚘𝚒𝚗𝚝∈\{ℐ∈\{ℐ¯,ℐ¯\}∣ℐ≠\[d\]\}\\mathtt\{endpoint\}\\in\\\{\\mathcal\{I\}\\in\\\{\\underline\{\\mathcal\{I\}\},\\overline\{\\mathcal\{I\}\}\\\}\\mid\\mathcal\{I\}\\neq\[d\]\\\}
if*𝚎𝚗𝚍𝚙𝚘𝚒𝚗𝚝=ℐ¯\\mathtt\{endpoint\}=\\underline\{\\mathcal\{I\}\}*then

choose

k∈\[d\]∖ℐ¯k\\in\[d\]\\setminus\\underline\{\\mathcal\{I\}\}J←I−\[δ​𝐞k,𝟎\]J\\leftarrow I\-\[\\delta\\mathbf\{e\}\_\{k\},\\mathbf\{0\}\]
if*⊧𝒮J,𝒩\\models\\mathscr\{S\}\_\{J,\\mathcal\{N\}\}*then

ℐ¯←ℐ¯∪\{k\}\\underline\{\\mathcal\{I\}\}\\leftarrow\\underline\{\\mathcal\{I\}\}\\cup\\\{k\\\}
continue

//Stop expanding this coordinate

end if

end if

else

choose

k∈\[d\]∖ℐ¯k\\in\[d\]\\setminus\\overline\{\\mathcal\{I\}\}J←I\+\[𝟎,δ​𝐞k\]J\\leftarrow I\+\[\\mathbf\{0\},\\delta\\mathbf\{e\}\_\{k\}\]
if*⊧𝒮J,𝒩\\models\\mathscr\{S\}\_\{J,\\mathcal\{N\}\}*then

ℐ¯←ℐ¯∪\{k\}\\overline\{\\mathcal\{I\}\}\\leftarrow\\overline\{\\mathcal\{I\}\}\\cup\\\{k\\\}
continue

//Stop expanding this coordinate

end if

end if

I←JI\\leftarrow J
//Keep the expansion only if it is sound

end while

Algorithm 3Non\-DeterministicExpansionInput:an interval

\[−ℓ,𝒖\]\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\],

ℓ,𝒖≥𝟎\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\\geq\\mathbf\{0\}, s\.t\.

\[−ℓ,𝒖\]⊆𝒟\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\subseteq\\mathcal\{D\}\.

Output:a maximally sound interval

\[−ℓ,𝒖\]\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\.

for*i∈\[d\]i\\in\[d\]*do

𝚕𝚘𝚠,𝚑𝚒𝚐𝚑←0,U¯i\\mathtt\{low\},\\mathtt\{high\}\\leftarrow 0,\\underline\{U\}\_\{i\}
//expandii\-th lower\-bound

while*𝚑𝚒𝚐𝚑−𝚕𝚘𝚠\>δ\\mathtt\{high\}\-\\mathtt\{low\}\>\\delta*do

ℓi←𝚕𝚘𝚠\+\(𝚑𝚒𝚐𝚑−𝚕𝚘𝚠\)/2\\ell\_\{i\}\\leftarrow\\mathtt\{low\}\+\(\\mathtt\{high\}\-\\mathtt\{low\}\)/2
if*𝒮\[−ℓ,𝐮\],𝒩​\(𝐱\)\\mathscr\{S\}\_\{\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\],\\mathcal\{N\}\}\(\\mathbf\{x\}\)*then

𝚕𝚘𝚠←ℓi\\mathtt\{low\}\\leftarrow\\ell\_\{i\}
end if

else

𝚑𝚒𝚐𝚑←ℓi\\mathtt\{high\}\\leftarrow\\ell\_\{i\}
end if

end while

ℓi←𝚕𝚘𝚠\\ell\_\{i\}\\leftarrow\\mathtt\{low\}
𝚕𝚘𝚠,𝚑𝚒𝚐𝚑←0,U¯i\\mathtt\{low\},\\mathtt\{high\}\\leftarrow 0,\\overline\{U\}\_\{i\}
//expandii\-th upper\-bound

while*𝚑𝚒𝚐𝚑−𝚕𝚘𝚠\>δ\\mathtt\{high\}\-\\mathtt\{low\}\>\\delta*do

ui←𝚕𝚘𝚠\+\(𝚑𝚒𝚐𝚑−𝚕𝚘𝚠\)/2u\_\{i\}\\leftarrow\\mathtt\{low\}\+\(\\mathtt\{high\}\-\\mathtt\{low\}\)/2
if*𝒮\[−ℓ,𝐮\],𝒩​\(𝐱\)\\mathscr\{S\}\_\{\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\],\\mathcal\{N\}\}\(\\mathbf\{x\}\)*then

𝚕𝚘𝚠←ui\\mathtt\{low\}\\leftarrow u\_\{i\}
end if

else

𝚑𝚒𝚐𝚑←ui\\mathtt\{high\}\\leftarrow u\_\{i\}
end if

end while

ui←𝚕𝚘𝚠u\_\{i\}\\leftarrow\\mathtt\{low\}
end for

return*\[−ℓ,𝐮\]\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]*

Algorithm 4Sequential Dichotomic Expansion###### Proposition 1

TheSequential Dichotomic Expansionalgorithm satisfies Lemma[8](https://arxiv.org/html/2607.08773#Thmdefinition8)\. Moreover, the algorithm terminates afterO\(d⋅log\(𝒜\(𝔽\)\)O\(d\\cdot\\log\(\\mathcal\{A\}\(\\mathbb\{F\}\)\)𝒮I,𝒩​\(⋅\)\\mathscr\{S\}\_\{I,\\mathcal\{N\}\}\(\\cdot\)oracle calls\.

###### Proof

Let\[−ℓ,𝒖\]\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]be the interval returned by theSequential Dichotomic Expansionalgorithm\. We assume that\[−ℓ,𝒖\]⊂𝔽\[\-\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\]\\subset\\mathbb\{F\}\. We prove that Lemma[8](https://arxiv.org/html/2607.08773#Thmdefinition8)is satisfied for theii–th coordinate of𝒖\\boldsymbol\{u\}\. The case for the other coordinates of𝒖\\boldsymbol\{u\}and the coordinates ofℓ\\boldsymbol\{\\ell\}are symmetrical\.

Consider the interval\[𝚕𝚘𝚠,𝚑𝚒𝚐𝚑\]\[\\mathtt\{low\},\\mathtt\{high\}\]of step[4](https://arxiv.org/html/2607.08773#algorithm4)\. We show that if there is a counterexample in\(0,U¯i\]\(0,\\underline\{U\}\_\{i\}\], there is always a counterexample in\(𝚕𝚘𝚠,𝚑𝚒𝚐𝚑\]\(\\mathtt\{low\},\\mathtt\{high\}\], throughout the execution of the algorithm\. Let𝚕𝚘𝚠j\\mathtt\{low\}\_\{j\},ui​ju\_\{ij\},𝚑𝚒𝚐𝚑j\\mathtt\{high\}\_\{j\}denote the values of the variables, of thejj–th iteration\. We prove this fact using induction\.

For the base step,\[𝚕𝚘𝚠0,𝚑𝚒𝚐𝚑0\]=\[0,U¯i\]\[\\mathtt\{low\}\_\{0\},\\mathtt\{high\}\_\{0\}\]=\[0,\\overline\{U\}\_\{i\}\]\. From our assumption, there is a counterexample𝐱a∈\[𝚕𝚘𝚠0,𝚑𝚒𝚐𝚑0\]\\mathbf\{x\}^\{a\}\\in\[\\mathtt\{low\}\_\{0\},\\mathtt\{high\}\_\{0\}\]\. Now assume that there is a counterexample in\[𝚕𝚘𝚠j,𝚑𝚒𝚐𝚑j\]\[\\mathtt\{low\}\_\{j\},\\mathtt\{high\}\_\{j\}\]\. We show that there is a counterexample in\[𝚕𝚘𝚠j\+1,𝚑𝚒𝚐𝚑j\+1\]\[\\mathtt\{low\}\_\{j\+1\},\\mathtt\{high\}\_\{j\+1\}\]\. Consider the variableui​\(j\+1\)u\_\{i\(j\+1\)\}at the\(j\+1\)\(j\+1\)–th iteration of the algorithm\. It holdsui​\(j\+1\)=𝚕𝚘𝚠j\+\(𝚑𝚒𝚐𝚑j−𝚕𝚘𝚠j\)/2u\_\{i\(j\+1\)\}=\\mathtt\{low\}\_\{j\}\+\(\\mathtt\{high\}\_\{j\}\-\\mathtt\{low\}\_\{j\}\)/2\. We take two cases, either there is a counterexample in\[𝚕𝚘𝚠i,ui​\(j\+1\)\]\[\\mathtt\{low\}\_\{i\},u\_\{i\(j\+1\)\}\], or not\.

If there is a counterexample in\[𝚕𝚘𝚠j,ui​\(j\+1\)\]\[\\mathtt\{low\}\_\{j\},u\_\{i\(j\+1\)\}\], then𝚕𝚘𝚠j\+1=𝚕𝚘𝚠j\\mathtt\{low\}\_\{j\+1\}=\\mathtt\{low\}\_\{j\}\. Moreover,𝚑𝚒𝚐𝚑j\+1=ui​\(j\+1\)\\mathtt\{high\}\_\{j\+1\}=u\_\{i\(j\+1\)\}\. Hence, exists a counter example in\[𝚕𝚘𝚠j\+1,𝚑𝚒𝚐𝚑j\+1\]\[\\mathtt\{low\}\_\{j\+1\},\\mathtt\{high\}\_\{j\+1\}\]\. Thus, we showed the desideratum\.

Now, we consider the case that there is no counterexample in\[𝚕𝚘𝚠j,ui​\(j\+1\)\]\[\\mathtt\{low\}\_\{j\},u\_\{i\(j\+1\)\}\]\. But, from the inductive hypothesis, there is a counterexample in\[𝚕𝚘𝚠j,𝚑𝚒𝚐𝚑j\]\[\\mathtt\{low\}\_\{j\},\\mathtt\{high\}\_\{j\}\]\. Therefore, there must be a counterexample in\[ui​\(j\+1\),𝚑𝚒𝚐𝚑j\]\[u\_\{i\(j\+1\)\},\\mathtt\{high\}\_\{j\}\]\. In this case, we have𝚕𝚘𝚠j\+1=ui​\(j\+1\)\\mathtt\{low\}\_\{j\+1\}=u\_\{i\(j\+1\)\}and𝚑𝚒𝚐𝚑j\+1=𝚑𝚒𝚐𝚑j\\mathtt\{high\}\_\{j\+1\}=\\mathtt\{high\}\_\{j\}\. Thus, there still exists a counterexample in\[𝚕𝚘𝚠j\+1,𝚑𝚒𝚐𝚑j\+1\]\[\\mathtt\{low\}\_\{j\+1\},\\mathtt\{high\}\_\{j\+1\}\]\.

From the step[4](https://arxiv.org/html/2607.08773#algorithm4)of the algorithm, the procedure terminates when𝚑𝚒𝚐𝚑−𝚕𝚘𝚠≤δ\\mathtt\{high\}\-\\mathtt\{low\}\\leq\\delta\. Moreover,ℓi=𝚕𝚘𝚠\\ell\_\{i\}=\\mathtt\{low\}\. From the above, there is a counterexample in\[𝚕𝚘𝚠,𝚑𝚒𝚐𝚑\]\[\\mathtt\{low\},\\mathtt\{high\}\]\. Thus, there is a counterexample in\[ℓ,𝒖\+δ​𝐞i\]\[\\boldsymbol\{\\ell\},\\boldsymbol\{u\}\+\\delta\\mathbf\{e\}^\{i\}\]\.

Finally, each expansion operation will take at mostlog⁡\(𝒜​\(𝔽\)\)\\log\(\\mathcal\{A\}\(\\mathbb\{F\}\)\)steps\. We makeddexpansions\. Moreover, the maximality of the returned solution is established by Lemma[8](https://arxiv.org/html/2607.08773#Thmdefinition8)\.□\\hfill\\Box

## Appendix 0\.DMore on Experimental Evaluation

In this appendix we review some additional statistics from the experiments presented in Sec\.[6](https://arxiv.org/html/2607.08773#S6), providing additional insights on the details of algorithms\.

### 0\.D\.1MNIST

![Refer to caption](https://arxiv.org/html/2607.08773v1/figures/analytics/MNIST-min-edge-len-big.png)Figure 5:Minimum edge length of the certifications computed by each algorithm, per MNIST input point\.We begin from the MNIST dataset and the corresponding MLP\. Tab\.[5](https://arxiv.org/html/2607.08773#Pt0.A4.T5)provides a detailed description of the metrics analyzed in Sec\.[6](https://arxiv.org/html/2607.08773#S6)\. For each metric, we report the*minimum \(Min\.\)*, the*average \(Avg\.\)*, and the*maximum \(Max\.\)*values\. In addition, we report the percentage of the inputs that timed out; the percentage of time consumed by the verification oracles; and the percentage of the non\-trivial solutions, returned by each algorithm\. Fig\.[5](https://arxiv.org/html/2607.08773#Pt0.A4.F5)shows the achieved*minimum edge length*for each input and algorithm\. Finally, in Tab\.[4](https://arxiv.org/html/2607.08773#Pt0.A4.T4)presents example images illustrating the computed bounds of the instance7\-4\.

BUSTDSSDETDS\+SDE𝔹\\mathbb\{B\}\-BUS𝔹\\mathbb\{B\}\-TDSLowerBound![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/complete-bu-7-4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/td-7-4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/bu-d-dfs-7-4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/td+bu-d-dfs-7-4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/complete-c-d-bu-7-4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/c-d-bu-7-4_lb.png)UpperBound![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/complete-bu-7-4_ub.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/td-7-4_ub.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/bu-d-dfs-7-4_ub.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/td+bu-d-dfs-7-4_ub.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/complete-c-d-bu-7-4_ub.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-MNIST/c-d-bu-7-4_ub.png)

Table 4:Examples of the execution of all the presented algorithms on MNIST\.From Tab\.[4](https://arxiv.org/html/2607.08773#Pt0.A4.T4), we observe that the*morphology*of each bound strongly depends on the applied algorithm\. Algorithms based on*symmetric*interval \(i\.e,ℓ∞\\ell\_\{\\infty\}\-spheres\) induce a uniform distortion on the given input\. In contrast, sequential algorithms, such asSDE, expand each pixel in turn, once further expansion of the previous pixel is no longer possible\. This results in a highly imbalanced distortion of the input image\. Finally, theTDSandBUSalgorithms lay between these two extremes\.

CPUTimeAlgorithmMin\.ValueAvg\.Max\.ValueStd Dev\.TimeoutsTimeoutPerc\. \(%\)BUS30\.2930\.29m38\.5438\.54m49\.7049\.70m5\.785\.78m00%TDS8\.978\.97m51\.1351\.13m62\.5462\.54m14\.6414\.64m282856%SDE11\.2711\.27m32\.7832\.78m67\.9567\.95m18\.0218\.02m131326%TDS\+SDE\+4\.04\+4\.04m\+42\.04\+42\.04m\+65\.72\+65\.72m14\.6414\.64m2550%𝔹\\mathbb\{B\}–BUS2\.822\.82s3\.923\.92s4\.834\.83s0\.550\.55s00%𝔹\\mathbb\{B\}–TDS1\.051\.05s21\.0621\.06s149\.26149\.26s27\.2727\.27s00%NumberofOracleCallsBUS17942085\.732529172\.391\.06s96%TDS17113753\.024862708\.150\.78s95%SDE12722963\.86326155\.280\.64s95%TDS\+SDE\+10\+1030\.55\+2569\+927\.372\.41s98%𝔹\\mathbb\{B\}–BUS44400\.94s99%𝔹\\mathbb\{B\}–TDS44400\.93s95%Min\.EdgeLengthα​\(⋅\)\\alpha\(\\cdot\)BUS0\.90\.991\.00\.021122%TDS00\.130\.40\.084896%SDE0\.00\.00\.00\.000%TDS\+SDE0\.00\.10\.40\.14896%𝔹\\mathbb\{B\}–BUS0\.940\.940\.940\.04998%𝔹\\mathbb\{B\}–TDS0\.00\.070\.190\.053672%

Table 5:Additional Analytics for the MNIST dataset\.
### 0\.D\.2Fashion MNIST

![Refer to caption](https://arxiv.org/html/2607.08773v1/figures/analytics/Fashion-MNIST-min-edge-len-big.png)Figure 6:Minimum edge length of the certifications computed by each algorithm, per Fashion MNIST input point\.Subsequently, we focus on the Fashion MNIST dataset and the corresponding MLP\. Tab\.[7](https://arxiv.org/html/2607.08773#Pt0.A4.T7)provides a detailed description of the metrics used, reporting the*minimum*, the*average*,*maximum\)*values, along with its*standard deviation*, similar to Tab\.[5](https://arxiv.org/html/2607.08773#Pt0.A4.T5)\. In addition, we report several percentage\-based metrics\. Fig\.[6](https://arxiv.org/html/2607.08773#Pt0.A4.F6)reports the achieved*minimum edge length*obtained for each input and algorithm\. Finally, Tab\.[6](https://arxiv.org/html/2607.08773#Pt0.A4.T6)presents example images illustrating the computed bounds of the instance7\-4\.

From Fig\.[6](https://arxiv.org/html/2607.08773#Pt0.A4.F6), we observe that theBUSalgorithm*fails*to compute a correct complete certification, whereas𝔹\\mathbb\{B\}\-BUSsucceeds\. We attribute this behavior toBUS’s sensitivity to the precision parameterδ\\delta\. As shown in Tab\.[6](https://arxiv.org/html/2607.08773#Pt0.A4.T6), theBUSalgorithm behaves well; the small value ofα\\alphais due to the involvement of only a few pixels\.

BUSTDSSDETDS\+SDE𝔹\\mathbb\{B\}\-BUS𝔹\\mathbb\{B\}\-TDSLowerBound![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/complete-bu-7_4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/td-7_4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/bu-d-dfs-7_4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/td+bu-d-dfs-7_4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/complete-c-bu-d-7_4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/c-bu-d-7_4_lb.png)UpperBound![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/complete-bu-7_4_ub.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/td-7_4_ub.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/bu-d-dfs-7_4_ub.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/td+bu-d-dfs-7_4_ub.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/c-bu-d-7_4_lb.png)![[Uncaptioned image]](https://arxiv.org/html/2607.08773v1/figures/examples-Fashion-MNIST/c-bu-d-7_4_ub.png)

Table 6:Examples on Fashion MNIST\.CPUTimeAlgorithmMin\.ValueAvg\.Max\.ValueStd Dev\.TimeoutsTimeoutPerc\. \(%\)BUS17\.1m23\.82m30\.87m3\.45m00%TDS13\.48m50\.17m61\.15m15\.31m3264%SDE10\.38m22\.82m60\.03m13\.27m36%TDS\+SDE\+6\.52m\+23\.91m\+60\.01m13m12%𝔹\\mathbb\{B\}–BUS2\.42s3\.52s4\.47s0\.63s00%𝔹\\mathbb\{B\}–TDS0\.76s5\.15s28\.48s6\.1s00%NumberofOracleCallsBUS987\.121375\.411782\.78200\.991\.11s96%TDS13433272\.765062724\.220\.88s95%SDE14503469\.484040390\.510\.36s92%TDS\+SDE\+819\+1779\.34\+2757386\.360\.77s96%𝔹\\mathbb\{B\}–BUS4440\.00\.85s96%𝔹\\mathbb\{B\}–TDS4440\.01\.26s98%Min\.EdgeLengthα​\(⋅\)\\alpha\(\\cdot\)BUS0\.10\.10\.10\.050100%TDS0\.00\.180\.50\.114896%SDE0\.00\.00\.00\.000%TDS\+SDE0\.00\.180\.50\.114896%𝔹\\mathbb\{B\}–BUS0\.940\.940\.940\.050100%𝔹\\mathbb\{B\}–TDS0\.00\.120\.310\.084488%

Table 7:Additional Experimental Statistics for the Fashion MNIST dataset\.