LEVIS: Large Exact Verifiable Input Spaces for Neural Networks
Authors: Mohamad Fares El Hajj Chehade
WENTING LI
Brian Wesley Bell
Russell Bent
Saif R. Kazi
Hao Zhu
Venue: ICML 2025 poster (2025)
Keywords: robustness of neural networks
verifiable input space
adversarial examples
mixed-integer programming
Primary area: deep_learning->robustness
TL;DR: We propose LEVIS, a set of algorithms to locate a large verifiable input space for neural networks.

Abstract: The robustness of neural networks is crucial in safety-critical applications, where identifying a reliable input space is essential for effective model selection, robustness evaluation, and the development of reliable control strategies. Most existing robustness verification methods assess the worst-case output under the assumption that the input space is known. However, precisely identifying a verifiable input space $ \mathcal{C} $, where no adversarial examples exist, is challenging due to the possible high dimensionality, discontinuity, and non-convex nature of the input space. To address this challenge, we propose a novel framework, **LEVIS**, comprising **LEVIS-$\alpha$** and **LEVIS-$\beta$**. **LEVIS-$\alpha$** identifies a single, large verifiable ball that intersects at least two boundaries of a bounded region $ \mathcal{C} $, while **LEVIS-$\beta$** systematically captures the entirety of the verifiable space by integrating multiple verifiable balls. Our contributions are fourfold: we introduce a verification framework, **LEVIS**, incorporating two optimization techniques for computing nearest and directional adversarial points based on mixed-integer programming (MIP); to enhance scalability, we integrate complementary constrained (CC) optimization with a reduced MIP formulation, achieving up to a 17-fold reduction in runtime by approximating the verifiable region in a principled way; we provide a theoretical analysis characterizing the properties of the verifiable balls obtained through **LEVIS-$\alpha$**; and we validate our approach across diverse applications, including electrical power flow regression and image classification, demonstrating performance improvements and visualizing the geometric properties of the verifiable region.

LEVIS:
Large Exact Verifiable Input Spaces for Neural Networks
Mohamad Chehade 12 Wenting Li Brian W. Bell 2 Russell Bent 2 Saif R. Kazi²
Hao Zhu'
Abstract
image classification, demonstrating performance improvements and visualizing the geometric prop-
The robustness of neural networks is crucial in safety-critich applications, where identifying re- liable input space is essential for effective model selection, robustness evaluation, and the devel- opment of reliable control strategies. Most ex- isting robustness verification methods assess the worst-case output under the assumption that the input space known. However, precisely identi- fying verifiable input space C, where adver- sarial examples exist, is challenging due to the possible high dimensionality, discontinuity, and non-convex nature of the input space. To address this challenge, we propose a novel framework, LEVIS, consisting of LEVIS-Ee a and LEVIS 3. LEVIS-a identifies single, large verifiable ball that intersects least boundaries of a bounded region C. In contrast, LEVIS-B sys- tematically captures the entirety of the verifiable space by integrating multiple verifiable balls. Our contributions are fourfold: (1) We introduce a ver- ification framework, LEVIS, incorporating two optimization techniques for computing nearest and directional adversarial points based on mixed- integer programming (MIP). (2) To enhance scal- ability, we integrate complementarity-oe constrrattt (CC) optimization with a reduced MIP formula- tion, achieving up to a 6-fold reduction in runtime while approximating the verifiable region in a principled manner. (3) We provide a theoretical analysis characterizing the properties of the veri- fiable balls obtained through LEVIS-a. (4) We validate our approach across diverse applications, including electrical power flow regression and
erties of the verifiable region.
1. Introduction
Despite the remarkable growth and transformative impact of neural network models, their deployment safety-critical domains remains limited. An example is neural network- based controllers for electric inverters that have significant potential to support the integration of renewable energy resources (Cui et al., 2022). These applications demand ex- tremely high accuracy and reliability, as even minor errors can lead to millions of dollars in economic losses or large- scale power grid failures. However, neural networks are inherently vulnerable data variations, including both natu- ral perturbations and adversarial attacks. For instance, slight noise added to input data can lead to significant misclassifi- cation errors (Goodfellow et al., 2015). Even state-of-the-an foundation models can achieve less than 80% accuracy when evaluated on perturbed inputs (Liu et al., 2023).
One promising approach to addressing these robustness challenges is neural network verification. Most existing re- search focuses verifying whether the outputs of a neural network satisfy specific worst-case criteria within a prede- fined input domain (Tjeng et al., 2019; Gowal et al., 2018 8). Techniques range from transforming nonlinear activations into integer constraints to compute worst-case outputs, to using linear (Wang & et.al., 2021) or quadratic (Kuvshinov & Günnemann, 2022) relaxations to estimate bounds. Ad- vanced methods further integrate optimization techniques like bound tightening and leverage parallelism for speedup (Zhang et al., 2022). However, these approaches typically assume the input domain is predefined and do not explicitly evaluate the structure of the input space itself, potentially leading to under- or over-estimations of robust input regions.
Equua contribution !Chandra Department of Electrical and Computer Engincering, The University Texas at Austin, Austin, TX, USA "Los Alamos National Labora- tory. Los Alamos, NM, USA. Correspondence to: Mo- hamad Chehade <chehade @ utexas.edu>>, Wenting Li <weet- ing@ gog@lanlggo>>, Brian W. Bell <bwbell@lanl.gov Russell Bent <rbent@ lanl. gov>,, Saif R. Kazi <skaziie lanl. gov>, Hao Zhu <haozhu udux
As illustrated in Figure 1, the verifiable input space con- tains all inputs given specification, such as f(x) > 0 (shown by the red boundary). However, C is often non-convex, discontinuous, and high-dimensional, making difficult to characterize precisely. Early work explored the input space primarily to identify adversarial vulnerabilities (Peck et al., 2017), while
C that produce outputs satisfying
Proceedings of the 42nd International Conference Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

LEVIS: Verifiable NN Input Spaces
Input
Output
a negligible error in global optimality (experimentally within 0.004). The core idea is to reformulate ReL.U activations using CC constraints, reducing the number of integer variables in the MIP formulation.
XEC
3. We propose two search strategies: LEVIS-O, which seeks a single large verifiable ball centered in the in- terior of C, and LEVIS-3, which aggregates multiple verifiable balls cover the full verifiable input space.
Figure 1. The verifiable input space (orange) consisting of the inputs æ E C that produce outputs satisfying the condition f(x) > O, determined by the red line. Note: the left orange space may only be a subset of the pre-image of the right orange space.
4.
We evaluate our methods on two neural network ap- plications -eecctric power flow regression and image both performance gains and visual insights into the geometry of the verifiable input space.
more recent research has aimed to define verifiable input regions meeting physical or aceuracy- -based criteria. These include abstraction-based approaches (Matoba & Fleuret, 2020), over-approximation of verifiable regions (Kotha et al., 2024; Sundar et al., 2023), and probabilistic verification techniques (Grunbacher et al., 2021: Bell et al., 2025). Nev- ertheless, the task of precisely identifying input regions that are entirely free of adversarial points remains largely unexplored.
2. Background and Related Work
Preliminary Notation. We use C and V to denote the veri- fiable region and the union of verifiable balls, respectively. Bic) represents a ball centered at c. The vector e is a standard basis vector where the k-th position is and all others are 0. The ||жн|μ norm is defined as (E /2, for = 1,2, and || = max, |zz]]. We define an L- layer rectified linear (ReL.U) neural network, where layer (for i 1,..., L) uses weights W E Rd, xd.- and biases 3 E Rd. The pre-activation and aost-activation outputs for layer i are given by 2 = W + B and 2 = (2') = max(2', 0), respectively. The input 2 equals the input data x E Rdo, and the output of the network is f(x) = x² E Rd
To address this gap, we propose a novel framework, LEVIS (Large and Exact Verifiable Input Spaces), to identify verifi- able input regions for neural networks. LEVIS consists of two algorithms: LEVIS-Q and LEVIS-B. LEVIS-a identi- fies a single, large verifiable ball that intersects the true space at two boundaries, capturing substantial region guaran- teed to be verifiable. In contrast, LEVIS-3 extends this idea by constructing collection of verifiable balls to cover the entire input space, which may be nigh-dimessional, non- convex, and discontinuous. Importantly, every point in the regions identified by LEVIS is guaranteed to satisfy the given verification criteria.
Bounds on the Output Domain: Verification of Neural Networks. Bounding the outputs of neural networks (NNs) is effective strategy for verifying robustness and enhane- ing model reliability. In standard verification, given an input region S, the output must satisfy predefined specification 'P to ensure safety or correctness. This is typically framed as an optimization problem: find f = minges f(x), sub- ject to 20 x, 2² Wi + 8 and 인² max(2 0) for i 1, 1,..,, L. The input domain is defined as S = (x | zo x S e). and the network is considered verified if the condition p { 0} holds.
To this end, we develop a new optimization framework that computes the largest verifiable ball at a given center, lo- cates adversarial points along specific directions, and scales effectively to large-scale problems. Our contributions are summarized as follows:
1. We develop a novel optimization framework to accu- rately locate the largest verifiable ball centered at a known input xy E IR", using mixed-integer program- ming (MIP) with global optimality guarantees. We fur- ther incorporate directional constraints into the frame- work to locate adversarial points along specific direc- tions.
Verification of neural networks is NP-complete, primarily due to nonlinear activation functions. Solution approaches can be categorized into three types: exact or complete ver- ifiers (Tjeng et al., 2019), approximate or incomplete ver- ifiers (Gowal et al., 2018: Wang & et.al., 2021), and prob- abilistic verifiers (Grunbacher et al., 2021; Marzar et al., 2024). Unlike these methods, which focus on confirming output correctness for a known input domain, our work prioritizes input domain analysis to identify the largest pos- sible region that yields verifiable outputs, ensuring all points within this region meet the satisfaction criteria.
2. To enhance scalability, propose complementarity- constrained (CC) relaxation that formulates an approx- imate verifier. Unlike other approximate methods, our approach explicitly characterizes the conditions under which the solution remains globally optimal. This re- laxation achieves up to a 6x speedup while maintaining
2

---

LEVIS: Verifiable NN Input Spaces
Bounds the Input Domain: Robustness to Adversar- ial Perturbations. Inputs that, when perturbed, result in erroncous neural network outputs are termed adversarial ex- amples. The subset of inputs free from adversarial examples forms the verifiable inpul region, which is crucial for robust model selection and training (Kuvshinov & Günnemann, 2022; Li et al., 2023). Early works primarily focused on measuring the maximum perturbation magnitudes that in- duce adversarial examples rather than characterizing the global structure of the verifiable input region (Kuvshinov & Günnemann, 2022). A recent approach approximates the input space using a convex hull derived via bound propaga- tion techniques (Kotha et al., 2024). However, this method results in an over-approximation of the verifiable region, meaning that some points within the convex hull may not actually be verifiable.
finding x" is structured as follows:
min
| cll
(la)
subject to
0 = x
(1b)
2' Wi
+ tB¹, i= 1=,,..., L
(1c)
200 - o(2(),,
i i=1,..,,--
(1d)
f(x) = st [(x) 0O
(1c)
(1f)
Equation (1f) ensures the solution violates the specified output condition, i.e., a adversarial. The objective (la) minimizes the fp-norm distance from the center c, seeking the nearest such adversarial point.
To solve this nonlinear program, we leverage mixed- integer programming (MIP) formulation by explicitly encod- ing the ReLU activation functions. ReLU is a piecewise lin- car function: for & = ReLU(W < +b). we have 2 = W2+ b if W + 2 O, and & = 0 otherwise. This behavior can be encoded in a MIP by introducing a binary variable a, where 0 otherwise. Using the
3. Problem Formulation
A verifiable space comprises input data points for neural networks that consistently yield verifiable outputs. Pre- cisely identifying large verifiable spaces is crucial for model selection, robustness evaluation, and safe control opera- tions (Kotha et al., 2024). The challenge lies in maximizing the verifiable input space C, where all data points in C' gen- erate outputs that satisfy verification guarantees. This objec- tive can be formalized as maxe minsec (1) > O, which defines a fundamentally intractable min-max optimization problem, especially when C is non-convex.
if W + b 2 0 and Big-M method, this conditional logic is translated into set of linear constraints, thereby enabling the global optimiza- tion of ReLU networks using standard MILP solvers (Tjeng et al., 2019). Similar formulations have been used for prov- ing equivalence between networks (Kleine Büning et al., 2020) and for finding the closest input that yields target label (Szegedy et al., 2014).
To manage this complexity, we propose approximating the verifiable space using one or more verifiable balls. Each ball is defined by center and radius such that all data points within it produce verifiable outputs when passed through the neural network. Crucial to our approach is the identification of centers and radii that ensure (1) the verifiability of all interior points under specified conditions, and (2) scalability to high-dimensional, non-convex input regions.
The verifiable ball, denoted as B(c), is characterized by the center and radius r ||- - -llp- All points inside B(e) are guaranteed to produce verifiable outputs, with x" repre- senting the closest violation. To improve the scalability of the MIP solver, we propose hybrid approach that integrates efficient nonlinear programming (NLP) with a reduced MIP formulation, achieving both computational efficiency and guaranteed optimality.
4. Proposed Approach
4.2. Fast Solver with complementarity Constraints
Our method begins by precisely identifying a maximal veri- fiable ball centered at a given point To, denoted as the center e, and then iteratively shifts this center to either identify a large boundary-touching verifiable ball (LEVIS-o) or as- semble a large union of such verifiable balls (LEVIS-9)..
We represent the ReLU function using complementarity constraints (CC): 0 I 3f 1 / z² 2 0, where the "1" operator enforces that at least one of the two inequalities
holds as an equality; that is, g = 0, a = 2', or both. This CC-based formulation replaces integer variables with continuous functions, enabling a more scalable neural net- work representation (Yang et al., 2022; Kilwein al., 2023). Although standard nonlinear programming (NLP) solvers can handle this formulation, they may converge to spurious stationary points with feasible descent directions (Leyffer & Munson, 2007). To mitigate this, we adopt the two-step hybrid strategy (Kazi et al., 2024), which integrates the NLP formulation with a reduced mixed- integerrer programming (MIP) approach. This strategy ensures global optimality
4.1. Find a Maximum Verifiable Input Ball around
We find the maximum verifiable ball around center e by locating the nearest adversarial data point x*. This point lies on the boundary of the verifiable input space and yields a violating output fx* S 0. The optimization problem for
3

---

LEVIS: Verifiable NN Input Spaces
under certain conditions while improving computational efficiency.
4.3. LEVIS: Large Exact Verifiable Input Spaces for Neural Networks
Specifically, let p' and q' be the complementarity variables for the ith neuron. The nonlinear optimization of (1) trans- forms into:
LEVIS employs two search strategies for identifying verifi- able balls. The key innovation lies in dynamically updating the centers based on adversarial points along different direc- tions, ensuring the verifiability of the newly selected centers. We first present the optimization formulation for computing directional adversarial points, followed by a detailed discus- (2a)
min 2,p"
(Ia)
x² = p² - q. 2² = p¹
sion on how these points guide the search trajectory across various geometric structures of the input space.
s.t.
p'q' 0, p¹.g¹ 2 0
(2b)
(Ib), (Ic)(1)
(2c)
4.3.1. DIRECTIONAL ADVERSARIAL POINT
Our LEVIS search algorithms are guided by adversarial points along specific directions, referred to as directional adversarial points. To achieve this, we incorporate direc- tional constraints into the original optimization problem in (I), which dictate the search direction. Given the center of the previous verifiable ball e and an adversarial point b, the next adversarial point b E R" is determined along, direction that forms a specified angle 0 with the vector be.
where constraints in (2b) represent a nonlinear equivalent of the ReLU function. To improve convergence behavior, we introduce a small regularization parameter E >> 0 (suggested to be 10-5), modifying the constraint to p'q' (Scholtes, 2001). This reduces the problem complexity from an NP- hard integer formulation to polynomial scaling in the num- ber of neurons, N.
However, NLP solvers may still converge to locally optimal solutions and spurious points where the bi-active set is non- empty, i.e., Lo {i p of = 0}. To address this, we classify neurons into three groups: if p} > 0 and of = O, then j E 1=: if p3 = 0 and oj > 0, then j E 12; and if p³ = of = 0, then j lg. We then construct a reduced MIP that introduces integer variables only for neurons in the set Io. balancing efficiency and optimality. This reduces the number of integer variables from N to ool. which is typically a small subset, as confirmed in Section 5.2. We assert that the solution is globally optimal and verifiable for all inputs within the ball, provided the neuron activation states active (in 4 inactive (in (L)-remain consistent with the sets 4 and T_
Precisely, we construct a general directional constraint and formulate the optimization for the directional adversarial point b in (3), where the search direction forms user- defined angle 0 with be. To define this direction, we in- troduce two orthogonal vectors d, E R": the vector d. aligned with bc, is given by d = c-b resents an orthogonal direction. It can be explicitly specified or generated by sampling random vector & ~ ~~((0, 1) and removing its component along d, yielding q = { &r4d. where the second term represents the projection of & onto d.
be- The vector rep-
Using these definitions, any direction can be expressed as (0)) = d cos (0)+ and the directional constraint for b is given by d + ko. Special cases of this formulation when 0 = 0, the constraint reduces to the collinear direction; when 0 = 90" it corresponds to the orthogonal constraint, i.e., (6-c))(b--)) = O. This formulation enables flexible directional adversarial search while maintaining mathematical rigor and generalizability.
include:
In terms of computational complexity, the NLP formulation derived from neural network verification exhibits substantial sparsity in its constraint Jacobian, owing to the localized connectivity and layered architecture of neural networks. As both the number of decision variables and constraints scale linearly with the total number of neurons, denoted by N, we characterize the overall complexity in terms of N. When solved using a sparse interior-point method such as IPOPT (Wächter & Biegler, 2006), the computational com- plexity is primarily governed by the cost of factorizing the Karush-Kuhn-Te Kuhn-Tucker (KKT) system at each iteration. This cost depends critically on the sparsity pattern and numerical properties of the constraint matrix. In favorable cases such as when the matrix has a particular structure that permits efficient factorization per-iteration cost can be reduced to (NlogN) using solvers like MA57 (Duff, 2004). In contrast, for less structured or denser matrices, the cost may grow toward O
min 6
1|b cllp
(3a)
subject to
(1b) - (1f), x x=
(3b)
b = c ko(0)
(3c)
((0) d doss()) (0) si)
(3d)
d = c b
TTd d d'd
== 5
(3c)
|| - b x
4

---

LEVIS: Verifiable NN Input Spaces
Figure 4, LEVIS-3 searches for the union of verifiable balls guided by directional adversarial points.
Figure 2. Illustration of the sequence of balls centered at the red points co. ... ,Cn obtained by LEVIS a, where the arrows point the nearest adversarial points that define the radius of those balls. The search converges at the final ball B(c,). which touches at least two boundaries of the bounded verifiable imput space.
N such that for all > -N B(c) contains two points almost symmetric about the center with less than mismmachh and these points lie on the boundary o.C.
4.3.2. (1) LEVIS-0: SEARCH FOR THE LARGE BOUNDARY-TOUCHING VERIFIABLE BALL
The rationale is that LEVIS-O progressively averages the collinear adversarial pairs (b2j+1; b25-2) using = 2d Σ by, minimizing asymmetry relative to the center in each iteration. Given that C is bounded, the search halts when at least one pair (6) touches the surface of the ball, while other pairs become symmetric with less than mismatch. Hence, the final ball intersects the boundary of at least two distinct points. The complete proof is provided in Appendix A.
The core technique of this search strategy is to average d pairs of boundary adversarial points b2j+1 and baj+2, j = d-1, obtained by solving the minimization in (1) with directional constraints. The detailed algorithm, termed LEVIS-a, is described Algorithm and illustrated in Figure 2.
Algorithm 1 LEVIS-0: Iterative Refinement for Center
LEVIS-a is suitable for exploring small, bounded verifi- able input spaces, In contrast, we introduce LEVIS-8, a more comprehensive and parallel-friendly strategy that sys- tematically identifies verifiable regions even when they are high digh-dimensional, non-convex, or discontinuous.
Estimation
1: Initialize: Given the original data æi as the ball center 2o, set r oc, Fold tolerance e >> 0, and neu- ral network parameters O (W*, Bt, 1 ., T.).
2: while rall 2 do
4.3.3. (2) LEVIS- COLLECT THE LARGE UNION OF VERIFIABLE BALLS
3: 6¹ + Solve (I), set = -bb - cllp
4: 82 t Solve (3) given and = 90
5: for = to 1 do
The innovative idea of this search strategy is to look for a verifiable new center outside the known verifiable union by exten- sively moving in all directions. Specificallyy, by solving (1) and (3), we obtain a verifiable ball ((c) centered at and nearest directional adversarial point b. Once a new ball B(c) is found, define the next center to be the point that lies the same line as and b but on the internal surface of B(c), ie..
6:
b2j+1 + Solve (3) given 12 0 = 90
7: b2j+2 + Solve (3) given b2j. 0º
8: end for
2d e. c 27 Ei=1 bi Fold 4-
9:
10: end while
11: Return c,
Figure 3. Illustration of the geometric po- sition of the surface point.
Algorithm updates the center of the verifiable hall in each iteration and eventually converges to a large exact verifiable ball in the central region of the verifiable space, touching least two adversarial points, illustrated in Figure 2. In each iteration, the algorithm searches for d pairs of adver- sarial points along collinear and orthogonal directions. The final region obtained from LEVIS-0 V-a is rigorously described below.
c b
Theorem 4.1. For any bounded verifiable region C C Rdd the sequence of balls (B(c,)} generated by LEVIS-a con- verges to a ball B(c) that intersects the boundary of at least at two points. Specifically, for any > O, there exists
m = c
[c
blpp
r,
<<>
as illustrated in Figure 3.
Our new Algorithm 2, termed LEVIS-8, preserves the ver-
5

---

LEVIS: Verifiable NN Input Spaces
Algorithm 2 LEVIS-B
rameters A, and random seeds to efficiently discover the full verifiable input space, discussed in Section 5.7.
1: Initialize: Given one data point z0 and label yo. the in- put bounds [1, ai), tolerance > O, shift factor y = 0.99, trained neural network parameters + {W*, 13,
5. Experiments
1.....4) L), step size A, angle 0, and random seed. 2: Initialize the set of verifiable balls V 0, let c
We implement our algorithms on two benchmark systems designed to meet specific requirements for physical con- straints and robust accuracy. We employ three-layer dense neural networks model solutions for both optimal power flow (regression) and image classification tasks.
+ A, and initialize the queue Q = {c}
3: while Q is not empty do
4: Pop the first element of Q as c; solve (1) to obtain the radius r centered at e with corresponding adver- sarial point 6.
For the optimal power flow (OPF) problem, we generate a direct-current (DC) power flow dataset, denoted as Dj = {( (Ix))*s) Zyk E R 3/k E R31 1000, /= using the IEEE 9- bus power grid benchmark a widely recognized model for simulating energy flow in power systems. The specification for DC-OPF requires the network output remain within a predefined limit Ymax. i..., f(xx) S y%
5: if < then
6:
Sample point from either the range [1, c] or [c, u] and iteratively resample until it is verifiable. Add this point to Q.
7:
8:
else
9:
Update the set V Vu r(..
10:
Solve (3) along the direction 6(0) to find the direc- tional adversarial point b.
For image classification, we utilize the MNIST (LeCun et al., 2010) and CIFAR-10 (Krizhevsky et al., 2009) datasets. MNIST consists of 60,000 training and 10,000 testing sam- ples with an input dimension of 784, while CIFAR- 10 in- cludes 50,000 training and 10,000 testing samples with an input dimension of 3,072. The robustness requirement man- dates that the predicted probability of the ground-truth class must be higher than that of an adversarial class I, for- mulated as: f(xxx) j - f(xxx): / > 0. Further details on the datasets are provided in Appendix B.
11:
Compute the surface point: m c- b--b
12:
Terminate the search if m & [L. u). otherwise add m to Q
13:
while m E and |Im - b12 > do
14:
m (m + /
15:
end while
16:
end if
17:
end while
Return
To solve the mixed intteerrreeerrrr programming (MIP) problems in (1) and (3), we Gurobi with OMLT (Ceccon et al., 2022) for small neural networks (fewer than 100 neurons) trained DC-OPF datasets. For large-scale MNIST and CIFAR- 10 networks, we adopt the Complementary Constraints (CC) approach (Section 4.2), employing Ipopt (Wächter & Biegler, 2006) for the NLP formulation and Gurobi for the reduced MIP. All optimization models are implemented using Pyomo (Hart al., 2024).
ifiability of the center while exploring multiple directions to identify external balls beyond the known union. Step 6 prevents the search from getting stuck at discontinuous or local boundaries before reaching the full extent of the input space, effectively addressing the discontinuity challenge in C. Steps 10-12 update the center using the surface point in the (0)) direction, ensuring both feasibility (i.e., m E 11, u)) and that m lies within a verifiable ball. Steps 13-15 refine m by nudging toward b if it overlaps with the existing union.
5.1. Visualization of the Exact Verifiable Ball
Figure illustrates the verifiable balls for different E, norms (p = 1, 2, oo) using the DC-OPF dataset in 3D. The anal- ysis provides key insights into selecting p and refining the search strategy. Notably, the volumes of these balls vary significantly, with the Lx norm producing the largest. We choose p = oo because its cube-shaped geometry minimizes gaps when adjacent cubes intersect, enhancing coverage. Al- though our solution to (1) guarantees verifiability within the ball, points equidistant from 2o to x may still be adver- sarial, potentially appearing anywhere the surface. This highlights the challenge of expanding verifiable regions via vertex enumeration. Instead, our method explores optimal directions to identify new verifiable balls, improving both coverage and efficiency.
Figure 4 illustrates the expansion of the union over iterations, where blue lines indicate search directions and red circles represent verifiable balls.
We assert that the new center e remains a verifi- able point throughout the execution of Algorithm Since 6 is the nearest adversarial point along the direction ((9), any point closer to the original center e along this direction remains verifiable. The surface point computed in Steps 10-12 satisfies this condition. Moreover, because each new center e is located outside the existing union of verifiable balls, the union's 's total volume expands progressively during the search. Notably, LEVIS-B can be executed in parallel across multiple directions with varying angles 0, shift pa-
Remark:
6

---

LEVIS: Verifiable NN Input Spaces
We train neural networks regress optimal power flow solutions and compare the verifiable radius from our method (solving the NLP in (I)-(1f) against the Lipschitz-based bound.
Lm norm
L norm
f norm
Ixx x0 16.21
1x x 47.28
||x" xal12 28.12
Due to the inherent randommess in training neural networks, we repeat the experiment across five independently trained models and report the resulting range of radius values. This repetition ensures robustness of the comparison across dif- ferent training instances.
Pin
Pi
Pin
Fis
Chetse (125, 90, 100)
Adversurial Point (172.23, 90, 100.05)
Table shows that our method consistently finds verifiable balls with radii up to 10x larger than those estimated by the baseline, underscoring the benefit of solving the exact optimization problem directly.
Figure 5. Single maximum verifiable balls obtained by solving (1) with different& lp norms using the DC-OPF dataset. The center is atu [125, 90, 100), with the nearest adversarial points x" marked as red nodes. The radius, given by ||x= - wollp- represents the smallest distance between and x". In the 3D input space, the verifiable regions for fo l1, and le norms (left to right) corre- spond to cube, octahedron, and sphere, respectively.
Table 2. Comparison of radii from the exact solver vs. Lipschitz- based lower bound for the DC-OPF network.
Method
p 0C
p
1
p
2
5.2. Efficiency Comparison
Baseline r
4.52
4.80
12.88
We evaluate the runtime of solving the optimization prob- lem in (1) and compare our method against a strengthened MIP baseline that uses bounds from the CROWN method. Experiments are conducted on image recognition datasets (MNIST and CIFAR-I0) using a three-layer ReLU network with 894 neurons.
Our r
16.24
47.28
28.12
5.4. Performance of LEVIS aa for DC-OPF
We implement LEVIS-a for the DC-OPF task and track the variations in the radius of verifiable balls, as shown in Figure 6. Each solid blue line denotes the mean radius across five random implementations of LEVIS-O, and the shaded regions represent standard deviations.
Table 1. Runtime (seconds) and relative speedup (in parentheses) for each method. Speedup relative to the MIPcROwN baseline.
Dataset CROWN (s) Proposed (s) Optimality Gap
Similar behavior is observed for other norms (p = 1,2). To demonstrate the substan- tial size of the final verifiable ball obtained by LEVIS-a, we compare it against two al- ternative methods: the Exact Fixed Center (EFC) method from (1), and a version of the Lipschitz- based Lower Bound (LLB) method (Fazlyab et al., 2021). Two key observations emerge: (1) LEVIS-O a yields radii 3-9x larger than the baselines, justifying its iterative center refinement in Algo- rithm 1; and (2) the radius converges, suggesting that the final ball touches two distinct edges of the verifiable region.
MNIST
10.48
1.34 (7.82x)
0.004
CIFAR-10
17.47
5.96 (2.93x) 0.0009
30
20
As shown in Table 1, the proposed method significantly improves efficiency compared to the MIP baseline, achieving a 7.82x speedup on MNIST and 2.93x speedup on CIFAR-10. Our solver (Section 4.2) solves each instance in 1.34 seconds on MNIST and 5.96 seconds on CIFAR-10, 10, while maintaining small optimality gap. The total runtime includes both nonlinear programming (NLP) phase and reduced MIP phase.
30
20
30
Figure 6. Radius over itera- tions for E.
5.3. Comparison of Radius Size with the Baseline
We compare the size of the verifiable ball obtained by our method with baseline method based on Lipschitz con- stants (Fazlyab et al., 2021). As neural networks are Lips- chitz continuous with constant = I || we can estimate a lower bound on the adversarial radius as
5.5. Performance of LEVIS-3 for DC-OPF
We evaluate the statistical behavior of LEVIS-3 on the DC-OPF task. Across iterations, LEVIS-3 discovers ver- ifiable balls of varying radii, with smaller balls appearing farther from the original center and closer to the bound- ary of the verifiable region. Figure 7(a) shows a histogram
8 .. -clp= 2
1
where ò min 17k
(ex (ex-es) f(()).
V2
7

---

LEVIS: Verifiable NN Input Spaces
Freqency
W K
10-
10
12
Distance to Orignnll Center (infinity Norm
150
200
250
300
550
400
Redius
Figure 9. t-SNE projection of verifiable ball centers under different search directions {0, 90, 180, 270 (left) and initialization shifts A {0, 0.02, 0.04, 0.06, 0.08) (right), with 10 runs per setting.
Figure 7. Radii distribution for LEVIS-B: (a) histogram of radii; (b) radii vs. distance to initial center. Smaller-radius balls tend to lie near the boundary of the verifiable region.
5.7. Geometric Characteristics of the Verifiable Input Space
0.06
Redg
0,06
Rontos Value
Ratius Veluee
0.04
Unlike over- under-approximation methods, each verifi- able ball in LEVIS-3 is exactly verified and adversarial-fre free. This allows us recover structural insights into the geom- etry of the input space. Figure 9 shows t-SNE projections of verifiable centers based on varying (left) and A (right). The four clusters in Figure 9(eft) reflect the orthogonal directions used in the search and suggest regularity the structure of the verifiable region. In contrast, Figure (right) shows that changing A leads denser but distinguishable center clusters. Together, these plots highlight the struc- tural diversity and robustness of our method in exploring the verifiable space.
0.02
0.02
0.00
0,00
0.95
1.00
1.10
1.10 Distance Original Center (infinity
1.05
Distance Original Center (Infinitt Nor
Figure& 8. Radii distribution from LEVIS-$ & for different directions 8 E {0, 90, 180, 270, 360") } (left) and initialization values A E {0.02, 0.04, 0.06, 0.08} with 10 random seeds per A (right).
of radii, while (b) plots each radius against its distance to the original center Together, these visualizations indi- cate that smaller-radius balls dominate the union and are concentrated near the boundaries- hiighiies-hhihhighttig the natural shrinkage of verifiable regions in such areas.
6. Conclusion and Future Work
Identifying verifiable input regions free from adversarial ex- amples is crucial for model selection, robustness evaluation, and reliable control strategies. This work introduces two MIP-enabled search algorithms, LEVIS-C and LEVIS-8. to identify verifiable input spaces. We formulate two opti- mization problems: one for computing the maximum verifi- able ball and another for locating nearest adversarial points along specified directions. These guide the LEVIS algo- rithms in dynamically updating ball centers, enabling elfi- cient exploration of the verifiable input space. We improve MIP scalability by up to 6x via hybrid NLP-MIP solver, with a worst-case optimality gap below 0.004. Unlike lo- cal optimizers, our method ensures global optimality when neuron activation patterns match those from the NLP solu- tion. We visualize verifiable balls under various norms to inform search design and benchmark our method against tfte-oof-hheart techniques in terms of efficiency and radius accuracy. Finally, we analyze the distribution of verifiable balls collected by LEVIS-3 across scenarios. Future work will adapt LEVIS to neural network-basee control systems to certify safe input regions ensuring stability and reliability.
5.6. Distribution of Radii Discovered by LEVIS-3 in High-Dimensionn Space
We analyze the distribution of verifiable ball radii discovered by LEVIS-8 on the MNIST dataset. Compared to DC-OPF, the radii generally smaller, which attribute the higher input dimensionality and network complexity. We visualize the relationship between radii and distance to the initial center under varying search angles 0, initialization shifts A, and random seeds.
Figure shows that most verifiable balls have radii below 0.07. Varying 0, A, and random seeds leads diverse veri- fiable balls distributed across the input space. Randomness mainly affects the orthogonal vector q in (3d), thereby in- fluencing search directions. Each run is independent and can be parallelized over different and A values. Multi- directional searches can further boost coverage efficiency, which we leave for future work.
8

---

LEVIS: Verifiable NN Input Spaces
Acknowledgements
References
The work was funded by Los Alamos National Laboratory's Directed Research and Development project, "Artificial In- telligence for Mission (ArlMis)" under U.S. DOE Contract No. DE-AC52-06NA25535 and by NSF Grant 2130706 and ARO Grant W91 1911NF2310266.
Bell, B., Geyer, M., Glickenstein, D., Hamm, K., Scheideg- ger, C., Fernandez, A., and Moore, J. Persistent classi- fication: Understanding adversarial attacks by studying decision boundary dynamics. Statistical Analysis and Data Mining: The ASA Data Science Journal, 18(1): el 1716,, 2025.
Impact Statement
Ceccon, F., Jalving, Haddad, Thebelt, A., Tsay, C.,
Laird, C. D., and Misener, R. Omlt: Optimization & machine learning toolkit. Journal of Machine Learning Research, 23(349):1-8 2022.
This work introduces LEVIS, novel MIP-enabled search framework for identifying verifiable input spaces in neural networks, ensuring robustness against adversarial attacks. By formulating two complementary optimization problems, we efficiently compute the maximum verifiable region and locate directional adversarial points, enabling scalable and reliable model verification. Our approach significantly en- hances neural network safety and interpretability, with po- tential applications in autonomous systems, power grid sta- bility, and secure Al-driven decision-making.
Cui, W., Jiang. Y., and Zhang, B. Reinforcement learning for optimal primary frequency control: Iyapunov approach. IEEE Transactions on Power Systems, 1872),1676-1688 2022.
Duff, I. S. Ma57-a code for the solution of sparse symmet- ric definite and indefinite systems. ACM Transactions on Mathematical Software (TOMS), 30(2):1 (000))11881100 100::188-1440 144, 2004.
Fazlyab, M., Morari, M., and Pappas, G. J. An introduction to neural network analysis via semidefinite programming. 202/ 60th IEEE Conference on Decision and Control (CDC), pp. 6341-6350, IEEE, 2021.
Frank, S., Steponavice, I,, and Rehennack, S. Optimal power flow: A bibliographic survey i: Formulations and deterministic methods. Energy systems, 3:221-258, 2012.
Goodfellow, I. J., Shlens, J., and Szegedy, C. Explaining and harnessing adversarial examples. In International Conference on Learning Representations (ICLR), 2015.
Gowal, S., Dvijotham, K., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann, T. A., and Kohli, P. On the effectiveness of interval bound propagation for training verifiably robust models. CoRR, abs/1810.12715. 2018.
Grunbacher, S., Hasani, R., Lechner, M., Cyranka, J., Smolka, S. A., and Grosu, R. On the verification of neural odes with stochastic guarantees. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pp. 11525- 11535, 2021.
Hart, W. et al. Pyomo: Python optimization modeling ob- jects. Available at https: www. pyomo. org, 2024.
Kazi, S. R., Thombre, M., and Biegler, Globally con- vergent method for optimal control of hybrid dynamical systems. PAAC-PaperSOnLine, 58(14))868-873 2024.
Kilwein, Z., Jalving, J., Eydenberg, M., Blakely, L., Skolfield, K., Laird, C., and Boukouvala, F. Optimization with neural network feasibility surrogates: Formulations and application to constrained optimal power flow. Energies, 16(16):5913, 2023.

---

LEVIS: Verifiable NN Input Spaces
Kingma, D. P. and Ba, L.. Adam: Amethod for stochastic optimization. In Proc. 3rd Int. Conf. Learn. Representa- tions, pp. 1-15, 2014.
Scholtes, S. Convergence properties of regularization scheme for mathematical programs with complementarity constraints. SIAM Journal on Optimization, 11(4):918- 936, 2001.
Kleine Büinng, M., Kern, P., and Sinz, C. Verifying equiva- Ience properties of neural networks with relu activation functions. In International Conference on Principles and Practice of Constraint Programming, pp. 868-884. Springer, 2020.
Sundar, K., Nagarajan, H., Misra, S., Lu, M., Coffrin, C., and Bent, R. Optimization-basee bound tightening using strengthened qe qe-relaxation of the optimal power flow problem. In 2023 62nd IEEE conference on decision and control (CDC), pp. 4598-4603 IEEE, 2023.
Kotha, S., Brix, C., Kolter, J. Z., Dvijotham, K., and Zhang, H. Provably bounding neural network preimages. Ad- vances in Neural Information Processing Systems, 36, 2024.
Szegedy, C.,, Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., and Fergus, R. Intriguing proper- ties of neural networks. In 2nd International Confer- ence on Learning Representations (ICLR), 2014. URL https: /tcpss//arzee presentation.
Krizhevsky, A., Hinton, G., et al. Learning multiple layers of features from tiny images. 2009.
6199. Poster
Kuvshinov, A. and Günnemann, S. Robustness verification of relu networks via quadratic programming. Machine Learning, 11477)3407-2433, 2022.
Tjeng, V., Xiao, K. Y., and Tedrake, R. Evaluating robust- ness of neural networks with mixed integer programming, In International Conference on Learning Representations, 2019. URL https:/ btstts::/opeere////// http//ppwwweeeeeeee/ee/ee net forum? id=HyGIdiRqtm.
2022.
LeCun, Y., Cortes, C., and Burges, C. Mnist hand- written digit database. ATT Labs [Online]. Available: http://yann.lecum.. www.:aannneecc.ccooo www.c//w...m/xxx//mmsstttt 2, 2010.
Wächter, A. and Biegler, L. T. On the implementation of an interior-point filter line-search algorithm for large-scale nonlinear programming. Mathematical Programming, 106(1):25--))) 2006. doi: 10.1007/s10107-004 0559-y.
Leyffer, S. and Munson, S. A globally convergent filter method for mpecs. Preprint ANLMCC-PP4457-D Ar- gonne National Laboratory, Mathematics and Computer Science Division, 2007.
Wang, S. and et.al. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network ro- bustness verification. In Advances in Neural Information Processing Systems 34, 2021.
Li, W., Deka, D., Wang, R., and Paternina, M. R. A. Physics- constrained adversarial training for neural networks in stochastic power grids. IEEE Transactions on Artificial Intelligence, 2023.
Yang. D., Balaprakash, P., and Leyffer, S. Modeling design and control problems involving neural network surrogates. Computational Optimization and Applications, 83(3):759- 800, 2022.
Liu, Y., Yao. Y., Ton, J.FF, Zhang, X., Guo, R., Cheng, H., Klochkov, Y., Taufiq, M. F., and Li, H. Trustwor- thy LLMs: survey and guideline for evaluating large language models' alignment. In Socially Responsible Language Modelling Research, 2023. URL https: //openreview net / forum? d=oss SuaPFfB.
Zhang, H., Wang, S., Xu, Ki, Li, Li, B., Jana, S., Hsieh, C.-J., and Kolter, J. Z. General cutting planes for bound- propagation-based neural network verification. Advances in neural information processing systems, 15:1656-1670, 2022.
Marzari, L., Corsi, D., Marchesini, E., Farinelli, A., and Cicalese, F. Enumerating safe regions in deep neural net- works with provable prohabilistic guarantees. In Proceed- ings of the AAAI Conference on Artificial Intelligence, volume 38. pp. 21387 22192,1944444 2024.
Matoba, K. and Fleuret, F. Exact preimages of neural net- work aireraft collision avoidance systems. In Proceedings of the Machine Learning for Engineering Modeling, Sim- ulation, and Design Workshop at Neural Information Processing Systems, pp. 2020.
Peck, J., Roels, J., Goossens, B., and Sacys, Y. Lower bounds on the robustness to adversarial perturbations. Advances in Neural Information Processing Systems, 30, 2017.
10

---

LEVIS: Verifiable NN Input Spaces
A. Appendix: Theoretical Results
Theorem A.1. For any convex bounded verifiable region C , the sequence of balls {B(c,) generated by LEVIS-O s-a converges a ball B(c) that intersects the boundary of C least at two points. Specifically, for any > 0, there exists a number of algorithm iterations N such that for all n > N, B(e) encompasses two points almost symmetric about the center with less than mismatch, and these two points lie on the boundary ofC.
Proof. Consider the convex, bounded, and closed region C C Rd. At each step n of Algorithm ball B(G.) with the radius Tn is generated, where On is the center, with the property that B(c,) C. By convexity and boundedness, the boundary aC is non-empty, compact, and ensures that the sequence (B(r,) must converge to a configuration where the ball touches the boundary of C at multiple points.
Next, we introduce a constant A, which we define as the greatest rate of change in the width of the region along any line passing through its center. Specifically, characterizes the maximum rate at which the distance between two points on the boundary of C, opposite sides of line passing through the center, changes as we move the line across C. This constant À is finite due the convexity and boundedness of C.
Now, consider the rays emanating from the center cn in the directions aligned with the axes of the & norm. The algorithm iteratively adjusts the center to reduce the asymmetry of the distances from On to the boundary aC along these rays. Let A. denote the measure of asymmetry at the n-th step, defined as the maximum difference between the distances from on to aC along opposite rays.
By the convexity of C, moving the center en results in a decrease in An at rate proportional to the radius In from on the boundary aC. Specifically, due to the convexity and the definition of X, the reduction in A,, between steps and can be bounded below by À Tu. Hence, the sequence { ) converges zero as increases.
To formalize this, given any E > 0, choose N such that for all n > N, the asymmetry A, is less than The constant À ensures that for n > N, the ball (c,,) touches the boundary aC at least at two distinct points, as the rays from the center are symmetrized to within e/>. Thus, B(c,) intersects òC at two points, say In and yn. satisfying || - yn ynlll 2 fx. Moreover, since the asymmetry A,, is controlled by X, the point 6, within B(c,) can be chosen such that || bn ll z and min |lb,. r|| < 6.
Therefore, the sequence (B(c,)) converges to a ball that touches the boundary of C at at least two distinct points, which completes the proof.
In general, for non non-convex regions, this does not necessarily hold. In particular, separate convex sub-regions separated by bottleneck can form an oscillator in this algorithm without convergence. In practice, we conjecture that this is a rare scenario and that our algorithm seems to reliably get "caught" in small convex sub-regions.
Note:
B. Appendix: Details of Datasets and Extra Experimental Results
B.1. Optimal Power Flow Datasets
8
2
[30,100]
[60,200]
90
125
100
[30,100]
Figure 10. IEEE 9-Bus system topology. The system has demand nodes (5,7,9) with nominal values (125, 90, 100) in MW, and the 3 generator nodes with (1,2,3) with limits 1030, [60,200], 100)) in MW. Therefore, the neural network has 3 inputs and 3 outputs.

---

LEVIS: Verifiable NN Input Spaces
We generate direct-current (DC) power flow datasets using the IEEE 9-bus power grid benchmark, widely recognized model for simulating energy flow in power grids, depicted in Figure 10. Nodes 1, 2, and are equipped with generators, while nodes 5, 7, and serve as load points. Power operators can adjust the output generator nodes, allowing for variations within predefined ranges. The neural network. (ppr generator nodes based on the demand (Pp) from the load nodes and PD E TR The dataset is created by solving the DC Optimal Power Flow (DC-OPF) problem (Frank et al., 2012) using nominal inputs 2g = [125, 90, 100 from standard datasets, perturbed by 10% uniform noise to produce a diverse set of 1,000 data samples. The DC-OPF specification requires that outputs stay within the physical limits of the generators, specifically PG1 [30, 100], PG2 E [60, 200], and Pcs E [30, 100]. We trained a three-layer ReLU neural network using the Adam optimizer (Kingma & Ba, 2014) to compute DC-OPF solutions, selecting 80% of the data samples randomly for training and reserving the remaining for testing.
Pc. predicts the electricity generated (Pc) at these three
12

---

LEVIS: Verifiable NN Input Spaces
7
7
+
Output: 7
Perturbation 2 0.1
Output: 3
Figure The minimum perturbation needed to the clean image of "7" (on the left) has value of and is shown in the center image. This results in an image (on the right) that is visually very close, but the classifier mistakes it for the digit "3".
B.2. MNIST and CIFAR-10 Datasets
We utilize the MNIST digit dataset, which consists of 60,000 training and 10,000 testing samples, for an image recognition task (LeCun et al., 2010). MNIST is widely used benchmark in neural network verification problems (Gowal et al., 2018; 88; Wang & et.al., 2021: Kotha et al., 2024), comprising handwritten digits across ten classes (0 to 9). The neural network Simage (I) = 9 predicts class probabilities for each input z, and the goal is to ensure that the predicted probability for the true class exceeds that of any other class. This operationalized as mingyr(es: - = (image(2))
We implement two-layer ReLU neural network trained using cross-entropy loss and optimized with the Adam optimizer learning rate of 0.001. The network architecture for MNIST consists of three layers: input x 784 two hidden layers =²,²² E 1R50 and output layer 23 E 1R The network achieves test accuracy of 97%. For evaluation, we select the first image in the test dataset as the initial point x. for computing the maximum verifiable ball. Principal Component Analysis (PCA) is optionally used for MNIST to accelerate training, though it is not essential for the core results.
For the CIFAR-10 10 dataset (Krizhevsky et al., 2009), we use a subset of 10,000 test images. CIFAR-10 consists of 32x32 RGB images across ten object categories such as airplanes, cars, birds, and so on. Unlike MNIST, PCA not used for dimensionality reduction due to the higher complexity and diversity of the image content.
Code and experiments are being made available at: https: http//ggttttt Lww.o/LLEVS---E LANVIIS-LANLIVIEE
B.3. Visualization of the nearest adversarial point for image classification
For image recognition, we find the closest adversarial point the clean image of the digit "7", in Figure 11. The distance to the adversarial point 0.1. (in terms of pixel magnitude), and despite the image being visually the same, the classifier, even with its high accuracy of 93%, mistakes it for the digit "3".
B.4. Statistical Performance of LEVIS-3
Table 3. Statistical Summary of the Radii
Statistic
Value
Number of Radii
52
Minimum Radius
0.10
Maximum Radius
23.58
Median
0.42
Mean
3.75
Lower Quartile
0.16
Upper Quartile
2.46
Variance
45.25
Standard Deviation
6.73
We provide more statistics on LEVIS-3 for DC-OPE. The main results are found in Table 3.
13

---

LEVIS: Verifiable NN Input Spaces
B.5. CPU Resources
We used three machines for the computations. The specifications of the machines are shown in Table 4, Table 5, and Table
Table 4. CPU 1 Information Summary
Attribute
Details
Processor
Intel(R) Core(TM) 17-8550U
CPU @ 1.80GHz
Base Speed
1.99 GHz
Current Speed
1.57 GHz (can vary)
Cores
Logical Processors
8
L1 Cache
256 KB
L2 Cache
MB
L3 Cache
8.0 MB
Virtualization
Disabled
Hyper-V Support
Yes
Table 5. CPU 2 Information Summary
Attribute
Details
Processor
Intel(R) Xeon(R)
Gold
6258R CPU @ 2.70GHz
Base Speed
2.70 GHz
Cores
56
Logical Processors
112
LI Cache
100 MB
1,2 Cache
3136 MB
L3 Cache
154 MB
Table 6. CPU 3 Information Summary
Attribute
Details
Processor
Apple M3 Max CPU
64GHz
Cores
14


Reviews:
[{"review_id": "1zQcD66a01", "reviewer": "Reviewer_Hx3K", "summary": "This paper presents an algorithm for computing inner-approximations of neural network preimages as a union of balls. The method is split into two sub-methods, one for maximizing an inner-approximating ball, and another for generating new balls to append to the overall approximation. Experiments are conducted on optimal power flow and MNIST digit classification examples to illustrate the performance and algorithmic properties of the proposed approach.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your detailed and constructive review. Below, we address the key concerns and questions you raised.\n\n---\n\n### Major Weaknesses\n\n> **Weakness #1:** Theorem 4.1 critically assumes that the input space is convex...\n\n**Response:**  \nThank you for identifying this. Empirically, most problems converge. Failures typically occur when the verifiable region is open—some ray-restricted subproblems may have no solution. Since these directions correspond to model-insensitive inputs, they are excluded from new center computations.\n\nWe verified that convergence still holds for star-shaped regions and unions of convex sets, up to a measure-zero set of oscillations. Algorithm 1 could be extended to isolate oscillatory behavior via added constraints or by requiring the final ball to include the starting point. In such cases, Theorem 4.1 (or its generalization) ensures convergence. Since these cases did not arise in practice, we omitted this detail. We will clarify the convexity assumption in the paper.\n\n> **Weakness #2:** The experimental comparison is weak... [Zhang et al., 2024] is not cited.\n\n**Response:**  \nOur formulation differs from prior work, limiting directly comparable baselines. We compare with MIP-based methods in Section 5.2. Zhang et al. (2024) assumes axis-aligned input hyperrectangles and polyhedral output sets, which differ from our setting. We will cite the work and clarify the distinctions.\n\n> **Weakness #3:** Experiments are conducted on small datasets...\n\n**Response:**  \nIn addition to MNIST, we report results on CIFAR-10 using our NLP solver from (2a)–(2c), compared against MIP$_\\text{CROWN}$ on identical tasks:\n\n| Dataset   | Proposed (s) | MIP$_\\text{CROWN}$ (s) | Optimality Gap |\n|-----------|--------------|------------------------|----------------|\n| MNIST     | 1.34         | 10.48                  | 0.004          |\n| CIFAR-10  | 5.96         | 17.47                  | 0.0009         |\n\nDespite CIFAR-10’s added complexity, our solver is ~3× faster with a tighter gap. This confirms our method’s scalability to larger networks.\n\n---\n\n### Questions For Authors\n\n> **Q1:** Can your methods scale to CIFAR-10?\n\n**Response:**  \nYes — as shown above, our method scales well to CIFAR-10 and outperforms MIP$_\\text{CROWN}$ in  runtime.\n\n> **Q2:** Have you considered optimizing the search angle?\n\n**Response:**  \nYes, and we believe it could improve convergence by reducing overlap. We plan to explore this in future work.\n\n> **Q3:** Do adjacent balls intersect? Figure 4 suggests otherwise.\n\n**Response:**  \nThey can. Figure 4 shows a simplified case. We will revise it to depict overlapping balls explicitly.\n\n---\n\n### Minor Comments & Suggestions\n\n> “Discontinuous” → “disconnected”\n\n**Response:**  \nAgreed — will revise.\n\n> Clarify radius of ball\n\n**Response:**  \nDefined as $r = \\||x^* - c\\||_p$, where $x^*$ is the nearest adversarial point, using the $l_p$ norm (see Section 2).\n\n> Perturbed inputs phrasing is confusing\n\n**Response:**  \nWe will clarify: perturbed inputs are adversarial only if they lead to misclassification (Goodfellow et al., 2014).\n\n> Is output scalar?\n\n**Response:**  \nNo — “scales” refers to scalability. We will revise for clarity.\n\n> “Cover entire verifiable space” is misleading\n\n**Response:**  \nWe will change to “tightly underapproximate the verifiable input space.”\n\n> Layer vs. neuron index\n\n**Response:**  \nIndex $i$ refers to the layer. We will clarify this.\n\n> Constraint classification\n\n**Response:**  \nOnly (2b) is nonlinear — we will clarify.\n\n> Redundant “then”\n\n**Response:**  \nWe will revise to remove “then.”\n\n> Notation reuse (e.g., $j$)\n\n**Response:**  \nWe will rename $j$ in Section 4.2 to $s$ for clarity.\n\n> Notation consistency\n\n**Response:**  \nWe will standardize all notation (e.g., $\\mathbb{R}^n$).\n\n> Algorithm 1 indexing style\n\n**Response:**  \nWe will fix inconsistencies.\n\n> “Almost symmetric” / “$\\varepsilon$-mismatch”\n\n**Response:**  \nWe will define “almost symmetric” precisely — angle > $\\pi/2$ between $x_1 - c$ and $x_2 - c$.\n\n> “Disconnectedness” vs. “discontinuity”\n\n**Response:**  \nWe agree — will revise to “disconnectedness.”\n\n> Source of $\\sqrt{2}$ term\n\n**Response:**  \nIt is from the $l_2$ norm difference between one-hot vectors, as in Fazlyab et al. (2021), Section II.D.\n\n> Section 4.3.2 formatting\n\n**Response:**  \nWe will revise the nested numbering.\n\n> Missing citation: Zhang et al., TACAS 2024\n\n**Response:**  \nWe will include this citation and clarify how their assumptions differ from ours.\n\n---\n\n### References\n\n- Fazlyab, M., Morari, M., & Pappas, G. J. (2021). *An introduction to neural network analysis via semidefinite programming.* IEEE CDC.\n- Goodfellow, I. J., Shlens, J., & Szegedy, C. (2014). *Explaining and harnessing adversarial examples.* arXiv:1412.6572.\n- Zhang, X., Wang, B., & Kwiatkowska, M. (2024). *Provable preimage under-approximation for neural networks.* TACAS.", "claims_and_evidence": "For the most part, the claims are adequately supported. My two primary concerns which lack clarity and/or convincing evidence are:\n\n1. Theorem 4.1 relies on the very strong (and impractical) assumption that the input set is convex, but this assumption is hidden away in the appendix and not mentioned at all in the main paper.\n\n2. The experiments attempt to show that the preimage inner-approximations generated by the proposed method are larger (stronger) than prior baselines. However, the chosen baseline based on Lipschitz bounds is quite weak, which degrades the experimental support.\n\nSee additional discussion in Other Comments Or Suggestions below.", "methods_and_evaluation_criteria": "Proposed methods and evaluation criteria make sense, but could be made stronger by using more realistically-sized datasets like CIFAR-10 or ImageNet.", "theoretical_claims": "The proof in the appendix seems to be rigorous, albeit missing the technical assumption that $\\mathcal{C}$ is full-dimensional (in the sense that it contains an open ball). Otherwise, the inner-approximation generated by the proposed method would be trivially empty.", "experimental_designs_or_analyses": "The experiments appear to be sound.", "relation_to_broader_scientific_literature": "This paper proposes a new method for neural network preimage approximation, which can be used for verifying the safety and reliability of neural networks employed in a variety of different scientific domains, e.g., control systems, power systems, medical diagnosis systems, etc., all of which require rigorous robustness guarantees. The proposed method is intimately related to prior works that focus on verifying the safety of fixed input regions.", "essential_references_not_discussed": "The paper focuses on preimage approximation, which is a relatively new area. The only highly related reference that I noticed was missing was [1]:\n\n[1] Zhang, Xiyue, Benjie Wang, and Marta Kwiatkowska. \"Provable preimage under-approximation for neural networks.\" International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer Nature Switzerland, 2024.", "other_strengths_and_weaknesses": "In general, I have a handful of questions, suggestions, and concerns regarding formatting and presentation, mathematical clarity and validity, and lack of convincing experimental baselines. Please see my specific comments in Other Comments Or Suggestions below.", "other_comments_or_suggestions": "1. Lines 55, 78, and 240 (Column 2): Do you mean \"disconnected\" instead of \"discontinuous\"?\n2. Line 75, Column 2: \"$\\mathcal{B}(c)$ represents a ball centered at $c$.\" Of what radius?\n3. Line 110: \"Inputs that, when perturbed,  result in erroneous neural network outputs...\" I think this needs rephrasing: the perturbed input is the adversarial example, not the (nominal) input that gets perturbed.\n4. It seems like from Line 86, Column 2, onwards, you are assuming that the output $f(x)$ is a scalar (so that, for instance, $\\min_{x\\in\\mathcal{S}} f(x)$ is well-defined). This is a common assumption in the verification literature, since the scalar-valued specification being verified can often be absorbed into the final linear transformation. If this is what you are assuming, then please explicitly mention this to the reader.\n5. Based on your optimization problem (1), it looks like you are computing a ball that inner-approximates the true verifiable input set. In the third listed contribution on Line 64, Column 2, you mention that your method \"cover the entire verifiable space,\" which would imply that you are generating an over-approximation. I suggest that you change the \"cover\" wording in this listed contribution to more accurately reflect your inner-approximation approach.\n6. Line 154, Column 2: \"...complementary variables for the ith neuron.\" Previously, you used $i$ to index the layer number, not the neuron, and it still looks like you are doing so in problem (2), since you are still using the preactivation and activation vectors $z^i$ and $\\hat{z}^i$. Therefore, do you mean to say \"layer\" instead of \"neuron\" here?\n7. Line 162, Column 2: \"...are the nonlinear equivalence of the ReLU function.\" The constraint (2a) is linear. It looks like the only nonlinear constraint is the bilinear inequality $p^i q^i \\le 0$. You may want to reword your sentence here to more accurately reflect this fact.\n8. It looks like you may want to remove the first \"then\" on Line 175.\n9. If I understand your directional adversarial point optimization approach, you are first fixing a direction to find an adversary along, and then running your optimization (3) in order to find the closest adversarial example to the previous one ($b$), along the given direction. If this is the case, aren't (3d) and (3e) already imposed before the optimization takes place? In other words, it seems like (3d) and (3e) are not optimization constraints.\n10. Section numbering: 4.3.2. (1) and 4.3.2. (2) look quite odd. I'd suggest formatting these sections differently to avoid the four-fold section numbering with parentheses.\n11. Line 209, Column 2: There is some clash in your notation. Previously, you used $d$ to denote a point in $\\mathbb{R}^n$ to set up your directional adversary optimization, but now you are using it to denote the number of pairs of boundary adversarial points. I'd suggest changing some of the notation to avoid this clash.\n12. On a related note (notation), you previously used $R^n$ to denote $n$-dimensional Euclidean space, but then later you used $\\mathbb{R}^n$. It is best to remain consistent throughout the paper.\n13. In Section 4.3.2. (1) and Algorithm 1, you are using both subscripts and superscripts on the iteratively computed $b$ vectors. It seems like you should stick to one or the other and make all of your indexing notation consistent for these vectors.\n14. Theorem 1: \"...almost symmetric about the center $c$ with less than $\\epsilon$ mismatch\" These terms \"almost symmetric\" and \"$\\epsilon$ mismatch\" really should be made mathematically precise.\n15. Line 267, Column 2: Again, I think that it is more common to use \"disconnectedness\" here rather than \"discontinuity.\"\n16. Clarifying question: For the LEVIS-$\\beta$ algorithm, it seems to me like you are creating your \"new ball\" by first determining a new center $m$, which is very close to the boundary of the previous ball, and then solving the directional adversary optimization (3) to find an adversarial example closest to $m$, which gives you a new ball centered at $m$. This would mean that two adjacent balls actually intersect. However, your Figure 4 suggests that the balls might not intersect. Am I missing something?\n17. Experiments: Can your methods scale up to something more reasonably sized, even as large as CIFAR-10?\n18. Have you thought of any methods for optimizing the search angle $\\theta$? Choosing $\\theta=0$ and $\\theta=90$ degrees seems like it could be extremely limited in high-dimensional space. Even a comparison of these angles to randomly chosen angles would be an interesting ablation study.\n19. Section 5.3 (comparison to baseline): It is well-known that network bounds based on the global Lipschitz constant are very overconservative. I would expect to see a comparison of your method versus a stronger method, one that is likely also a MIP-based or branch-and-bound-based technique. For example, [1] appears to be one of the current state-of-the-art methods for computing inner-approximations of neural network pre-images.\n20. Where is the $\\sqrt{2}$ coming from in line 378? I would expect to see a $\\sqrt{n}$ if it were based on equivalence of norm inequalities.\n21. The main theoretical result, Theorem 4.1, does not state any restriction about the convexity of the input space $\\mathcal{C}$ in the main body of the paper. But then, in the appendix, the theorem statement is changed to be restricted to convex input spaces $\\mathcal{C}$. This is a \\emph{major} restriction both theoretically and practically; it is not just a minor ``condition.'' As you mention multiple times in the paper, the input spaces $\\mathcal{C}$ are typically nonconvex for neural networks. This poses a significant limitation for your theoretical result, and, in my opinion, it is simply unacceptable (and seemingly dishonest) to hide this condition until the appendix.\n\n[1] Zhang, Xiyue, Benjie Wang, and Marta Kwiatkowska. \"Provable preimage under-approximation for neural networks.\" International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer Nature Switzerland, 2024.", "questions_for_authors": "See above Other Comments Or Suggestions.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "qeCBhSTCb5", "reviewer": "Reviewer_h45y", "summary": "The paper aims to find verifiable input space for a NN, i.e., input region where no adversarial example exists.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your thoughtful and encouraging review. We are glad to hear that you found our contributions clear and innovative. Below, we respond to your comments and suggestions.\n\n---\n\n### Comments on Claims and Evidence\n\n> **Comment C2 / Evidence E2:** The conversion of the ReLU function into an alternative MIP-friendly formulation was unclear. A small example may help.\n\n**Response:**  \nReLU is a piecewise linear function: for $\\hat{z} = \\text{ReLU}(Wz + b)$, we have $\\hat{z} = Wz + b$ if  $Wz + b \\geq 0$, and $\\hat{z} = 0$ otherwise. To encode this in a MIP, we introduce a binary variable $a$, where $a = 1$ if $Wz + b \\geq 0$, and $a = 0$ otherwise. Using the Big-M method, this conditional behavior can be captured with linear constraints, making the ReLU compatible with MILP solvers.\n\n---\n\n### Weaknesses\n\n> **Weakness #1:** Section 4.2 (after Equation 2c) could be written more clearly for non-experts.\n\n**Response to Weakness #1:**  \nSure, here is a revised version to be easier to comprehend for non-experts:\n\nWe introduce a small regularization parameter $\\varepsilon > 0$ (recommended to be $10^{-5}$) to handle the nonlinear inequality $p^i q^i \\leq \\varepsilon$ for better convergence [Scholtes, 2001]. This simplifies the problem, allowing it to scale polynomially with the number of neurons $N$ instead of being NP-hard.\n\nHowever, solvers for nonlinear programming (NLP) may still find only locally optimal solutions, particularly when both $p^i_j$ and $q^i_j$ are zero for some neuron $j$ (called the **bi-active set**). This set is defined as: $I_0 \\equiv \\{ j \\mid p^i_j = q^i_j = 0 \\}.$ To manage this, we categorize neurons into three groups: If $p^i_j > 0$, then $q^i_j = 0$ and $j \\in I_+^i$. If $p^i_j = 0$ and $q^i_j > 0$, then $j \\in I_-^i$. If $p^i_j = 0$ and $q^i_j = 0$, then $j \\in I_0^i$.\n\nWe then construct a simplified MIP that includes integer variables only for neurons in $I_0^i$. This significantly reduces the number of binary variables—often to a small subset of neurons—making the optimization more tractable, as shown in Section 5.2. When the activation states are consistent with $I_+^i$ and $I_-^i$, the resulting solution is globally optimal.\n\n---\n\n### Question For Authors\n\n> **Question #1:** Is there a way to exactly compute the total volumes of the verified regions provided by LEVIS-beta?\n\n**Response to Question #1:**  \nThis is a very good question. Computing the volume of the union of balls may be difficult as the balls overlap, and consequently, the total volume is not the sum of individual volumes, but it is definitely a good suggestion to be considered in future work.", "claims_and_evidence": "C1.  A MIP based verification framework that provides maximum verifiable input ball around a center c. \n\nE1. The paper provides a clear formalization of this claim in eq. 1a-1f.\n\nC2. Faster solver for the MIP based verification framework.\n\nE2. They convert the ReLU function, into an alternative formalization ---  however, the details of how this is obtained is not clear to me. A small example regarding this may help.\n\nC3. The authors provide a novel search strategy based on dynamically updating the centers based on adversarial points along different directions.\n\nE3. This strategy is quite clearly explained in section 4.3.1 and 4.3.2\n\nC4. The paper provides another search strategy that provides a union of verified balls. \n\nE4. The strategy is quite clearly explained in section 4.3.3 and Algorithm 2.", "methods_and_evaluation_criteria": "The paper builds a MIP based verification framework for getting certified input spaces.\nAnd they also empirically verify the computational superiority of their method both in terms of time complexity and radii of the verified input region. The experimental setting is quite simple.", "theoretical_claims": "The main theoretical claims (informally) states that the verified balls provided by their methodology intersects the boundary of the true (verified) region atleast on two points.\n\nI did not check the proof. But the claim seems quite reasonable given the paper's methodology.", "experimental_designs_or_analyses": "The authors provide a rigorous set of experiments, analyzing computational time, and verified radii.", "relation_to_broader_scientific_literature": "The paper is quite relevant to the general research in verifying NNs.", "essential_references_not_discussed": "None, to the best of my knowledge", "other_strengths_and_weaknesses": "Strength: \n- Clarity: Although, I am not an expert in the field, I found most aspects of the paper to be quite clearly written. Except, the evidence for C2 (see above in claims and evidence).\n\n- Novelty: The proposed MIP based search strategies are quite innovative.\n\nWeaknesses: \n\n- None, in my understanding. However, I could have missed some details. And I am not well-versed with the larger literature.", "other_comments_or_suggestions": "I think section 4.2 after equation 2c, can be written more clearly for non-experts.", "questions_for_authors": "Is there a way to exactly compute the total volumes of the verified regions provided by LEVIS-beta?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "usniN9x9xt", "reviewer": "Reviewer_JdfX", "summary": "In Neural Network Verification, the goal is to verify that a certain input-output relation holds. E.g. all inputs in some local neighborhood should have the same classification. This is a challenging (NP-hard) task. The authors propose a new technique that can be used to compute a *underapproximation* of the preimage of an output set that satisfies some linear constraint. All inputs in this preimage are guaranteed to satisfy the constraint. To this end, they also propose to use complementary constrained optimization to speed up MIP problems. The authors evaluate their new technique on a variety of applications.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your thoughtful and encouraging review. We address your comments and suggestions below.\n\n---\n\n### Clarifications on Claims\n\n> **Claim Concern:** The statement that \"LEVIS-beta captures the entirety of the verifiable space\" is too strong, especially since the method depends on random initialization.\n\n**Response:**  \nWe agree and will revise the wording to more accurately reflect that LEVIS-beta computes increasingly larger lower bounds on the verifiable space. While LEVIS-beta often achieves broad coverage, we do not claim it captures the entire space. It provides a growing conservative approximation under limited compute.\n\n---\n\n### Questions\n\n> **Q1:** In Section 4.2, how are the complementary variables $z_i, w_i$ computed? Do you first run an NLP to extract them, then create the MIP? Could this be improved with IBP?\n\n**Response:**  \nWe compute the complementary variables by solving the NLP in (2a)–(2c), where $p_i, q_i$ are decision variables jointly optimized. IBP is not used here directly, but can help in MIP formulations by tightening bounds on ReLU outputs and reducing integer variables.  \n\n> **Q2:** If sampling verification queries (e.g., from VNN-COMP), how many can your technique verify immediately? What is the runtime comparison between verification and preimage computation?\n\n**Response:**  \nOur solver is applicable to general ReLU-based networks but we have not yet evaluated on VNN-COMP queries due to time constraints. Since the problem formulations differ, direct runtime comparison between verification and preimage computation is nontrivial. Instead, we compare against a standard MIP baseline under similar conditions (Section 5.2).\n\n---\n\n### Minor Comments & Suggestions\n\n> **S1:** Could MIP constraints 1a–1f be replaced by adversarial search? It would not guarantee completeness but may be faster.\n\n**Response:**  \nAdversarial search is appealing but lacks full coverage of the adversarial space. Techniques based on gradients can be misleading due to local sensitivity. MIP (or its relaxations) is needed to map **global** bounds. Still, adversarial search could assist with initialization or guidance—this is a promising direction for future work.\n\n> **S2:** $z_i$ and $w_i$ appear in Section 4.2 but are not clearly introduced.\n\n**Response:**  \nAgreed—we will clarify that $z_i$ and $w_i$ are **complementary slack variables** enforcing the relaxed constraint $z_i w_i \\leq \\varepsilon$ in the NLP formulation.\n\n> **S3:** Please discuss whether larger networks can be processed.\n\n**Response:**  \nYes, our method scales well. As shown below, it runs faster than MIP$_\\text{CROWN}$ on CIFAR-10 while maintaining tight optimality gaps:\n\n| Dataset   | Proposed (s) | MIP$_\\text{CROWN}$ (s) | Opt. Gap |\n|-----------|--------------|------------------------|----------|\n| MNIST     | 1.34         | 10.48                  | 0.004    |\n| CIFAR-10  | 5.96         | 17.47                  | 0.0009   |\n\nCIFAR-10 has ~12.4K more neurons than MNIST and 4× the input size. Our solver remains efficient and scalable. For large networks, we first compute an approximate solution with a small optimality gap, then refine it using a reduced MIP (Section 4.2). Lowering $\\varepsilon$ (e.g., suggest to be $10^{-5}$) tightens the gap while preserving tractability.", "claims_and_evidence": "*LEVIS-alpha can find \"a single, large verifiable ball that intersects at least two boundaries of a bounded [output] region\"*\nThe argument is sound and convincing: 1a-1f find the closest adv. ex, so every point closer to the center must not be an adv. ex.\n\n*LEVIS-beta \"captures the entirety of the verifiable space\"* I find this claim to be too strong - according to the last sentence in 4.3.3, LEVIS-beta depends on the random initialization. So I fear there's a risk of not finding the \"right\" random seeds and therefore not identifying the entire verifiable space. Even in the best case, it would only approximate it up to $\\epsilon$. \"LEVIS-beta is an any-time algorithm that computes increasingly larger lower bounds to the verifiable space\" may be a more appropriate claim.\n\n*Complementary constrained optimization speeds up the MIP verification*\nThis seems to be confirmed by the experiments.", "methods_and_evaluation_criteria": "The benchmarks are appropriate in the sense that other preimage papers use similarly small network architectures (e.g. Katha et al.). But the paper would benefit from a discussion why larger networks cannot be processed this way - or if they can, the respective experiments.", "theoretical_claims": "I checked Theorem 4.1 and did not find any issues", "experimental_designs_or_analyses": "The experimental design seemed to be correct, but I did not check them in depth.", "relation_to_broader_scientific_literature": "The key contribution is LEVIS-alpha/beta, which is a novel idea.", "essential_references_not_discussed": "I'm not aware of uncited essential references.", "other_strengths_and_weaknesses": "The paper proposes two interesting algorithms (LEVIS-alpha/beta) that are novel in the literature. It's a promising approach to compute an *underapproximation* of the preimage of an output set, which has significant applications e.g. for safe controllers.", "other_comments_or_suggestions": "1) Could the MIP using 1a-1f be replaced by an adversarial search? This would not guarantee that there are no closer adversarial examples, but could be much faster. As long as the original MIP is solved *eventually* (as LEVIS converges to a center), this should be sufficient, right?\n\n2) $p^i$ and $q^i$ are used in Section 4.2 but not properly introduced. Their meaning can be inferred, but a short description would be helpful. In what cases do they take which values? Currently, they are called the \"complementary variables\", but that term is not defined.", "questions_for_authors": "1) In Section 4.2, you state that you use $p^i$ and $q^i$ to decide for which neurons to include integer variables. How do you first compute these values? Do you run NLP once, then extract them, and then create the MIP? Could this be replaced/improved by e.g. using IBP (integer bound propagation) instead?\n\n2) If you sample verification queries (or use a benchmark from VNN-COMP, if there is one with a network small enough to support your procedure), how many of them could you immediately verify using your technique? If the query is about an input region that's covered by your preimage, it's known to be safe. How does this runtime compare to the time you need to compute the preimage?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "uzwHsnoLmf", "reviewer": "Reviewer_wzBC", "summary": "The paper proposes an approach for the generation of verifiable input spaces for a neural network:\nInstead of providing an answer on whether a given input space region is safe, the paper instead proposes to generate an input region for which the NN is verified. The paper claims that this technique can be used for model selection. The approach is evaluated on a set of benchmarks.\n\n## update after rebuttal\nI appreciate the authors' response which lifted all open questions and concerns I had.  \nI trust that the authors will update their paper as promised in the rebuttal.  \nIn particular, regarding the approximative nature of the solution in Section 4.2 and regarding the convexity assumption.  \nFollowing the rebuttal, I have raised my score to \"Accept\" and stand with this score -- I am in favour of accepting the paper.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your detailed review and thoughtful feedback. We address your concerns below.\n\n---\n\n### Theoretical Claims\n\n**#1:** The paper inconsistently uses $f^* > 0$ for satisfaction and $f < 0$ for violation.\n\nWe leverage $f > 0$ to ensure satisfaction and $f < 0$ to ensure violation—these are distinct objectives. In Problem (1a)-(1f), we seek a verifiable ball by finding the nearest violating point $x^*$, which defines the ball’s radius $r = \\|| x^* - c \\||_p$. This formulation guarantees a minimum is sought.\n\n**#2:** Claim of $\\mathcal{O}(N \\log N)$ NLP runtime lacks justification.\n\nOur solver guarantees global optimality when ReLU activation states (active/inactive) remain consistent with the given index sets $I_+$ and $I_-$. This introduces a constrained space where the optimization is exact. The empirical optimality gap is zero for DC-OPF and only 0.004 for MNIST, indicating high fidelity in practice.\n\n**#3:** Theorem 4.1 omits convexity/closedness assumptions in main text.\n\nWe appreciate you catching this—our empirical results indicate most problems converge. A common failure mode occurs when the verifiable region is open and ray-restricted subproblems lack solutions. These unbounded directions correspond to insensitive model dimensions and are excluded when computing new centers. The result also holds for star-shaped regions and finite-unions of convex sets (up to a measure-zero set of oscillators). While Algorithm 1 could be modified to detect oscillations or constrain to regions around the origin to force convexity, in both cases, convergence follows from Theorem 4.1 or its generalization. Since these issues didn’t arise in practice, we omitted them. The empirical performance mirrors the convexity-based guarantee, which we should have included explicitly.\n\n**#4:** $p^i_j = q^i_j = 0$ seems to imply $z^i = \\hat{z}^i = 0$ for ReLU.\n\nSetting $p^i_j = q^i_j = 0$ does not imply $z^i = \\hat{z}^i = 0$. These values result from solving the nonlinear program in Equations (2a)–(2c), not from direct assignment. The solution reflects ReLU behavior.\n\n---\n\n### Experimental Evaluation\n\n**#5:** Section 5.2 only evaluates MNIST's first image. How robust is performance?\n\nWe evaluated multiple initial points and classes. As long as the input is correctly classified, performance is consistent. Poor initial points (e.g., radius = 0) lead all solvers to converge quickly. Runtime scales with neuron count, not class count. With more neurons, our method outpaces MIP-based baselines.\n\nBelow, we show more experiments on MNIST and CIFAR-10:\n| Dataset   | Proposed (s) | MIP$_\\text{CROWN}$ (s) | Opt. Gap |\n|-----------|--------------|------------------------|----------|\n| MNIST     | 1.34         | 10.48                  | 0.004    |\n| CIFAR-10  | 5.96         | 17.47                  | 0.0009   |\n\n**Takeaway:** The approach scales to larger networks, and compute time is independent of the initial point.\n\n**#6:** Clarify benchmark and setup in Table 2; the phrase “five random implementations” is unclear.\n\n- **Benchmark:** NN regression for OPF, as in [Brix et al., 2023].\n- **Baseline:** Lipschitz-based bound from [Fazlyab et al., 2021].\n- **Setup:** We solve (1)-(2) for the NLP variant and compare radius to the baseline.\n- **“Five random implementations”:** Due to training randomness, we repeat 5× and report intervals.\n\n---\n\n### Related Work\n\n**AAAI24 Comparison:** AAAI24 proposes sampling-based guarantees; we focus on deterministic ones via LEVIS. Our regions give 100% coverage under fixed activations and stronger guarantees at lower cost. This is useful under adversarial risks [Goldwasser et al., 2022].\n\n**Radius Works [CP20], [arxiv13]:** [CP20] finds nearest disagreements, [arxiv13] the closest confirmation point. We find the nearest *misclassified* point. These are complementary and will be cited.\n\n**NP-Completeness [CAV17], [RP21]:** We acknowledge verification and reachability are NP-complete. Our solver yields exact results when ReLU states—active ($I_+$) or inactive ($I_-$)—are fixed. Though this may introduce an optimality gap, empirical results show it’s negligible (e.g., 0 for DC-OPF, 0.004 for MNIST).\n\n---\n\n### Other Clarifications\n\n**Variables & Notation:** We used $\\mathcal{P}$ (not $\\mathcal{F}$) for the verification condition. Fixed citation spacing, 90° notation, and unified $b_i$ vs $b^i$.\n\n**Algorithm 2 Logic:** Early termination ensures efficiency; the order is correct.\n\n**Model Selection:** We estimate verifiable input space to assess robustness. In safety-critical settings (e.g., power grids), this supports model selection based on stability guarantees (Cui et al., 2023).\n\n---\n\n### References\n\n- Brix et al. (2023), *arXiv*  \n- Cui et al. (2023), *NeurIPS*  \n- Fazlyab et al. (2021), *CDC*  \n- Goldwasser et al. (2022), *arXiv*", "claims_and_evidence": "See issues discussed below.", "methods_and_evaluation_criteria": "The proposed methodology seems to fit the problem well even though I have numerous concerns with the theory as currently presented (see \"Theoretical Claims\").\nIssues with the evaluation are discussed in \"Experimental Design Or Analyses\".", "theoretical_claims": "The paper seems to switch between notation where the property is satisfied if f*>0 and notation where the property is violated when f < 0 (only one of the two can be correct as 0 must be either safe or unsafe).\nImportantly, this issue also shows up in the optimization problem formulated in (1a)-(1f):\nIn my understanding, since (1) is a strict inequality, this optimization problem might not have a minimum, but only a supremum.\nConsequently, it might be advisable to go for the formulation where f(x)=0 is already unsafe? However, in that case the mathematics of the paper should be uniformly phrased in this manner.\n\nConcerning the time complexity analysis on page 4:\nWhile there may be empirical advantages to the chosen polynomial NN encoding, it is not clear to me why the NLP solver would only have a runtime of O(N log N). The paper does not provide any detailed analysis on why the worst-case computational complexity of this optimization problem would be so low. In particular, it seems to me that the bi-active neurons, while apparently a problem for optimization, do not lead to spurious counterexamples as for $p_j^i=q_j^i=0$ we have a consistent assignment of a ReLU's input and output variables (namely $z^i=\\hat{z}^i=0$). Consequently, since NN verification alone does not require any optimization, a low complexity would break the NP-completeness which I find implausible.\nI hope we can resolve this misunderstanding through the rebuttal.\n\nConcerning Theorem 4.1:\nThe guarantees on LEVIS-$\\alpha$ also require that $\\mathcal{C}$ is convex and closed, which is dropped in the paper version of Theorem 4.1 and only appears in the appendix version.\nNotably, this is quite a strong assumption: Note that even the visualization in Figure 2 does not satisfy this assumption as the red shaded area is *not* a convex set. If this assumption is indeed necessary (which seems to be the case judging from the proof), this warrants further discussion.", "experimental_designs_or_analyses": "In Section 5.2 the paper compares the efficiency of their new relaxation with existing approaches on one input region for MNIST. In B.2 you mention that for your evaluation you use as the initial point the first image in the dataset. How does the performance of your approach (in 5.1 but also more generally) change for other initial points? Do you observe similar speedups? Is there a difference in behaviour across MNIST classes? I realize that it might be too late now to run these experiments, but this information would be essential to get a better understanding of the approach. As NN verification performance tends to have drastic variation across benchmarks and inputs, it is not clear whether the observed speedups hold in general or are specific to this particular NN and input region.\n\nAdditionally, a comparison to the techniques from [AAAI24] would be interesting (see \"Relation to Broader Scientific Literature\").\nIn case their technique is not directly comparable, the approach should be at least discussed as related work, as it seems strongly related.", "relation_to_broader_scientific_literature": "[AAAI24] proposed an approach for the enumeration of safe regions for a given NN specification. Even though the paper's main contribution is a probabilistic approach, the work seems strongly related to the paper at hand and should be discussed.\n\n[AAAI24] https://ojs.aaai.org/index.php/AAAI/article/view/30134", "essential_references_not_discussed": "Minimization of radii where specifications are verified has previously been explored [CP20] (see Section 4.3) which in turn cites another well-known work that minimizes adversarial radii outside the verification context [arxiv13] (see 4.1).\n\n[CP20] https://link.springer.com/chapter/10.1007/978-3-030-58475-7_50\n[arxiv13] https://arxiv.org/abs/1312.6199", "other_strengths_and_weaknesses": "I like the idea of turning the problem of NN verification on its head and instead search for the regions where robustness is verifiable.\nI also like the proposed approaches to search for large epsilon balls to this end.", "other_comments_or_suggestions": "Page 2:\n- $f^*$ is not explicitly defined in the background section.\n- It might be sensible to cite relevant literature on the NP-completeness of NN verification ([CAV17] or [RP21])\n\nPage 4:\n- missing space before (Scholtes, 2001)\n- As mentioned before $p_j^i=q_j^i=0$ seems to have a consistent assignment for the ReLU inputs and outputs via $z^i=\\hat{z}^i=0$\n  Consequently, this seems to be an issue specific to the performed optimization. It would be good to emphasize this more.\n\nPage 5:\n- There is a recurring inconsistency between the usage of $b_i$ and the usage of $b^i$ in places that seem to mean the same variable (e.g. line 3 vs line 6 of Algorithm 1)\n- Degree sign of 90° misses ^\n\nPage 6:\n- If my understanding is correct Line 12 and line 13-15 in Algorithm 2 should be the other way around?\n\nPage 7:\n- It is not clear what benchmark is used for Table 2 and the experiments described in Section 5.3\n- \"of five random implementations\": I think this is supposed to read executions/runs?\n\nGeneral:\n- Your paper does not explain on how your proposed approach could aid model selection, even though the paper starts and ends with this suggestion. Can you provide more concrete details on how your approach could be helpful here?\n\n[CAV17] https://link.springer.com/chapter/10.1007/978-3-319-63387-9_5\n[RP21] https://link.springer.com/chapter/10.1007/978-3-030-89716-1_10", "questions_for_authors": "**(Q1)** Please respond to my concerns outlined in \"Theoretical Claims\".\nIf I am mistaken about them or you have answers on how to fix these issues, I would be willing to increase my score.  \n**(Q2)** How does your approach compare (empirically or conceptually) to the work in [AAAI24]?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: this is a paper that proposes a method for computing verifiable input spaces of a given neural network. The reviewers' liked the theory and the method suggested. Several questions were clarified during the discussion phase. Overall this paper is recommended for acceptance and the authors are encouraged to prepare the final version in accordance with the promised clarifications and changes as suggested by the reviewers.
Decision: Accept (poster)