Thank you for your thoughtful and encouraging review. We address your comments and suggestions below.

Clarifications on Claims

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.

Response:
We 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.

Questions

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?

Response:
We 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.

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?

Response:
Our 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).

Minor Comments & Suggestions

S1: Could MIP constraints 1a–1f be replaced by adversarial search? It would not guarantee completeness but may be faster.

Response:
Adversarial 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.

S2: $z_i$ and $w_i$ appear in Section 4.2 but are not clearly introduced.

Response:
Agreed—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.

S3: Please discuss whether larger networks can be processed.

Response:
Yes, our method scales well. As shown below, it runs faster than MIP$_\text{CROWN}$ on CIFAR-10 while maintaining tight optimality gaps:

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

Thank you for your detailed review and thoughtful feedback. We address your concerns below.

Theoretical Claims

#1: The paper inconsistently uses $f^* > 0$ for satisfaction and $f < 0$ for violation.

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

#2: Claim of $\mathcal{O}(N \log N)$ NLP runtime lacks justification.

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

#3: Theorem 4.1 omits convexity/closedness assumptions in main text.

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

#4: $p^i_j = q^i_j = 0$ seems to imply $z^i = \hat{z}^i = 0$ for ReLU.

Setting $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.

Experimental Evaluation

#5: Section 5.2 only evaluates MNIST's first image. How robust is performance?

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

Below, we show more experiments on MNIST and CIFAR-10:

Takeaway: The approach scales to larger networks, and compute time is independent of the initial point.

#6: Clarify benchmark and setup in Table 2; the phrase “five random implementations” is unclear.

• Benchmark: NN regression for OPF, as in [Brix et al., 2023].
• Baseline: Lipschitz-based bound from [Fazlyab et al., 2021].
• Setup: We solve (1)-(2) for the NLP variant and compare radius to the baseline.
• “Five random implementations”: Due to training randomness, we repeat 5× and report intervals.

Related Work

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

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.

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

Other Clarifications

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

Algorithm 2 Logic: Early termination ensures efficiency; the order is correct.

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

References

• Brix et al. (2023), arXiv
• Cui et al. (2023), NeurIPS
• Fazlyab et al. (2021), CDC
• Goldwasser et al. (2022), arXiv

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.

Comments on Claims and Evidence

Comment C2 / Evidence E2: The conversion of the ReLU function into an alternative MIP-friendly formulation was unclear. A small example may help.

Response:
ReLU 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.

Weaknesses

Weakness #1: Section 4.2 (after Equation 2c) could be written more clearly for non-experts.

Response to Weakness #1:
Sure, here is a revised version to be easier to comprehend for non-experts:

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

However, 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$.

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

Question For Authors

Question #1: Is there a way to exactly compute the total volumes of the verified regions provided by LEVIS-beta?

Response to Question #1:
This 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.

Thank you for your detailed and constructive review. Below, we address the key concerns and questions you raised.

Major Weaknesses

Weakness #1: Theorem 4.1 critically assumes that the input space is convex...

Response:
Thank 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.

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

Weakness #2: The experimental comparison is weak... [Zhang et al., 2024] is not cited.

Response:
Our 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.

Weakness #3: Experiments are conducted on small datasets...

Response:
In addition to MNIST, we report results on CIFAR-10 using our NLP solver from (2a)–(2c), compared against MIP$_\text{CROWN}$ on identical tasks:

Despite CIFAR-10’s added complexity, our solver is ~3× faster with a tighter gap. This confirms our method’s scalability to larger networks.

Questions For Authors

Q1: Can your methods scale to CIFAR-10?

Response:
Yes — as shown above, our method scales well to CIFAR-10 and outperforms MIP$_\text{CROWN}$ in runtime.

Q2: Have you considered optimizing the search angle?

Response:
Yes, and we believe it could improve convergence by reducing overlap. We plan to explore this in future work.

Q3: Do adjacent balls intersect? Figure 4 suggests otherwise.

Response:
They can. Figure 4 shows a simplified case. We will revise it to depict overlapping balls explicitly.

Minor Comments & Suggestions

“Discontinuous” → “disconnected”

Response:
Agreed — will revise.

Clarify radius of ball

Response:
Defined as $r = \||x^* - c\||_p$, where $x^*$ is the nearest adversarial point, using the $l_p$ norm (see Section 2).

Perturbed inputs phrasing is confusing

Response:
We will clarify: perturbed inputs are adversarial only if they lead to misclassification (Goodfellow et al., 2014).

Is output scalar?

Response:
No — “scales” refers to scalability. We will revise for clarity.

“Cover entire verifiable space” is misleading

Response:
We will change to “tightly underapproximate the verifiable input space.”

Layer vs. neuron index

Response:
Index $i$ refers to the layer. We will clarify this.

Constraint classification

Response:
Only (2b) is nonlinear — we will clarify.

Redundant “then”

Response:
We will revise to remove “then.”

Notation reuse (e.g., $j$)

Response:
We will rename $j$ in Section 4.2 to $s$ for clarity.

Notation consistency

Response:
We will standardize all notation (e.g., $\mathbb{R}^n$).

Algorithm 1 indexing style

Response:
We will fix inconsistencies.

“Almost symmetric” / “$\varepsilon$-mismatch”

Response:
We will define “almost symmetric” precisely — angle > $\pi/2$ between $x_1 - c$ and $x_2 - c$.

“Disconnectedness” vs. “discontinuity”

Response:
We agree — will revise to “disconnectedness.”

Source of $\sqrt{2}$ term

Response:
It is from the $l_2$ norm difference between one-hot vectors, as in Fazlyab et al. (2021), Section II.D.

Section 4.3.2 formatting

Response:
We will revise the nested numbering.

Missing citation: Zhang et al., TACAS 2024

Response:
We will include this citation and clarify how their assumptions differ from ours.

References

• Fazlyab, M., Morari, M., & Pappas, G. J. (2021). An introduction to neural network analysis via semidefinite programming. IEEE CDC.
• Goodfellow, I. J., Shlens, J., & Szegedy, C. (2014). Explaining and harnessing adversarial examples. arXiv:1412.6572.
• Zhang, X., Wang, B., & Kwiatkowska, M. (2024). Provable preimage under-approximation for neural networks. TACAS.