Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification

We thank Reviewer wsa3 for the constructive and detailed feedback. We have included new experimental results on non-ReLU networks (ViT benchmark from VNN-COMP), as well as new experiments on solving difficult verification problems from real-world applications of NN verification. We will also enhance the discussion of the limitations of our work, as you suggested.

W1 & Q1: Unclear scalability of the proposed method on extremely large or complex neural networks.

Thank you for this important question about scalability! Our Clip-and-Verify pipeline is model-structure-agnostic and delivers strong performance across a wide range of network architectures and size. It is important to note that our work consists of various benchmarks that can scale to a large number of parameters. In particular, Table 2 shows our evaluation on the TinyImageNet (VNN-COMP 2024 [2]) benchmark consisting of models with up to 3.6M parameters and an effective input dimension of 9408. Additionally, we have extended our evaluation to transformers during the rebuttal period.. These results show that the efficacy of our approach extends to more complex architectures:

• Vision Transforms (ViT) (VNN-COMP 2023 [1]): A benchmark consisting of two vision transformer-based based classifiers, an effective input dimension of 3072, including complex nonlinear activations, such as dot-product self-attention and softmax. We presented the results below. Our method is able to verify three more hard instances on this benchmark and also reduced the average verification time on all instances by 50%.

In addition, we will also present a very hard task from a real application of NN verification, as published in a recent arxiv paper. We give more details in our response to W3 & Q3.

References: [1]: arXiv:2312.16760 [2]: arXiv:2412.19985

W2 & Q2: Limited evaluation on non-standard architectures and activation functions beyond VNN-COMP ReLU networks.

We emphasize that our framework is activation-agnostic. In particular, any neuron split of the form:

can be handled by updating the right hand side of our Equation 3 by absorbing $s$ into the offset such that our offset in the equation gets updated as $h \gets h - s$. Prior work [1] shows general splits of this form conveniently allow for a more general branch-and-bound paradigm that incorporates activations such as trigonometric functions and Sigmoid. We reiterate that our framework is indeed capable of more general and complex networks, and kindly refer the reader to our response to W1 & Q1 which present new results of the efficacy of our approach on vision transformer architectures. References: [1] arXiv:2405.21063

W3 & Q3: Dependence on benchmark datasets raises concerns about the method’s generalizability to real-world, safety-critical applications.

Thank you for this concern. Over the years, VNN-COMP has introduced complex networks that are used in a variety of applications. To name a few: LSNC (Lyapunov stability of NN controllers [2]), ViT (vision transforms), tinyimagenet (image classification), NN4sys (computer system [cite NN4sys bench paper]), AcasXu (aircraft collision detection [3]). Validating our approach on VNN-COMP allows us to fairly compare our work to other NN verification toolkits in a suite of diverse network architectures and applications. Additionally, our code will be open-sourced and our code is applicable to other scenarios, not exclusive to VNN-COMP benchmarks.

To show that our method is generalizable to real-world applications of neural network verification, and also demonstrate a very challenging verification problem, we apply our proposed method to a recent arxiv paper which has a challenging neural network verification task [1]. The paper addresses the problem of jointly training neural network controllers and Lyapunov functions for continuous-time systems with provable stability. In this paper, the authors presented two challenging verification problems (corresponding to physical environments considered in their paper): Cartpole and Quadrotor-2D, and they verified these problems using a state-of-the-art verifier, α,β-CROWN. These verification problems are very difficult - for example, for the Quadrotor-2D setting with a [0.2, 0.20001] region of attraction (ROA), they used about 2.5 days to verify with α,β-CROWN. We can verify the same problem using about 1/3 of the time. In addition, we considered an even more challenging setting with a larger ROA of [0.2, 0.21], which α,β-CROWN cannot verify within a few days of running, and we can solve it in about one day.

Here’s the total run time on these three verification tasks:

Here’s the total visited domains on these three tasks

The results on these three challenging verification tasks clearly show the effectiveness of our method. For these tasks, complete clipping is able to cut down the number of visited domains, and transfer the cut down in visited domains into a proportionate verification time decrease.

References: [1] arXiv:2506.01356 [2] arXiv:2404.07956 [3] arXiv:2201.06626

W4: Conceptual Similarities to Related Work: Although the proposed framework is novel, there are some conceptual similarities to related work.

We build upon the insight of utilizing linear constraints to tighten bounds. However, we emphasize that prior work such as [1], [2], [3], and more have explored this idea to refine the bounds of the final layer of a network to speed up verification. However, an important factor that is not considered in prior work is the tightness of intermediate layer bounds, which defines the tightness of verification relaxation and can consequently improve the final verification bound substantially. The challenge in this setting is that there are often many intermediate layer neurons in a neural network (thousands to millions), and it is very hard to refine these bounds in an efficient manner, that actually brings overall benefits that outweigh the cost. In contrast, our Complete Clipping approach is an efficient procedure that can efficiently utilize linear constraints to improve intermediate bounds without sacrificing scalability. Furthermore, our Relaxed Clipping procedure updates the input domain itself using a closed-form solution. To our knowledge, no prior work has simultaneously achieved intermediate-layer bound improvement in an efficient and effective manner as our proposed Clip-and-Verify framework. References: [1] arXiv:2103.06624 [2] arXiv:2208.05740 [3] arXiv:2501.00200

We thank the reviewer for the thorough review and insightful suggestions. We address each concern in detail below.

W1 & Q1: Justifications for top-k heuristics and additional ablation studies/comparisons

We agree that neuron selection is key to bound tightness in our clipping framework. The BaBSR heuristic, originally proposed for branching in branch‑and‑bound [1], scores neurons by estimating how much tightening their bounds would improve the final verification bounds. While BaBSR was designed for branching, our limited complete‑clipping budget requires similar prioritization—neurons with higher scores are more likely to yield significant bound improvements when clipped. We evaluated BaBSR against three alternative heuristics on the tinyimagenet benchmark (122 BaB‑verifiable instances, VNN‑COMP 2024) and cifar100, varying the number of selected neurons $k$ (Top‑10, Top‑20, or all). The heuristics include: BaBSR Strategic selection based on estimated bound impact [1]. U-L and -(U $\times$ L) Proxies that prioritize neurons with wide bound gaps. Random selection Baseline without strategic selection. For the top-k values, we expect a trade-off between computational cost and verification effectiveness:

• All neurons refined does complete clipping on every neuron, maximizing bound tightness but requiring the most computation
• Top-20 provides a balanced middle ground
• Top-10 uses minimal computation but may miss some important neurons Table for Time | Heuristic | Random | -U $\times$ L | U-L| BaBSR| |-|-|-|-|-| | Top-10 per layer (tinyimagenet) | 16.3s | 16.5 |16.8s | 16.2s | | Top-20 per layer (tinyimagenet) | 18.1s | 17.9s |17.2s | 15.1s | | All neurons refined (tinyimagenet) | 22.4s | 22.4s |22.3s | 22.7s | | Top-10 per layer (cifar100) | 26.2s | 26.6s | 27.0s | 26.1s | | Top-20 per layer (cifar100) | 29.1s | 28.8s | 27.7s | 24.3s | | All neurons refined (cifar100) | 36.5s | 36.4s | 36.4s | 36.5s |

Table for Domain Visited:

When all neurons are refined, results converge since no selection is involved. The table shows that better heuristics reduce verification time by prioritizing neurons whose clipping most tightens final bounds. BaBSR excels by targeting the most impactful neurons, enabling stronger relaxations and earlier pruning. U‑L and −U×L provide a reasonable but less precise proxy, while random selection often wastes effort on low‑impact neurons. References: [1] arXiv:1909.06588

W2: Evaluation of the trade-off

You are correct that subdomain reductions do not always scale linearly to runtime savings, a familiar tradeoff in neural network verification. Tight‑bound methods (e.g., LP‑based verifiers) are precise but slow and scale poorly, while fast methods (e.g., linear bound propagation) are efficient but produce looser bounds, often failing on harder tasks. Approaches like GCP‑CROWN [2] and multi‑neuron relaxations balance this by adding modest overhead in exchange for tighter bounds and better scalability. Similarly, our Clip‑and‑Verify pipeline introduces constraints efficiently, pruning infeasible regions and tightening intermediate bounds. On VNN‑COMP benchmarks, it consistently outperforms baselines, verifying more shared and unique instances, justifying its added cost much like GCP‑CROWN. To illustrate the trade‑off between clipping overhead and subdomain reduction, we analyze the lsnc benchmark (instance 0) using our BaBSR‑based heuristic, varying the number of neurons selected for complete clipping:

Complete clipping rapidly reduces visited domains and typically shortens runtime. This should be seen as a sign of strong pruning, not a drawback. In harder tasks—where many domains remain even after pruning—complete clipping sustains high GPU utilization and achieves substantial runtime gains. This is most evident in three challenging tasks from [1]: Cartpole invariant set, Quadrotor‑2D [0.2, 0.2 + 1e‑5], and Quadrotor‑2D [0.2, 0.21]. Without clipping, all three time out or run prohibitively long. With complete clipping, they become tractable:

• Cartpole invariant set
• Quadrotor-2D [0.2, 0.2+1e-5] invariant set
• Quadrotor-2D [0.2, 0.21] invariant set (larger ROA) Total runtime (seconds): |Method|Cartpole|Quadrotor-2D|Quadrotor-2D (larger ROA)| |-|-|-|-| |Relaxed clipping|460|209,504|Timeout| |Complete clipping|126|78,818|104,614|

Total domains visited:

Complete clipping cuts domains by orders of magnitude and turns infeasible problems into solvable ones (e.g., Quadrotor‑2D [0.2, 0.21] completes in ~29 h vs. timeout). In short, Clip‑and‑Verify’s overhead yields a decisive net gain in the hardest regimes. References: [1] arXiv:2506.01356 [2] arXiv:2208.05740

W3: Figure 1 is not intuitive and difficult to understand.

Thank you for this suggestion. We agree that a more concrete and visually guided presentation will help clarify the intuition behind relaxed and complete clipping. In the revision, we will make the following targeted changes to Figure 1:

• Simplify the example network (Fig. 1a): We will reduce the illustrated network to a small feedforward ReLU network with a scalar output. This enables us to add a corresponding 2D visualization of the input space.
• Add step-by-step illustrations: Show relaxed clipping refining the input domain and updating output bounds, and complete clipping tightening intermediate bounds, propagating changes to the final layer.

Q2:Could the authors provide a breakdown of runtime with respect to the difficulty level of subproblems (e.g., trivial vs. hard)? This would help clarify how the trade-off between fewer subproblems and their individual complexity affects overall performance.

Re: Please refer to the cactus plot in Figure 2 of our paper, which illustrates the number of instances verified as runtime varies. Each line represents a method, with the x-axis showing the cumulative verified instances under a given timeout (y-axis). This style, used in prior work [1,2] and in VNN-COMP reports (though transposed there) [3,4], effectively captures the trade-off between subproblem difficulty and runtime performance. Key interpretations: The curve’s right end indicates total solved instances—further right means more instances verified within the timeout.

A steep initial rise reflects many easy instances solved quickly.

A curve below and to the right of another shows consistently faster or earlier solving.

The x-axis ordering reflects instance difficulty, from easy (left) to hard (right).

For example, on the tinyimagenet benchmark (Fig. 2f), our Complete Clipping + BICCOS variant solves easy instances faster and solves more hard instances. Across these benchmarks, the proposed Clip-and-Verify framework demonstrates a favorable balance: it reduces the number of hard subproblems, leading to more instances being verified within moderate time thresholds. This suggests that although our clipping procedures incur additional overhead that may be noticeable in easy instances, the overall net gain is highlighted in its ability to solve more instances and hard instances with shorter verification times. References: [1] arXiv:1909.06588 [2] arXiv:2103.06624 [3] arXiv:2109.00498 [4] arXiv:2212.10376

>Q3: Lack of breakdown comparison on solving time for instances commonly verified by both the proposed method and existing baselines. Re: Thank you for your construction suggestions. Due to the space limit, here we will only present the instance-wise comparison on acasxu benchmark. In the final version of our paper, we will add this instance-wise results for other benchmarks to appendix D2.

For visited domain, our clipping method clearly exhibits its advantage over α,β-CROWN, especially for hard instances such as instance 65 and 73. For instance 65, beside α,β-CROWN other verifiers are also unable to verify it.

Here’s the instance-wise verification time on acasxu

The cactus plot (Fig. 2a) compares both mutually verifiable and previously unverifiable instances. Differences in curve length show that some methods solve more instances within the timeout. For example, on the ACASXu benchmark, relaxed and complete clipping each verify one more instance than α,β‑CROWN (x = 139), with complete clipping solving the hardest instance faster.

>Q4:For the results presented in Tables 2 and 3, as well as Figure 2, which variant of Clip-and-Verify is used? Relaxed + Reorder? Re: We used solely complete clipping with reorder in the results presented in these tables. We will make this more clear in the paper.

We sincerely appreciate Reviewer RvvA’s insightful and constructive comments. We clarify that our method is indeed model-structure-agnostic, and we add additional experiments which justify our use of the BaBSR heuristic for complete clipping as it improves performance with respect to time and number of domains visited compared to other heuristics. Below, we provide point-by-point responses, along with additional experimental results.

W1 & Q3: The method is only applicable to ReLU activation functions. Why is the proposed method restricted to ReLU activation functions, and what challenges arise if other activations are used?

Re: Our method is model-structure-agnostic as it relies on linear bounds which can be obtained via linear bound propagation like CROWN on any computation graph. In particular, when dealing with branch-and-bound on the activation space that is not necessarily ReLU, [1] shows that splits can be performed on a neuron to create two subproblems: $z_j^{(i)} \leq s$ and $z_j^{(i)} \geq s$, where $s$ is trivially 0 for ReLU neurons, i.e. the Planet relaxation. Equation 3 in our work shows how to perform exact bound refinement with a single constraint, and with an arbitrary split $s$, we can update this equation to be:

We can set the right-hand side of the inequality constraint to be 0 and absorb this arbitrary split into $h$ such that $h \gets h - s$. Therefore, equation 3 and the subsequent steps in our methodology are without loss of generality. To demonstrate the efficacy of our approach on non-ReLU networks, we present results on the ViT benchmark which constraints transformer layers.

References: [1] arXiv:2405.21063

W2 The paper provides few running examples, which limits intuitive understanding.

Re: Thank you for your suggestion, a simple running example would indeed foster intuitive understanding. Due to the character limitation, we are not able to attach our full step-by-step illustration that elucidates linear bound propagation, relaxed clipping, and complete clipping, but this detailed example will indeed be prepared for the final paper.

W3 Complete Clipping only targets the top-k key neurons selected based on heuristics; if the heuristic misidentifies key neurons, it may affect the final bound tightness.

Re: We agree that the neuron selection mechanism can play a crucial role in the bound’s tightness. To understand how top-k key neurons selection helps leverage solving time and visited subproblems, we did a series of experiments. To keep brevity, we put the experimental results and analysis in the response to Q1.

Q1 How does Complete Clipping determine the top-k key neurons using the BABSR intercept score, and what criteria are used in this heuristic?.

Re: To determine the top-k key ones within $H$ neurons, we will first compute the BABSR score over these $H$ neurons. The neurons with top-k big BABSR score will then be selected to run complete clipping on. BaBSR estimates the top-neurons which has the largest impacts on verification bounds. It was originally designed to determine which neuron to branch. In particular, we used the “intercept score” in BaBSR, which depends on the preactivation bounds to decide how loose the relaxation is for a certain nonlinear activation function. More details may be found in [1]. We evaluated BaBSR against three alternative heuristics on the tinyimagenet benchmark (122 BaB‑verifiable instances, VNN‑COMP 2024) and cifar100, varying the number of selected neurons $k$ (Top‑10, Top‑20, or all). The heuristics include:

• BaBSR: Strategic selection based on estimated bound impact [1].
• U‑L and −U×L: Proxies that prioritize neurons with wide bound gaps. U and L denote the neuron's upper and lower bound, respectively.
• Random: Baseline without strategic selection.

For the top-k values, we expect a trade-off between computational cost and verification effectiveness:

• All neurons refined does complete clipping on every neuron, maximizing bound tightness but requiring the most computation
• Top-20 provides a balanced middle ground
• Top-10 uses minimal computation but may miss some important neurons

Table for Time

Table for Domain Visited:

Note that when all neurons are refined, these numbers will converge since we are no longer dealing with selecting a subset of the neurons. This table reveals better heuristics actually reduce total verification time because they make smarter choices about which neurons deserve the complete clipping when only a subset is allowed to be refined. When BaBSR identifies the most impactful neurons—those whose bound improvements will most significantly tighten the final verification bounds—the resulting stronger relaxations allow the branch-and-bound procedure to verify more subdomains immediately and prune infeasible regions much earlier. The U-L and -U*L heuristic falls between these extremes because selecting neurons with larger bound gaps provides a reasonable but less precise proxy for impact compared to BaBSR's direct estimation of influence on final bounds, while random selection wastes complete clipping computation on neurons that may contribute minimally to verification progress.

References: [1] arXiv:1909.06588

> Q2: In line 787-788, what are the main limitations of Complete Clipping in handling networks with large hidden layers and sparse constraints

Re: Complete clipping requires us to solve a linear programming problem per neuron. While our GPU-parallelized implementation is an efficient procedure, the cost is not negligible when the number of subproblems is large during branch-and-bound. Further, although our method shows strong improvements, handling convolutional networks with possibly sparse constraints or objectives still offers room for improvement in our implementation. Our paper demonstrates significant improvements with complete clipping, but we believe there remains ample opportunity for future work to develop more effective top‑k objectives for critical neuron selection to further enhance refinement in large networks.

> Q3: Why is the proposed method restricted to ReLU activation functions, and what challenges arise if other activations are used?

Re: Our approach is agnostic to any activation function, and we’ve added new experiments on ViT (vision transformer). Our work can be naturally combined with existing work on branch-and-bound for general activations [1] . For example, [1] shows that splits can be performed on a neuron to create two subproblems: $z_j^{(i)} \leq s$ and $z_j^{(i)} \geq s$, where $s$ is trivially 0 for ReLU neurons, i.e. the Planet relaxation. Equation 3 in our work shows how to perform exact bound refinement with a single constraint, and with an arbitrary split $s$, we can update this equation to be:

We can set the right-hand side of the inequality constraint to be 0 and absorb this arbitrary split into $h$ such that $h \gets h - s$. Therefore, equation 3 and the subsequent steps in our methodology are without loss of generality. To demonstrate the efficacy of our approach on non-ReLU networks, we present results on the ViT benchmark (VNN-COMP 2023) which constraints transformer layers.

References: [1] arXiv:1909.06588

We sincerely thank Reviewer BXrA for the thoughtful and constructive feedback. To enhance our paper, we added additional experiments on very challenging verification queries coming from real applications, as well as non-ReLU models (ViT). Below is our response to the reviewer’s question.

W1: scaling verification to bigger models/harder verification queries

Thank you for your question. For our response to the scalability concern, please look into our response to question 1.

Besides the application to existing VNN-COMP benchmarks in our paper, our proposed method has been applied to other works which contain significantly difficult verification tasks. For example, neural network control system.[1]

The paper addresses the problem of jointly training neural network controllers and Lyapunov functions for continuous-time systems with provable stability. In this paper, the authors presented two challenging verification problems (corresponding to physical environments considered in their paper): Cartpole and Quadrotor-2D, and they verified these problems using a state-of-the-art verifier, α,β-CROWN. These verification problems are very difficult - for example, for the Quadrotor-2D setting with a [0.2, 0.20001] region of attraction (ROA), they used about 2.5 days to verify with α,β-CROWN. We can verify the same problem using about 1/3 of the time. In addition, we considered an even more challenging setting with a larger ROA of [0.2, 0.21], which α,β-CROWN cannot verify within a few days of running, and we can solve it in about one day.

Here’s the total run time on these three verification tasks:

Here’s the total visited domains on these three tasks

The results on these three challenging verification tasks clearly show the effectiveness of our method. For these tasks, complete clipping is able to cut down the number of visited domains, and transfer the cut down in visited domains into a proportionate verification time decrease.

References: [1] arxiv:2506.01356

Q1 Can you please specify the input dimensionality and layer sizes for which the efficacy of the proposed method may weaken?

Thank you for this important question about scalability limits. Our proposed method demonstrates strong performance across a wide range of network architectures and sizes. We have successfully evaluated on networks spanning from small models (thousands of parameters) to large-scale networks, including TinyImageNet models, 10 layers with 3.6M parameters and effective input dimensions of 9408, as well as ViT architectures (new results added during rebuttal period) with 2 Softmax layers (one Softmax layer introduce 5 unstable layers: 3 MatMul, 1 Exp, and 1 Reciprocal) and 2 ReLU layers with ~76k parameters and input dimensions of 3072. We also show our method can scale to the large vision transformer architecture:

Our approach is not fundamentally limited by input dimensionality or layer width. The core algorithms scale efficiently: complete clipping operates at $\mathcal{O}(n log n)$ complexity per constraint, while relaxed clipping requires only $\mathcal{O}(n)$ operations per input dimension. The memory complexity of complete clipping scales as $\mathcal{O}(B×N×M)$, where $B$ represents the number of BaB subproblems, $N$ denotes neurons in the largest layer, and $M$ corresponds to the number of linear constraints. When networks have very large hidden layers combined with numerous unstable neurons, we address potential computational bottlenecks through our top-k heuristic, which strategically selects the most critical neurons for complete clipping while maintaining global relaxed clipping benefits. Since the NN verification problem is NP-hard in general, the actual scalability depends on how difficult a verification query is. Input dimensionality and the number of layers are indirect factors. For example, in the Lyapunov control experiments added above, the dimension is low and the neural network size is small, yet the property is still challenging to verify since it is defined on a large set of input space with complex nonlinear constraints. Our experimental results on benchmarks ranging from ACAS-Xu (small networks) to TinyImageNet (large networks) demonstrate that the method maintains effectiveness across the entire model spectrum, so the scalability is not limited by our method, but mostly likely limited by the hardness of the verification problem. The key insight is that our approach adapts computational effort based on problem characteristics rather than being constrained by absolute dimensional limits, ensuring practical applicability across diverse verification scenarios.

Anonymous Authors

Thank you for the insightful connection to knapsack problems. We prove our algorithm is equivalent to the greedy knapsack approach with the same complexity. We also added experiments comparing LP and addressing your concerns below.

Q1. Connections to the continuous knapsack problem

Re: Thank you for the insightful reference to the continuous knapsack problem. We agree with this connection; our algorithm is equivalent to the greedy approach. Since our implementation is already identical, no new experiments were needed.

First, we would like to briefly outline the intuition behind our derivation, which allows us to prove the optimality of our solution based on the foundation of dual optimization theory. Specifically, we consider the primal problem:

We formulate the Lagrangian dual of this problem. Using strong duality, we convert the min-max to a max-min problem, and then eliminate the inner minimization using properties of dual norms. This yields the dual objective: $D(\beta) = (a + \beta g)^\top x_0 - \|a + \beta g\|_1 \cdot \epsilon + \beta h, \quad \beta \geq 0$

This function is concave and piecewise-linear in the single dual variable $\beta$. The nonsmooth breakpoints, where the gradient changes, occur at values $\beta_i = -a_i / g_i$. Our algorithm finds the maximum of this concave function by identifying where the super-gradient contains 0. This is done in $\mathcal{O}(n \log n)$ time via sorting the breakpoints. This yields a globally optimal solution, independent of any knapsack formulation.

To demonstrate equivalence to the continuous (fractional) knapsack problem, we perform the change of variables: $y_i = \frac{x_i - (x_{0,i} - \epsilon_i)}{2\epsilon_i}$ This transforms the primal problem into the standard knapsack form: $\max_{y \in [0, 1]^n} \quad r^\top y \quad \text{s.t.} \quad s^\top y \leq t$ where $r = -2\epsilon \odot a, s = 2\epsilon \odot g, t = -\left(g^\top (x_0 - \epsilon) + h\right)$. This is a continuous knapsack problem, potentially with negative coefficients. As noted by the reviewer and by [1](Sec. 1.4), such problems can be transformed into a standard form with positive coefficients:

• If $r_i \geq 0$ and $s_i \leq 0$: Set $y_i = 1$
• If $r_i \leq 0$ and $s_i \geq 0$: Set $y_i = 0$

These variables can be removed with corresponding adjustments to the capacity $t$. For the remaining variables with $r_i$ and $s_i$ having the same sign, we apply a further substitution to obtain all-positive coefficients, enabling the greedy solution. This leads to a line-by-line correspondence between our algorithm and the knapsack method:

• The efficiency ratios $r_j / s_j = -a_j / g_j$ used for sorting in the knapsack algorithm are identical to the breakpoints in our dual function.
• Both algorithms have identical time complexity: $\mathcal{O}(n \log n)$ (due to sorting).

Thus, implementing a knapsack-based algorithm for empirical comparison would be redundant—it would yield the exact same sequence of operations and results as our current method.

We will properly claim our contributions to this part, pointing out the connection and previous results in the main text, section 3.2, and leave the detailed discussions above in the appendix. We agree that the connection to the continuous knapsack problem is helpful for readers to better understand the structure and complexity of our problem. It is common in optimization to view a problem through multiple equivalent formulations. We believe our alternative derivation of the same algorithm remains valuable and insightful, particularly for readers with an optimization background. The existence of such a formulation does not diminish the contribution of developing a correct and efficient algorithm from a different theoretical foundation and applying it to the NN verification setting.

Finally, we emphasize that the core contribution of our paper is not the development of a solver for the single-constraint LP. Instead, our contributions are:

• The novel application of this fast, exact solver to the domain of neural network verification, for refining variable bounds, using cheaply obtained linear bounds from bound propagation;
• The integration of this solver into a larger coordinate descent framework, enabling efficient handling of many-constraint problems without relying on generic LP solvers, while being effective, enabling scalable neural network verification. * Our overall framework is highly scalable and achieves state-of-the-art performance on difficult verification tasks. While the subproblem solver may be equivalent to a known approach, its application and integration within our verification pipeline are novel, and this is what constitutes the main contribution of our work.

[1] Kellerer, Pferschy, and Pisinger. "Knapsack Problems"

Q2. Comprehensive Comparison with LP Solvers

Re: Thank you for this excellent suggestion. We acknowledge that a fair comparison should evaluate our coordinate ascent method against LP solvers with iteration limits rather than only comparing to LP solvers run to optimality. During the rebuttal period, we conducted additional experiments below and the results strongly validate our approach. We incorporated LP solvers into our BaB framework, using them to solve the primal form for each batch of neurons per layer. We tested dual simplex with varying iteration limits (1, 10, and 20 iterations) on the acasxu benchmark instance 65 (the hardest instance in the benchmark, which cannot be solved without clipping). The verification pipeline for LP and ours are exactly the same (following algorithm 4), and the only difference is whether we solve the clipping problem using LP or our proposed method. We report the time for the optimize() function in gurobi, ignoring all overhead on creating the LP problem (this should give an advantage to the LP solver). Here are our findings:

The reported bounds and time are averaged over 30M LP calls during the entire BaB process, so the numbers are statistically significant. Noted that Gurobi will run its presolve routine before starting the dual simplex algorithm, and the dual simplex algorithm cannot begin iterating until it has a valid starting point—an initial basis factorization. The process of creating this initial basis is a one-time setup cost within the m.optimize() call. This cost is identical whether we subsequently run 1 iteration or 20, so the time cost $t_{total} = (t_{presolve} + t_{basis \ construction}) + (n_{simplex \ iter} \times t_{per \ simplex \ iter})$

These results demonstrate that our coordinate ascent method achieves:

1. 740× speedup over even the most limited LP heuristic (1 iteration)
2. Comparable accuracy to 10-iteration LP while being 880× faster
3. Near-optimal bounds (error of only avg. 0.00085 compared to full LP solution)

The performance difference stems from fundamental architectural considerations in neural network verification:

GPU Parallelization: Our coordinate ascent algorithm is specifically designed for massively parallel execution on GPUs. We can process thousands of neurons simultaneously, leveraging the GPU's architecture. In contrast, LP solvers like dual simplex are inherently sequential and cannot effectively utilize GPU parallelism.

Scalability Requirements: Modern neural network verification requires processing networks with millions of parameters and thousands of subproblems in branch-and-bound. Even with iteration limits, LP solvers introduce prohibitive overhead when called repeatedly. The neural network verification community has reached a consensus that scalable verifiers cannot rely on LP solvers at any stage - this is why state-of-the-art verifiers like α,β-CROWN [52], Mn-BaB [22] have moved away from LP-based approaches.

We will revise our paper to include this comparison table and clarify that our efficiency claims are validated against both exact LP solvers and LP-based heuristics with iteration limits. This strengthens our contribution by demonstrating that our method outperforms LP solvers even when they are used as fast heuristics rather than exact solvers.

[22, 52]: in our reference

Q3. Direct Proof for Relaxed Clipping

Re: We appreciate your suggestion for a more intuitive proof. This geometric interpretation is clearer: we push all other variables to their constraint-loosening extremes to maximize the feasible range for $x_i$. We will include this direct proof alongside our duality-based derivation in Appendix B.3.

Q4. Top-k Heuristic Details for input split

Re: For the input split method, we refined all neurons in each step without a top-k heuristic. This approach was computationally feasible because the benchmarks used were relatively small (e.g., ACAS-XU with 300 neurons, LSNC with 406). However, for significantly larger networks, a top-k heuristic like the one we used for ReLU splitting would be beneficial to reduce computational cost. We discuss this strategy in detail in our response to Reviewer XvZp (Q1).

Q5 ReLU Splits and Relaxed Clipping

Re: We use complete clipping for ReLU splits as relaxed clipping is ineffective. A single ReLU constraint, $A x+c​\geq0$, gives loose bounds in high dimensions. Our branch-and-bound procedure accumulates many constraints, allowing complete clipping to use them simultaneously for tighter bounds. Section 3.5 provides further geometric intuition.