Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification
Authors: Duo Zhou
Jorge Chavez
Hesun Chen
Grani A. Hanasusanto
Huan Zhang
Venue: NeurIPS 2025 poster ()
Keywords: Neuron Network Verification; AI Safety; Robustness; Formal Methods
Primary area: social_and_economic_aspects_of_machine_learning

Abstract: State-of-the-art neural network verifiers demonstrate that applying the branch-and-bound (BaB) procedure with fast bounding techniques plays a key role in tackling many challenging verification properties. 
In this work, we introduce the \emph{linear constraint-driven clipping} framework, a class of scalable and efficient methods to enhance bound propagation verifiers. Under this framework, we develop two novel algorithms that efficiently utilize constraints to 1) reduce portions of the input space that are either verified or irrelevant to a subdomain in the context of branch-and-bound, and 2) directly improve intermediate bounds throughout the network. 
The process novelly uses linear constraints that are readily available during verification in a highly scalable manner compared to using off-the-shelf linear programming (LP) solvers. 
This reduction tightens bounds globally and can significantly reduce the number of subproblems
handled during BaB. We show our clipping procedures can intuitively and efficiently be incorporated into BaB-based verifiers such as $\alpha, \beta$-CROWN, and is amenable to BaB procedures that split upon the input or activation space. We demonstrate the effectiveness of our procedure on a broad range of benchmarks where, in some instances, we witness a 96\% reduction 
in the number of subproblems during branch-and-bound, and also achieve state-of-the-art verified accuracy across multiple benchmarks.

Clip-and- Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification
Duo Zhou"
Jorge Chavez"
Hesun Chen
Grani A. Hanasusanto Huan Zhang
University of Illinois Stbana-Champaign joroee,,, hesunc2, gasumciiga edu, huan@huan -aaann.. com
"Equal Contribution
Abstract
State-of-the neural network (NN) verifiers demonstrate that applying the branch- and-bound (BaB) procedure with fast bounding techniques plays key role tackling many challenging verification properties. In this work, we introduce the linear constraint-die driiee clipping framework, class of scalable and efficient meth- ods designed to enhance the efficacy of NN verifiers. Under this framework, we develop two novel algorithms that efficiently utilize linear constraints to 1) reduce portions of the input space that are either verified or irrelevant to subproblem and 2) directly improve intermediate bounds throughout the network. The process novelly leverages linear constraints that often arise from bound propagation methods and is general enough to also incorporate constraints from other sources. It efficiently handles linear constraints using specialized GPU procedure that can scale to large neural networks without the use of expensive external solvers. Our verification procedure, Clip-and-Verie consis- tently tightens bounds across multiple benchmarks and can significantly reduce the number of subproblems handled during BaB. We show that our clipping algorithms can be integrated with BaB- BaB-based verifiers such as R,8-CROWN, utilizing either the split constraints in activation-space BaB the output constraints that denote the unverified input space. We demonstrate the effectiveness of our procedure on broad range of benchmarks where, some instances, we witness 96% reduc- tion in the number of subproblems during state-of-the-as verified accuracy across multiple benchmarks. Clip-and- Veriify is part of the 3BR-COW verifier, the VNN-COMP 2025 winner. Code available at https: htt.aa/ccoooooeo.eeaaeaaeeeaaaaa helpiignnneeeeppppeeeeee Verify
in the context of branch-and-bow
and also achieve
Introduction
The neural network (NN) verification problem is imperative mission-critical applications 70 58 [6] 75 (22 where formally proving properties such as safety and robustness over specified input domain is essential. Recent approaches make neural network verification more tractable by relaxing the original non non-convex problem into convex formulations that are amenable to linear programming semidefinite programming (SDP)
18 19], and bound propagation- These convex relaxations can be further strengthened by tightening single-neuron relaxations through convex geometric analysis (55), constructing convex- hull approximations to capture multi-inpun dependencies 48], and introducing cutting planes that encode inter-neuron dependencies 776 79). To handle properties that cannot be certified by a single relaxation, sate-offthhearr verifiers couple bound propagation methods with the branch-and-bound (BaB) paradigm 14 66 5 [3 as this technique can be efficiently parallelized and scaled on
(LP)
25
based solvers 77
29
55
67
24
66
64
GPUs. Linear bound propagation methods such as CROWN [77] recursively compute bounds on the activations of each layer, referred to as intermediate bounds, which serve as critical building blocks for determining the tightness of the overall relaxation and for guiding the BaB search.
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

While BaB and cutting- pattinng-paaeeeeee techniques can further refine the relaxation by incorporating additional constraints at the final layer, they cannot directly and efficiently improve the intermediate bounds themselves. In BaB, where the number of subproblems grows exponentially, loose intermediate bounds weaken the relaxation, resulting in deeper branching and longer verification times. Although algorithms such as 3-CROWN [66] theoretically support optimizing bounds at intermediate layers, doing so in practice is prohibitively expensive as the number of hidden neurons typically outnumber the output neurons used for property verification by several orders of magnitude. Consequently, updating bounds for all intermediate layers introduces significant computational overhead that far outweigh the gains brought from their tighter convex relaxations. As a result, existing implementations fix the global intermediate bounds computed at initialization (e.g., via a- G-CROWN (74) and focus their optimization efforts solely at the final layer. While this design choice preserves scalability, it limits the ability to tighten the relaxation throughout the network, motivating methods that can refine intermediate bounds both effectively and efficiently.
To this end, we introduce Clip-and-Veriee a verification pipeline designed to enhance NN verifiers by opportunistically refining bounds at any layer with minimal computational overhead. Our core insight is that the bounding planes generated by linear bound propagation at all layers naturally align with our pipeline, enabling us to exploit their geometry to eliminate infeasible regions of the input domain and prune redundant subproblems early in verification. We formalize the task of tightening any layer's 's bounds the objective of our linear constraint-driven clipping framework, and we propose two novel algorithms: complete clipping, which directly optimizes neurons' bounds via a specialized coordinate ascent procedure, and relaxed clipping, which refines the input domain to enhance the intermediate relaxations and consequently improves the NN's bounds. An intuitive illustration of this refinement is given in Figure T. and our main contributions are as follows:
We propose two specialized GPU algorithms within our novel linear constraint-driven clipping framework for tightening bounds at any layer, preserving the scalability of state-of-the-art NN verifiers without relying on external solvers. Relaxed clipping optimizes the imput domain bounds as a proxy, offering good improvements with little costs, while complete clipping employs a customized coordinate ascent solver to directly refine the bounds at every layer of the NN.
We show that linear bound propagation methods produce linear constraints that can be obtained "for free" during both input and activation BaB procedures. By leveraging these cheaply available constraints and integrating our two efficient clipping algorithms, we introduce Clip-and- Verify, a verification pipeline that tightens the all neurons bounds with minimal computational overhead.
Across large number of benchmarks from the Verification of Neural Networks Competition (VNN-COMP) [ and existing literature, we demonstrate that our Clip- Verify framework is capable of reducing the number of BaB subproblems by as much as 96% and consistently verifying more properties on benchmarks from the Verification of Neural Networks Competition.
2 Preliminaries
The NN Verification Problem. Given some input belonging to the set X' and forward network ʃ(-) with general activation functions, the goal of NN verification can be formulated as verifying f(x) 2 0 for all inputs in X. One manner of verifying this property involves solving minnex I (ar), which challenging due to the non-convexity of the NN and is generally NP-complete [35 On the other hand, convex-reaxxation algorithms compute a sound, approximate lower bound, f(x). to the network's 's true minimum such that when fx) > 0, the property is sufficiently verified, otherwise the problem is unknown without further refinement or falsification.
approximate neuron bounds layer by layer by relaxing the nonlincarities of activation functions, making these techniques a fast and popular approach for NN verification. For L-layered, feedforward network, the bounds for the 5th neuron at the 7th layer may be expressed as:
Bound Propagation. Linear bound propagation methods 156 55
min A E
(T)
x
+
(1)
< 2
(1)
max A xEX
T x +
(I)
When X' is an Lo box (i.e. of the layer using Lemma
x
|| 01100 I c)), we may "concretize" the lower and upper bounds
B.I
200) A (1)
(i) le + clt) and (0)
(i) a + A (3) (()
Once concretized, the post-activation neuron,
(() $)
may be bounded (e.g. via Planet relaxation 25 for
2

---

Collected Constrainte
Cllp domain
Ioupeova Bosnnd
Goal: tighten the lower bound of
3/1
222
Relased Chipping
Hayed
Inpur region
plli constraint
onigui conaiimiii
2F2
clip on
222
1g frastble
trasible
2.2.1
9-3
R1
Clipping
Lineaz Lower bound
Linearly relaxed constrsints
371
(b)
Figure 1: (a) Linear bound propagation produces linear bounds on all neurons w.r.t. the input. These linear bounds are later used as linearly relaxed constraints. figure (a), the blue and the red lines are used as the linearly relaxed boundary of constraint 22 S 0 and S O. Our goal is to further tighten (6) Linear constraints (e.g. split constraint 22 S 0 and output constraint y1 I 0) can be applied to shrink the input region and provide tighter bounds. In Relaxed Clipping. the feasible region is relaxed its tightest covering box. In complete clipping, the infeasible region is completely cropped off, leaving the exact feasible region to improve bounds on. Both two clipping methods improve the bound to 21 clipped but due to the relaxation nature, Relaxed Clipping yields looser 2]
the lower bound of 2 via these constraints;
elipped A detailed numerical example given Appendix C.5
ReLU), The lower/upper bounding planes, A
(f)
A (4)
and (())) /c( are produced via backpropagation,
and their definitions are given in Appendix A determine if the problem is verified.
The lower bound at the final layer, 2 is used to
systematically partitions the verification problem into smaller subproblems, X X U X2, enabling tighter bounds on each subdomain. BaB split upon the input space (e.g. axis-aligned constraints) the activation space (e.g. split activation neurons). See Appendix A. for the formal definition and complexity implications. The exponential growth of subdomains can lead high computational cost but be mitigated by verifying domains early and often, a direct consequence of Clip-and- -eir-ffy-Verrfy..
Baanchandd-oundd The BaB paradigm 14
66
53
76 79
3 Enhancing Neural Network Verification with Clip-and- Verify
3.1 Motivation and Overview
BaB-based verifiers manage complexity by partitioning the input or activation space into tractable subproblems. Within each branch, linear relaxations provide bounds the network's 's neurons which can guide branching decisions and verify properties. Crucially, the constraints introduced at each BaB split implicitly define tighter feasible imput domain and offer opportunities refine the bounds at any layer. As shown in Fig. [b] linear constraints can shrink an &o norm ball during robustness verification, yielding tighter intermediate bounds and enabling more effective search-space pruning.
In large NNs, full linear bound propagation is often limited to an initial pass for efficiency. Alternative methods like using LPs to update intermediate bounds (5I) or full re-propagation after each split also prove too costly. Such overhead restricts frequent bound updates in deep NNs or extensive branching.
To fully exploit these opportunities, we propose Clip-and- Verify, pipeline which tightens the input box and re-concretizes intermediate bounds at each BaB node using linear constraints (c.g. activation split and final layer bound). without running full pass. It contains two algorithms: Complete Clipping, which performs a fast coordinate- wise dual search with sorted breakpoints per constraint to obtain near-LP tightening at fraction of the cost, and Relaxed Clipping, which performs per- constraint exacr tightening for axis-aligned boxes by solving the one-dimentn mie-iimensional dual in closed form and then re-concretizing cached linear constraints over the shrunk box.
3.2 Complete Clipping: Optimizing Intermediate Bounds Directly via Linear Constraints
Exact Bound Refinement with a Single Constraint via Optimized Duality. Suppose we wish to improve the lower bound of a linear function x + over an input domain X, given new linear

---

constraint g"x + h S O. The primal optimization problem is:
min (a T + g a + h 50 øEX
Instead of directly solving this potentially high-dimensional LP, we formulate its Lagrangian dual. The key advantage and insight is that, for fixed dual variable 3 E R., the inner minimization over a can be solved analytically for box domains, transforming the problem into a simpler optimization over single dual variable. This leads the following theorem:
Theorem 3.1 (Exact Bound Refinement under a Single Linear Constraint), Let a IR, IR, RR, h E IR, and the input domain be X' { á 6. S S & + c}. The optimal value I.* of the constrained minimization problem (2) is given by the solution the dual problem:
== max BERI
(a [g) Φ
Σ (a 3g) +c
(3)
j=l
Dunl Objective (f))
D(3) in is concave and piecewise-linedt in B E R.. Its maximum L and the optimal 3 can be determined exactly and efficiently by identifying its breakpoints (values of 3 where (a + Bg), = for some j E (nl) and analyzing the super- super-gradient gradients within the resulting linear segments.
For proof, Appendix B.2 Theorem 3.1 converts potentially expensive n-dimensional LP into a ID concave maximization problem (D(B) that can be solved without iterative gradient methods. The process of finding breakpoints and the optimal segment (detailed below and in Algorithm | for the multi multi-constraint case) is highly amenable to efficient computation, making suitable for refining bounds across many neurons and subdomains in parallel. An analogous theorem holds for tightening h S 0}.
the upper bound by solving max x +
Before optimizing Eq. (3). infeasibility can be detected a priori: the problem is infeasible iff g _ + h Σ [gile > 0. Such a scenario arises when the property being verified imposes constraints unsatisfiable within the current input domain X' (e.g., contradictory ReLU assignments), and may be considered verified without further refinement.
Note that our primal optimization problem is mathematically equivalent to continuous knapsack problem which can be obtained via change of variables as detailed in Appendix [33 The breakpoints
3 - -a:99 /9: in our dual formulation are identical to the efficiency ratios r used in the standard greedy knapsack algorithm. Thus, our dual-based solver and the greedy knapsack algorithm are equivalent, both finding the provably optimal solution with On log n) complexity.
Coordinate Ascent for Multiple Constraints When multiple linear constraints Ga h < (where G E R=x", h R"") are available, the dual problem involves optimizing multiple Lagrange multipliers B Ry:
" L' max (a + BT G) - Σ (a (3++3"G))le; +c+ BER
(4)
The single constraint problem
easy solve using Theorem thus we can use coordinate ascent to solve (4). Algorithm details single pass of this coordinate ascent procedure. This iterative approach optimizes one dual variable 3g at a time, keeping others fixed. Each step thus reduces to solving the ID problem described in Theorem 3.1 (with a replaced by a a Eppx&B,G. and g replaced by ). Since the dual objective remains concave and piecewise-lincas along each coordinate Se. we can efficiently exploit the breakpoint structure for each update. An order dependency is discussed in Appendix B.5] Algorithm [ is significantly more efficient and scalable LP solvers, even when those solvers are used as fast heuristics to get a bound rather than converge to optimal. We conducted a detailed comparison in Appendix [.3] integrating a state-of-the-arr LP solver (Gurobi) into our BaB framework. The results show that even when running dual simplex with 10-iteration limit, the LP solver was over 880 slower than our GPU-parallelized coordinate ascent (0.0028s vs. 2.47s per round) while achieving comparable bound accuracy (0.00085 vs 0.0007 mean error).
than using general-purponn

---

Algorithm 1 Coordinate Ascent with Multiple Constraints
Require: Objective
T x + c: a E R", c R; Constraints Gæ + h v 0: G R h R
1: B + [O.....
0] Initialize vector of m Lagrange multipliers as zero]
2: Φ f- æ+v
2-- Initialize centroid and the radius of the input hyper-rectangular)
2
3: for constraint k in [ do
4: q < (a + 3 G)G (Calculate the breakpoints)
5: I < argsort( ④)
6:
g イ Gk.:l @ (Scale by box half-widths)
7:
Isontd t 9r (Reorder by the same argsort index T}
8:
9
-- _j=1(19onoc (j),j E [r>] ((Negative) cumulative sum of sorted breakpoints]
g (+) t g (-) - -1 (Shift g to its positive range)
9:
Vg + g + +g' GR..a 11. h& (Supergradient; monotone nondecreasing in i)
11:
1 t minfie [n] Vg. S 03 (First sign change]
12:
J I,- (Map the i"-th breakpoint in the sorted order back to the original coordinate index)
13:
BR f max (g.. ; 0} (Ensure feasibility]
14:
1' C a B G c (a (a+ G)G a 3Th + (Calculate dual objective]
Ensure: 1*
3.3 Relaxed Clipping: Optimizing Intermediate Bounds Indirectly via Input Refinement
Although the coordinate ascent is significantly efficient compared to LP solvers, it is still computa- tionally expensive when there are various subproblems with many unstable neurons and multiple constraints. To address this issue, we propose a more efficient Relaxed Clipping algorithm, which shrinks the input domain by leveraging linear constraints (e.g., from final-layer outputs or activation branchings) to shrink axis-aligned portions of the input. By adopting a box input domain as proxy. we avoid repeatedly solving linear programs for each intermediate-layer neuron, and can solve the resulting optimization problem efficiently via the dual norm without relying on external solvers. The remaining task is determine the clipped box X' C X' that best respects the constraints.
We assume a hyper-rectangular input region and a set of m linear constraints Ax + S O, with A mm and e E R". To refine the lower and upper bounds of the input along each input dimension i E [ma]. we solve:
Formulating Relaxed Clipping for a Elyper-Rectange
2 == min =
Ax + S 0),
max
Ax + S).
(5)
=EX
These refined bounds, 22, and m; clip the original domain X' reflect only the portion that satisfies all the linear constraints. We derive a simple closed-form solution when there is only one linear inequality, a² x + c
S 0, foregoing the need solve 55) via LP solvers or gradient-based methods.
Theorem 3.2 (Relaxed clipping under a single constraint). Let x E X' and a T x + c S 0 be the sole constraint. For brevity, denote the closed-form solution as ae = -- 1 -l, Then, for each coordinate i, the new upper (or lower) bound is updated as follows:
c)/ a,
2
(new)
min
x
(clip)
IG
if aa; >0
2 (new)
maxx
(elip)
ifa; <0
no change
otherwise
Appendix B.4 gives a proof showing that, for a single linear constraint a x + c < O. we can clip the box X' to new box X' in one pass using the closed-form updates in Theorem 3.2 without any external solvers. The resulting box is the tightest axis-alignas exis-aligned over-approximation of the feasible set X' n (æ: a + c 0} C X' C X, and it is component-wise tight: no coordinate bound of X' can be further refined while remaining a box that still contains the feasible set. The computation costs only (n)) arithmetic operations. For example, re- propagating bounds for network with intermediate layers (4096, 2048, and 100 neurons respectively) and containing 800-1600 unstable neurons can take 10s per subdomain, versus 0.3s when re-concretizing the intermediate bounds.
This Relaxed Clipping step complements Complete Clipping. Whereas Complete Clipping solves problem (3) for each neuron, Relaxed Clipping tightens the shared input box X' once, and then
5

---

all intermediate bounds are cheaply re-concretized over this tighter box, yielding network-wide bound improvements from a single cheap update. By keeping the shared domain as a box, we avoid polyhedral operations and repeated per-neuron optimizations, substantially improving scalability.
Clipping for Multiple Constraints. When several linear constraints are present, we apply Theo- rem 3.2 in parallel to each constraint in Az + c S 0. Algorithm outlines this procedure: Given the original box bounds, E and Σ, we compute its center and radius, & and c. Then, for each constraint k and dimension i, we apply Theorem 3.2 independently and in parallel refine E; and H,, After processing all constraints, the resulting clipped bounds are aggregated, and the tightest bounds selected to form the final clipped domain. This formulation preserves scalability and supports parallelization. We present a sequential variation in Appendix C.2 that foregoes parallelization for further refinement in which the box center and radius are recalculated after each constraint is applied. Nonetheless, we emphasize our current formulation as a core strength of domain clipping, maintaining both efficiency and effectiveness. Similar direct clipping, Algorithm 2 may identify infeasibility by returning clipped bounds where a is larger than T along some dimension(s).
Algorithm 2 Linear Constraint Driven Relaxed Clipping (Parallel)
Require:
T Input lower bounds; 3 Input upper bounds; Ax S c Constraints.
1: ④: 5- Z+E 6
2 Z- x (elciipped) t- 22 (cllpppped) <- T [Initialize the original bounds]
2: for each constraint k (1, ..... (A) do
3: for each input dimension i E (1, cols( A)) do
4: x
(new)
-ize Ac, + -,z, A Ck
(Update x using Theorem 3.2
Ab,
5:
if
A 2 0 then
6:
(clipped) min (
(clipped)
x.
((ew)) (Iteratively tighten the upper bound)
7:
else
(clipped) max(ạ, (clipped) L x (elipped), ((clipped)
(clipppl
x (now)) [Iteratively tighten the lower bound]
8:
Ensure:
We have discussed how to use the linear constraints to tighten bounds, the next step is to find these linear constraints. We can use output constraints or activation split constraints during BaB. The next two sections we will discuss how to find the constraints and incorporate our algorithm into BaB.
3.4 Integrating Clipping into Input BaB Verification
In input BaB, the verifier partitions the network's ' input region (often an -box) along axis- splits, generating multiple subdomains { Each subdomain is then fed into a bound-propagation verifier (e.g., CROWN) obtain linear hyper-planes that are used to lower-bound the final-layer output with respect to the input. Existing verifiers typically use these final-layer hyperplanes only to compute the bounds and decide whether the entire subdomain can be immediately verified or must be further subdivided. It may be the case that the hyperplanes used for computing the final layer bounds are tight enough verify a subset of the input, but not tight enough verify the input in its entirety (see Fig. g in Appendix). The key insight is that we can remove infeasible parts in a subproblem via linear constraints and then consider a partially verified problem the next iteration of BaB. These already calculated hyperplanes can then be effectively re-used as constraints, making them appropriate for our clipping paradigms.
Using Final- Bounds for Clipping. After a subdomain has been bounded, the final-layer's bounding plane(s) are retained after concretization if the subdomain cannot be fully verified. For the verification objective, f(x) 2 O, it suffices to verify the input region, {x a (L) x + c(4) 2 0}. In this case, the bounding plane acts as constraint that separates this verified subset from the complimentary subset of the input domain that requires further analysis, i.e., {x (1)T x+((l) < 0}. For verification problems with multiple output conditions in the form of fi 2 0 f2(2) Z 0 A ^ (Tx 2 0, we can have multiple linear bounds (1) one for each clause, and all of them can be used. Rather than treating each property separately, we jointly collect all relevant final-layer constraints and apply them using Algorithms and accelerating batch verification on GPU,

---

Modifications to the Standard Input BaB Procedure. Algorithm 4 in Appendix outlines our modification to the standard input BaB loop, highlighted in brown. Our first key modification after bounding batch of domains, is that we perform relaxed clipping after we split the domains. This reordering allows two child domains to inherit their parent's constraint after axis-aligned split. The inheritance enables more tailored domain clipping procedure for each child, which is often more effective than clipping the parent domain directly. The resulting subdomains are reinserted into the domain list along with their associated constraints. In the subsequent bounding step, we perform complete clipping for the unstable neurons in each layer, where constraints are leveraged to directly to tighten the lower/upper bound objectives. When the number of unstable neurons is large, we heuristically select a subset of critical neurons for Complete Clipping: the selection heuristics are detailed in Appendix D.4 Neurons not selected for complete clipping still benefit indirectly, their concretized bounds are refined due to the clipped domain inherited from the prior BaB iteration.
3.5 Integrating Clipping into Activation BaB Verification
We now demonstrate how our clipping framework naturally extends to branch-and- on the activation space. Our method is cecivation-agnostii as it operates on general linear constraints derived from any activation split. For given neuron 2]
(6) BaB can introduce splits of the form
(1) 2 or 2; S where s is a split point (s 0 for a ReLU split) This inequality can be relaxed by bound propagation algorithms and expressed as a linear constraint on the input, g' x + h I 0, which is directly usable by our algorithms. This flexibility allows our framework to apply to networks with various activation functions, as demonstrated by our experiments on Vision Transformer models in Section 4 By assigning certain unstable neurons to either regime, we obtain linear relaxation split constraints that can further optimize the intermediate bounds, boosting verification efficacy. A key insight is that many constraints from multiple activation assignments can accumulate, potentially tightening intermediate bounds significantly.
3j
Using Linear Constraints in Activation Space for Clipping, We prioritize neurons whose convex envelopes incur the largest relaxation error; for ReLU this typically coincides with "unstable" units (Appendix A.I.. At any BaB node with input box Nr linear bound propagation yields, for each neuron (1,5),
1 T
x
60 S 22 (x)
x
Vo E X₂
(6)
(1) Then we can validate of activation-space linear constraints. If branch assigns 2) 2 then any feasible x must satisfy
x 2 A TT)
since 2/ (z) S A
x x x Symmetrically, for 2) (1) S s we obtain the necessary condition
A T c s. Thus the activation-branchingg provide sound linear constraints in the input space that encode the assigned activation regime.
We can cache and reuse the initialized activation branching linear constraints. When bound initializa- tion is executed at a node, we cache (A, c) and (A, Z) for all "unstable" neurons, and further use the constraints based on the branching domains during BaB to do (i) Relaxed Clipping: treat (7) (and its lower-bound analogue) as box-consistency constraints and update X₁ + X in closed form following Algorithm. 2). (ii) Complete Clipping: on a selected set (()) of neurons, we directly tighten their per-neuron affine bounds using the same constraints using Algorithm. | their original bounds, but still tighten indirectly when re-concretized over X²
Neurons not in ((P) keep
Here, C(P) is the set of "critical neurons" that are heuristically expected to benefit most from bound refinement. While one could apply our method to every neuron in the network, this may be challenging for networks with high-ding eigh-dimensional hidden layers. To address this, we propose a top-k objective selection heuristic that adaptively selects neurons based on the BaBSR intercept score [33. This heuristic strategically prioritizes neurons whose refinement is most likely to tighten the overall verification bounds. detailed justification for this choice, including an ablation study comparing BaBSR to other common heuristics, is provided in Appendix D.4] Neurons not selected by this heuristic retain their standard bounds as computed by CROWN but may still benefit indirectly from relaxed clipping. Since relaxed clipping is computationally lightweight and highly scalable, it should always be applied to refine the input domain as effectively as possible.
7

---

Table I: Comparison of different toolkits on few representative VNN-COMP benchmarks with input BaB. "." indicates that the benchmark was not supported. Time calculated as the total time taken to verify verified instances. The number of BaB subproblems by a, B-CROWN is set as the baseline, and the reduction rate is calculated from this number. Complete clipping significantly reduces the number of subproblems during BaB, while relaxed clipping is sometimes faster overall. Reordering generally helps reduce time and subproblems.
banc
nadeys
Method
limets)
subproblems
vetilled
timets)
subproblems
Af eetilled
timets)
subpeoSlems
veriteed
munumm
213.41
130
Mambburt
1342,00
133
151.31
PyRAT=
30
90-40
1484.39
137
704.55
53
Never2
10
1365. 78
121
NNV1
2633.49
70
Come
1566.80
134
22.88
NeuralSAT
1316,85
136
CROWNN
115.27
142,293,985
280.51
7,154,357
138
1580.66
4,440,252
Clip and Veridy (Ouss)
Relesed clipcing
99.12
02.4002227-95.17
22.-2-3-11 398
151.37
100456 305
139
1193,99
15911259949.... 495
Relased + Reorder
98:42
66.412.652-00
40
150.25
2.557.715104 sog
133
1166.08
2,700,894
194
Complete elipping
5,334,221
.90.90
168.57
1,533066
2,141,288
Table 2: Performance of Clip-and- Verify on challenging control system verification tasks. Complete clipping is essential for verifying the most difficult properties. The timeout is 3 days (259,200s).
cartpole
Quadrotor
22
Quad 20 Large
Method
time(s)
subproblems
timo(s)
subproblems
time(s)
sabproblems
P.B8-ROWN (No clipping)
1602
54,260,909
timeout
timeout
Clip and Verily (Relaxed clipping)
484
16,453,971
488.77 7%
209.504
2,630,043,050
timeout
Clip-and and Verily (Complete clipping)
2,438,359
95 5%
1,112,917,436- 57
104,614
1,472,33,971
CLOCN Clp-aan Nartly
200
BCROWN
CONCRROW' ropp csta
lartly (Camplaoe)
150
B10006
100
Cel-erddeell DOCCO
Leafl (200))
102
112
155
133
121
128
130
136
140
20
0
20
90
80
50
100
(a) acasxu
(b) Isnc
(c) cifar-enn-b-ady
300
B.RRWWN
CSOWN
100
CROWN
GUP-CROWN
BOOOS
SICCOS
NULUS
Cip-arabNeeds
Cli-and-onty
200
Clp Vnd
Cli-and-tertty mCcos
Clp-and-arrth BICCOS
Cup-ansiAreitt nip cats
Tiase Lesit (100)
Tines Lini. (102)
Clip-ndAAveit RICrDS
(500)
40
40
100
20
20
40
45
50
60
100
102
330
11.5
120
125
130
110
135
130
125
330
135
140
(d) cifarl O-resnet
(c) cifar100
(f) tinyimagenet
Figure 2: Representative benchmarks visualization. (a) and (b) are input BaB benchmarks with timeout 120s and 100s respectively, (c) and (d) represent medium-size ReLU nets, whereas (e) and (f) are substantially larger. These latter 4 benchmarks utilize ReLU splitting, for which we use complete clipping. Despite their differences in scale, our Clip-and- algorithm demonstrates strong performance on both. Please refer to appendix D.2 for detailed interpretation.
Modifications to the Standard Activation BaB Procedure. Our activation space BaB Algorithm shown in Appendix C.4] iteratively uses activation split constraints to optimize the intermediate bounds via Complete Clipping (Theorem B.I). This strategy fully exploits accumulated constraints through complete clipping on intermediate bounds directly, bypassing costly LP solves.
4 Experiments
We evaluate the effectiveness of Clip-and-Verre on several benchmarks from VNN-COMP 2021- 2024 6 49 10]. We first demonstrate its benefits on three benchmarks and three hard NN control system problems that are commonly solved with the input BaB procedure, then evaluate our approach on challenging activation space BaB benchmarks in VNN-COMPs, as well as SDP-FO benchmarks
8

---

Table 3: Comparison of different toolkits and Clip-and-Verte on VNN-COMP benchmarks with activation split BaB. Results of 3-CROWN and BICCOS were from the same hardware our experiments for direct comparison: other results are from VNN-COMP reports. indicates the benchmark was not supported.
ova122
cifari0 -rennet
cifar100- 2024
tinyimaoonet 2024
Method
time(s)
# verilied
limefs)
verified
time(s)
verilied
time(s)
verilied
nncnum
0
630.06
233.
24,74
OVAL"
20
393.14 14
11
Venus2
9
39
386.71
17
VeriNeti
32
83
73.65
17
8.11
48
MN-BaB
23
137.13
19
Marabouf
30
5.33
40.42
0
PyRATI
20
42.38
68
55.64
49
B-CROWN
77
29.39
9.17
119
8.65
BICCOS 76
79
31.72
25
16.73
63
8.75
121
9.73
138
Clip-and: Verify with 8-CROWN
28.15
22
6.06
63
6.59
126
9.48
140
Clip-and-Verify with BICCOS
46.48
11.81
8.17
131
10.48
Upper Bound
29
72
168
157
Results from VNN COMP 2021 report 6
from VNN COMP 2022 report
[49
from VNN COMP 2024 report [00
Table 4: Verified accuracy (Var.%), avg. per-example verification time (s) on VNN-COMP benchmarks and other commonly used benchmarks. The average time is calculated on verified images only. Clip-and- Cui-annd-Verify consistently outperforms all baselines when combined with state-of of-------thtttt BaB verifiers such BICCOS (79
Danaset
Model
J-CROWN
GCP-CROWN with MIP cuts Ver.%
BICCOS
Clip-and-Vert with 5 CROWN Ver.%
Clip-and-Vart Varify with MIP cuts Ver.
Clip-and-Virte Veriyy with BICCOS Ver.%
Upper
bound
0.3 and 2/255
Ver.%
Time (6)
Timets)
Ver.
Time(s)
Timets)
Timets)
Timets)
MNIST
CNN-A-Adv
4.28
6.64
76.0
6.91
73.5
76
6.39
76.5
Ads
50.0
4
46.5
1.25
2.64
48.5
1.55
46.5
0.62
48.5
2.06
48.5
1.31
49.5
CIFAR
CNN-A-Mix-l
CNN-A-Mix
42.0
$1.0
4.00
1.05
47.5
55.0
10:49
5.94
56.0
48.0
9.22
9.00
43.0
$1.0
4.34
0.84
47.5
55.0
10.53
4.44
56.5
48.0
5.12
7.45
53.0
57.5
CNN-B-Adv
47.0
8:25
49.5
12:16
51.0
10.79
49
7.54
$1.5
11.08
$1.5
7.68
06.0
B-dy-4
55,0
2.91
58.5
59.5
4,7
$6.5
60.0
6.67
60.5
5.55
63.5
claar0
16.71
oval22
66.66
83.33
63.53
31.72
73.33
28:15
45.52
90,00
difar 100-2024
59.5
8:15
60.5
8.75
63.0
6.59
65.5
8.17
$4.0
tiny 20yimngenet-22144
67.5
8.65
69.0
9.73
70.0
9.48
72,0
10.48
7X.5
Viiion--rnnffrmmn 2024
53
3930
2204
61.8
1081
10000
[66.. Fig. shows the overview of results of selected benchmarks. All results visualization and details about the configuration see Appendix D.I
introduced in previous studies [9.66)
Verification Results on Input Split Benchmarks and Hard NN Control Systems. For evaluation, we focus the following benchmarks from VNN-COMP 23 and VNN-COMP 24: acasxu, 1snc, and ny4sys. we have considered all input benchmarks and these three are the mostly challenging ones when solved using input BaB. We compare Overall, Clip-and- Verify reduces the number of branches by over 50% and accelerating the verification process. For 1snc, we reduced the number of domains by 96%. We further tested method on three challenging verification tasks from a recent study on provably stable neural network control systems [75] [1] 42]:
approach to other baseline tools shown in Table [
cartpole, Quadrotor-20 and require certifying Lyapunov-basee stability over high-volume state domains, and can not be solved by existing verifiers. The challenge of the verification problem that we need to verify inside the intersection of a large box and level set of its Lyapunov function. Detailed settings see Appendix D.T] These instances therefore test whether verifier can reason about Lyapunov decrease and boundary non-escape over large. physically meaningful state ranges, rather than over small ad adversarial balls. While general-purpose purpose robustness verifiers are not designed for such volumes, our method targets exactly this regime. As shown in Table 2 baseline methods without clipping fail to solve these problems within the time limit. Both relaxed and complete clipping enable verification, with complete clipping demonstrating superior performance by drastically reducing both the number of visited BaB subproblems and the total runtime, turning previously intractable problems into verifiable ones.
These tasks
Verification Results on General Activation Split Benchmarks Shown in Table B we further compare the proposed methods against a wide range of existing neural network verification toolk- its on six challenging VNN-COMP benchmarks: oval22, cifar10-resned tinyimagenet -002. and vit-2024 Each method is evaluated terms of average runtime (sec- onds) and the number of verified properties (# verified). A dash (-) denotes that the corresponding tool
cifar 10122000-2024

---

was not applicable or did not support that particular benchmark. Clip-and- Veriffy with BICCOS attains state-of-the-arr verification coverage on the evaluated VNN-COMP benchmarks, pushing closer to the theoretical upper bound in terms of the number of properties verified. When combined with BICCOS, whose tight bounding routines complement Clip-and-Veriine s efficient splitting, coverage reaches to 131 and 144, underscoring the method's s broad applicability and scalability. Besides of the ReLU nets, we further evaluated our method on a Vision Transformer (ViT) model [53], which contains non-ReLU layers such as Softmax. Verifying such architectures is challenging due to the complex, non-linear constraints introduced by these operators. The model tested has approximately 76k parameters and an input dimension of 3072. Tables 4 6 outperforms the baseline, verifying more properties in about half the time and with nearly 45% fewer subproblems in VIT. This demonstrates the applicability of our framework general networks.
sid--nn-Verrfyy show that Clip-and- Verify significantly
Ablation Studies. We compare the BaB baseline without clipping, Relaxed Clipping only, and the full pipeline (Relaxed + Complete) in Table [ and LP solvers in Section and scoring rule for choosing critical neurons (e.g.. BaBSR intercept, envelope gap, bound width) in Complete Clipping in Section D..] For each configuration we report time and visited subproblems under identical branching/timeon settings in Table 4 and Table 6 detailed breakdowns, per-model trends, and ablation protocols are in Appendix D.2
We further vary the comparison of complete clipping
5 Related Work
Verification becomes easier when we tighten the base relaxations that bound intermediate layers and contruct the inpul region, so that a subsequent branch-and-bound (BaB) search explores fewer and easier subproblems. BaB frameworks unify many complete verifiers and show that stronger node bounds reduce tree size [14, 13 55 64,
77 5). Subsequent improvements include faster dual/active-
set solvers and better branching 20 66 27). Our clipping steps make each node strictly easier (smaller box and tighter intermediate relaxations) without spawning additional subproblems, and are therefore complementary to any branching heuristic. Our method contracts the box domain using linear constraints and injects the same constraints to tighten intermediate affine bounds, thus improving the node-wise base problem before any additional branching is introduced.
For tighter base relaxations, linear-relaxatton--aasee bound propagation (e.g.. CROWN 7 and
DeepPoly (56)) provide fast base bounds. Beyond this, early single-neuron triangle relaxations such as PLANET [25) and the convex adversarial Salyytope/oon--Keee
line (69 underpin modern propa-
gation methods;
variants (DeepZ /A12 [29]/Nerrffy /OSIP
31I) further improve hidden-layer bounds in practice. Multi-ncuron relaxations overcome single- neuron limits by coupling activations [34]
48 57 Beyond K-ReLU and PRIMA [54 48) tightened
layer-wise convex relaxations [59] and barrier-oriented analyses (e.g., for simplex inputs or active-set scaling) show how to systematically overcome single-neuron limits. Beyond pure LP, SDP-based
Orthogonal to envelopes, NN-specific cutting planes have been injected directly into bound propagation e.g., general cutting planes (GCP-CROWN (76)) and conflict-driven cuts (BICCOS (79) to strengthen node-wise relaxations before or alongside BaB. Exact formulations (MIL P/SMT) and their strengthened variants remain an important baseline and hybrid component 660 2 35 36). though scalability constraints often shift emphasis toward stronger relaxations and BaB. Recent work also tightens bounds via optimization-driven bolling-horizon decomposition, effectively performing layerwise optimization- based bound tightening to improve intermediate bounds 78]. Our Complete Clipping is orthogonal: instead of inventing new global envelopes, we reuse existing linear constraints produced during framework. On
relaxations with linear cuts capture neuron coupling when affordable (8] 40 18]
verification to tighten per-neuron affine bounds inside the same hound-propagenn the other hand, Contract-Simple [7] contracts zonotope using one output inequality. We generalize this in a way tailored to bound propagation: Relaxed Clipping applies arbitrary linear constraints from final-layer bounds or activation branchings box proxy with closed-form updates, avoiding repeated I. solves while yielding globally useful domain reductions reused across all neurons.
6 Conclusion
We proposed Hhip-and-Verifyy a framework that enhances the Branch- and-Bound paradigm in neural network verification through our novel linear constraint-driven domain clipping algorithms. An efficient and light- paradigm for tightening intermediate-laye bounds has been remaining gap in neural network verification that has finally been addressed by our framework, Limitation and broader impacts discussed in Appendix E
10

---

Acknowledgements
Huan Zhang is supported in part by the A12050 program at Schmidt Sciences (A12050 Early Career Fellowship) and NSF (ISS-2331667.. Grani A. Hanasusanto is supported in part by NSF (CCF- 2343869 and ECCS-2404413), We thank the anonymous reviewers for their constructive feedback. In particular, we acknowledge Reviewer vsjp for their invaluable insights on the theoretical foundations of our work, particularly for identifying the connection between our dual optimization approach and the continuous knapsack problem.

---

References
[1] Matthias Althoff. An introduction to CORA 2015. Proc. the the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems, pages 120-151. EasyChair, 12shhir. December 2015.
[2] Ross Anderson, Jocy Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks. Mathematiiaa Programming, 183(1-2) 2020.
[3] David Applegate, Mateo Díaz, Oliver Hinder, Haihao Lu, Miles Lubin, Brendan O' O'Donoghue, and Warren Schudy. Practical large-scale linear programming using primal-dual hybrid gradient. Advances in Neural Information Processing Systems, 34:20243-20257, 2021.
[4] David Applegate, Mateo Díaz, Oliver Hinder, Haihao Lu, Miles Lubin, Brendan O O'Donoghue, and Warren Schudy. Pdlp: A practical first-order method for large-scale linear programming. arXiv preprint 2rX1::2501.07018, 2025.
[5] Stanley Bak. nnenum: Verification of relu neural networks with optimized abstraction refinement. In NASA Formal Methods Sympositm, pages 19-36. Springer, 2021.
[6] Stanley Bak, Changliu Liu, and Taylor Johnson. The second international verification of neural networks competition (vnn-comp 2021); Summary and results. arXiv preprint arXiv:2109.00499, 2021.
[7] Stanley Bak, Hoang- -ung Tran, Kerianne Hobbs, and Taylor T. Johnson. Improved geometric path enumeration for verifying relu neural networks. In Proceedings of the 32nd International Conference on Computer Aided Verification. Springer, 2020.
[8] Ben Batten, Panagiotis Kouvaros, Alessio Lomuscio, and Yang Zheng. Efficient neural network verification via layer-based semidefinite relaxations and linear cuts. In IJCAI, pages 2184-2190 2021.
[9] Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. Efficient verification of relu-based neural networks via dependency analysis. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 3291-3299 2020.
[10] Christopher Brix, Stanley Bak, Taylor T Johnson, and Haoze Wu. The fifth international verification of neural networks competition (ynn-comp 2024): Summary and results, arXiv preprint arXiv: 2024.
(11) Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T Johnson. The fourth international verification of neural networks competition (ynn-comp 2023): Summary and results. arXiv preprint arXiv:2312. /6760, 2023.
[12] Robin Brown. Edward Schmerling, Navid Azizan, and Marco Pavone. A unified view of sdp- based neural network verification through completely positive programming, 2022.
[13] Rudy Bunel, Jingyue Lu, I1ker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(42): 1-39, 2020.
[14] Rudy R Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan K Mudigonda. A unified view of piecewise linear neural network verification. Advances in Neural Information Processing Systems, 31, 2018.
[15] Nicholas Carlini, Guy Katz, Clark W. Barrett, and David L. Dill. Ground-truth adversarial examples. CoRR, abs/ 709. 10207, 2017.
[16] Shaoru Chen, Lekan Molu, and Mahyar Fazlyab. Verification-aided learning of neural network barrier functions with termination guarantees. arXiv preprint arXiv:2403.00 073000 2024.
[17] Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. CoRR, hwtp/10550004000 2017.
12

---

[18] Hong-Minng Chiu, Hao Chen, Huan Zhang, and Richard Zhang. Sdp-crown: Efficient bound propagation for neural network verification with tightness of semidefinite programming. In International Conference on Machine Learning (ICMI., 2025. ICML 2025.
[19] Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy R Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy S Liang, al. Enabling certification of verification-agnostie networks via memory-efficcien semidefinite programming. Advances in Neural Information Processing Systems (NeurIPS), 2020.
[20] Alessandro De Palma, Harkirat Singh Behl, Rudy Bunel, Philip H. S. Torr, and M. Pawan Kumar. Scaling the convex barrier with active sets. International Conference on Learning Representations (ICLR), 2021.
[21] Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip HS Torr, and M Pawan Kumar. Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104. 100.:60000...61 06718, 2021.
[22] Hai Duong, Linhan Li, Vu Nguyen, and Matthew Dwyer. A dpll (t) framework for verifying deep neural networks. arXiv preprint arXiv:2307. 10266 2023.
[23] Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium, 2018.
[24] Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. A dual approach to scalable verification of deep networks. Conference on Uncertainty in Artificial Intelligence (UAI), 2018.
[25] Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings 15, pages 269-286 Springer, 2017.
[26] Mahyar Fazlyab, Manfred Morari, and George Pappas. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Transactions Automatic Control, 2020.
[27] Claudio Ferrari, Mark Niklas Muller, Nikola Jovanovic, and Martin Vechev. Complete verifica- tion via multi-neuron relaxation guided branch-and-bound. arXiv preprint 20Xiv:2205.00263 2022.
[28] Matteo Fischetti and Jason Jo. Deep neural networks as 0-1 mixed integer linear programs: A 2017.
feasibility study. CORR,
[29] Timon Gehr, Matthew Mirman, Dana Drachsler- Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP). IEEE, 2018
[30] Julien Girard-Satabin, Michele Alberti, Francois Bobot, Zakaria Chihani, and Augustin Lemesle. Caisar: platform for characterizing artificial intelligence safety and robustness. arXiv preprint arXiv:2206. 03044, 2022.
[31] Vahid Hashemi, Panagiotis Kouvaros, and Alessio Lomuscio. Osip: Tightened bound propaga- tion for the verification of relu neural networks. In Software Engineering and Formal Methods: 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings. page 463 480, Berlin, Heidelberg, 2021. Springer- Verlag.
[32] Patrick Henriksen and Alessio Lomuscio. Efficient neural network verification via adaptive refinement and adversarial search. In ECA/ 2020, pages 2513-2520 IOS Press, 2020.
[33] Patrick Henriksen and Alessio Lomuscio. Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In Proceedings of the 30th international joint conference on artificial intelligence (IJCAI21), pages 2549-2555, 2021.
[34] IBM. Ibm ilog cplex optimizer, 2022.
13

---

[35] Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smm solver for verifying deep neural networks. In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part 30, pages 97-117. Springer, 2017.
[36] Guy Katz, Derek A Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, et al. The marabou framework for verification and analysis of deep neural networks. In International Conference on Computer Aided Verification (CAV), 2019.
[37] Hans Kellerer, Ulrich Pferschy, and David Pisinger. Knapsack Problems. Springer Berlin, Heidelberg, 2004.
[38] Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. International Conference on Learning Representations (ICLR), 2015.
[39] Panagiotis Kouvaros and Alessio Lomuscio. Towards scalable complete verification of relu neural networks via dependency- baased branching. In IJCAI, pages 2643-2650, 2021.
[40] Jianglin Lan, Yang Zheng, and Alessio Lomuscio. Tight neural network verification via semidefinite relaxations and linear reformulations. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 36, pages 7272-7280, 2022.
[41] Haoyu Li, Xiangru Zhong. Bin Hu, and Huan Zhang. Neural contraction metrics with for- mal guarantees for discrete-time nonlinear dynamical systems. 7th Annual Learning for Dynamics's & Control Conference, pages 1447-1459. PMLR, 2025.
[42] Haoyu Li, Xiangru Zhong, Bin Hu, and Huan Zhang. Two-stage learning of stabiliz- ing neural controllers via zubov sampling and iterative domain expansion. arXiv preprint arXiv:2506.01356, 2025.
[43] Alessio Lomuscio and Lalit Maganti. An approach to reachability analysis for bewd-fowward relu neural networks. CoRR, (bs//706.,,35,,, 2017.
[44] Ziye Ma and Somayeh Sojoudi. Strengthened sdp verification of neural network robustness via non-convex cuts. arXiv preprint arXiv:2010.08603, pages 715-727, 2020.
[45] David R. Morrison, Sheldon H. Jacobson, Jason J. Sauppe, and Edward C. Sewell. Branch-and bound algorithms: A survey of recent advances in searching, branching, and pruning. Discrete Optimization, 19:79-102, 2016.
[46] Christoph Müller, Francois Serre, Gagandeep Singh, Markus Püschel, and Martin Vechev. Scaling polyhedral neural network verification on gpus. Proceedings of Machine Learning and Systems, 3:733-746, 2021.
[47] Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Precise multi-neuron abstractions for neural network certification. arXiv preprint arXiv:2103.03368,, 2021.
[48] Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Prima: general and precise neural network certification via scalable convex hull approximations. Proceedings of the ACM on Programming Languages, 6(POPL):1-33, 2022.
[49] Mark Niklas Müller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The third international verification of neural networks competition (vnn-comp 2022): Summary and results, 2023.
[50] Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
[51] Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang A convex relaxation barrier to tight robustness verification neural networks. In Advances in Neural Information Processing Systems (NeurIPS), 2019.
14

---

[52] Karsten Scheibler, Leonore Winterer, Ralf Wimmer, and Bernd Becker. Towards verification of artificial neural networks. In MBMV, pages 30-40, 2015.
[53] Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana. Cho-Jui Hsieh, and Huan Zhang, Neural net- work verification with bou-- for general nonlinearities. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2025.
[54] Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems (NeurIPS), 2019.
[55] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems (NeurlPS), 2018.
[56] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL): 30, 2019.
[57] Harkirat Singh, M Pawan Kumar, Philip Torr, and Krishnamurthy Dj Dvijotham. Overcoming the convex barrier for simplex inputs. In Advances in Neural Information Processing Systems, 2021.
[58] Chuangchuang Sun, Dong-Ki Ki Kim, and Jonathan P How. Romax: Certifiably robust deep multiagent reinforcement learning via convex relaxation. In 2022 International Conference on Robotics and Automation (ICRA), pages 5503-5510, IEEE, 2022.
[59] Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. Advances in Neural Information Processing Systems (NeurIPS), 2020.
[60] Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv: 2017.
[61] Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019.
[62] Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T Johnson. Nnv: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In International Conference on Computer Aided Verification, pages 3-17. Springer, 2020.
[63] Andreas Venzke and Spyros Chatzivasileiadis. Verification of neural network behaviour: Formal guarantees for power system applications. IEEE Transactions on Smart Grid, 12(1)3383-397 2020.
[64] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
[65] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In USENIX Security Symposium, 2018.
[66] Shiqi Wang, Huan Zhang. Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 34:29909-29922 2021.
[67] Tsui- Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation certified robustness for relu networks. In International Conference on Machine Learning, pages 5273-5282, 2018.
15

---

[68] Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In ICML, 2018.
[69] Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning (ICML), 2018.
[70] Eric Wong, Tim Schneider, Joerg Schmitt, Frank R Schmidt, and J Zico Kolter. Neural network virtual sensors for fuel injection quantities with provable performance specifications. In 2020 IEEE Intelligent Vehicles Symposium (IV), pages 1753- 1758. IEEE, 2020.
[71] Haoze Wu, Omri Isac, Alcksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, et al. Marabou 2.0: a versatile formal analyzer of neural networks. In International Conference on Computer Aided Verification, pages Springer, 2024.
[72] Junlin Wu, Andrew Clark, Yiannis Kantaros, and Yevgeniy Vorobeychik. Neural Iyapunov control for discrete-time systems. Advances in Neural Information Processing Systems, 36:2939-
2955, 2023.
[73] Kai Yuanqing Xiao, Vincent Tjeng, Nur Muhammad (Mahi) Shafiullah, and Aleksander Madry. Training for faster adversarial robustness verification via inducing relu stability. CoRR, abs/1 0e//1809.00000 2018.
[74] Kaidi Xu, Huan Zhang, Shiqi Wang. Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. International Conference on Learning Representations (ICLR), 2021.
[75] Lujie Yang. Hongkai Dai, Zhouxing Shi, Cho-Jui Hsieh, Russ Tedrake, and Huan Zhang. I Lyapunov-stable neural control for state and output feedback: novel formulation. In Pro- ceedings of the 41st International Conference on Machine Learning, ICML'24. JMLR.org. 2024.
[76] Huan Zhang, Shiqi Wang. Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsich, and J Zico Kolter. General cutting planes for bound- propagation- based neural network verification. Ad- vances in Neural Information Processing Systems, 35:1656-1670, 2022.
[77] Huan Zhang, Tsui-Wei Weng, Pin-Yu Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neu- ral network robustness certification with general activation functions. Advances neural information processing systems, 31, 2018.
[78] Haoruo Zhao, Hassan Hijazi, Haydn Jones, Juston Moore, Mathieu Tanneau, and Pascal Van Hentenryck. Bound tightening using rolling- horizon decomposition for neural network verification. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 21 International Conference, CPAIOR 2024, Uppsala, Sweden, May 28-31, 2024, Proceedings, Purt I1, page 289-303, Berlin, Heidelberg, 2024. Springer-Verlag.
[79] Duo Zhou, Christopher Brix, Grani Hanasusanto, and Huan Zhang. Scalable neural network verification with branch-and annuh-and--ooud inferred cutting planes. Advances in Neural Information Processing Systems, 11.:2324--93533 2024.
16

---

Appendix
Contents
Formulations
17
A.1
Unstable Neurons and Complexity
17
A.2
MIP Formulation and LP & Planet Relaxation
18
A.3
Formulating Bounding Hyperplanes in Linear Bound Propagation
19
A.4
Verilication Properties Given as Boolean Logical Formulae
20
Proofs
21
B.1
Statement and proof of Lemma B.
21
B.2
Proof of Theorem 3.]
................................
B.3
Equivalence to the Continuous Knapsack Problem
23
Proof of Theorem 3.2
23
B.5
Proof of Order Dependency
25
Al
Algorithms
25
C.1
Overview
25
C.2
Sequential Clipping for Multiple Constraints]
26
Algorithms for Clip-and-Vers in Input Branch-and andhhhandd--aa uand-buund Scheme
27
C.4
Algorithms for Clip-and Verify in Activation franch-and--one Scheme
28
C.5
2D Toy Example
29
Experiments
33
D.1
Experiments Settings
33
D.2
Ablation Studies
34
D.3
Detailed Comparison with LP Solvers
35
D.4
Details of Heuristics
36
Limitation and Broader Impacts
38
A
Formulations
A.1 Unstable Neurons and Complexity
Unstable neurons for General Activations Let 2, be the pre-activation of neuron (i.j) in layer
number j with interval bounds (2] ;
=f") and let the component-wv wise activation be ((0) Given
sound linear relaxation (convex envelope) for the scalar graph of ci(0) over Lz (6) (0) denote by
( and u/ (8) (z) its lower and upper affine bounds, and define the envelope gap (or relaxation error):
8/0)
(2))
max 2E 20)
(8)
We call neuron (i.j) stable 859 = (the relaxation exact on the interval), and unstable
6(9) > This definition is oetivation-agnostie for piecewise- (PWL) activations, stability is cquivalent to [, x(() lying inside a single linear piece (c.g., for ReLU it reduces to z < or
2) 0); for smooth nonlinear activations one typically adopts a PWL relaxation, which case instability means the interval spans least segments (hence nonzero envelope gap).
Complexity. Let U be the number of unstable neurons at a BaB node. Once every unstable neuron has its activation region (piece) fixed, the network reduces to an affine map over the input box, and the remaining subproblem is convex. For PWL activations where each unstable neuron has at most
17

---

K' admissible pieces the number of global activation patterns is bounded by K Consequently. any exact verifier that distinguishes activation pieces (e.g.. MILP/SMT encodings with one discrete choice per unstable neuron, or BaB that branches on activation pieces) faces, in the worst case,
# subproblems E ((K and hence time hound K))
where Tound the per-node cost to evaluate/tighten bounds. particular, for ReLU networks K 2. yielding the familiar exponential scaling S2(24); ); thus any mechanism that reduces U (e.g.. by stabilizing neurons via tighter pre-activation intervals) produces a multiplicative reduction in worst-case search, by factor of K when U decreases by AU.
A.2 MIP Formulation and LP& & Planet Relaxation
Early approaches pursue exact guarantees for verification through Mixed-Integer Linear Programming (MILP)
17 43 23
28
61
73 and Satisfiability Modulo Theories (SMT) [52] 35 15 25
The MIP Formulation The mixed integer programming (MIP) formulation is the root of many NN verification algorithms. Given the RELU activation function's 's piecewise linearity, the model requires binary encoding variables, or ReLU indicators 8 only for unstable neurons. We formulate the optimization problem aiming to minimize the function f(x), subject to a set of constraints that encapsulate the DNN's architecture and the perturbation limits around given input as follows:
f min fxx x,2
s.t. f(x) = 2,4,,,00 = x
(9a)
20 2
b(:; iE [4]
(9b)
I+( (j 11:1000)
(9c)
I- (j:u) <0)
(9d)
70 = -0:0
(9c)
I --
(9f)
(9g)
8) 2 je
(9h)
30
(91)
80
3 S3 (0 --
[L
(9j)
( =
(9k)
20 =
(91)
8 = 0:j 1 ( ie 1]
99m)
To initialize intermediate bounds for each neuron, we replace the original objective f(x) with the neuron's pre-activation value 2/ This lets us solve the following bounds for every neuron j in layer i, with i [L 1] and j E J(0:
g min 1/ (x),
u (
max (() x
(x).
Here, the set (1) comprises all neurons in layer i, which can be categorized into three groups: "active" (I+))), 'inactive" (I)())), and 'unstable' (Z(0).
Next, the MIP formulation initialized with the constraints
For ReLU, K = 2 (inactive/active). For HardTanh or ReLU6. K & 3. For smooth activations under an S-segment relaxation, take K = S.
18

---

Both of across all neurons and layers i. These bounds can be computed recursively, propagating from the first layer up to the i-th layer. However, since MIP problems involve integer variables, they are generally NP-hard, reflecting the computational challenge of this approach.
The LP and Planet relaxation. By relaxing the binary variables in 9k to
10.1..j I i
[T. 1], can get the I.P relaxation formulation. By replacing the constraints in 9i). (9j..
(9
with
30
(5) 10
-
19);; j -
(10)
3
we can eliminate the d variables and get the well-known Planet relaxation formulation 25 these two relaxations are solvable in polynomial time to yield lower bounds.
A.3 Formulating Bounding Hyperplanes in Linear Bound Propagation
In feedforward network, A (1) ,,A" (+)) and (+)) must be derived for every linear layer preceding an activation layer, well as the final layer of the network. In order to derive the hyperplane coefficients
(A A and biases (c!*) (c())/(()) ). at this 8t layer, all preceding activation layers must have already had their inputs bounded. The following lemma describes how ReLU activation layer may be relaxed which will be useful for defining bounding hyperplanes, A A cl and c(
Lemma A.1. (Relaxation of a ReLU layer in CROWN), Given the lower and upper bounds of z
denoted as 1 1(11)) and u; (1-1), respectively, the linear layer proceeding the ReLU activation layer may be nower-bounder element-wise by the following inequality:
(5) w (2 W ( (i-11) ((g
(II)
where ((6-1) diagonal matrix with shape IR. P. xn.-1 whose off-diagonal entries are 0, and on-diagonal entries are defined as:
1,
(i-1) 2 0
(1-1) 00
0
(1-1)
(1-1)
( < 0 < u
(1-1)
and w(()
(12)
(i-1) < 0 u
(-1)) and w 0
and by (1-1)
is vector with shape Th m4-1 whose elements are defined as:
0,
1(1-1) > 0 u
S 1)
7 i- <0 u and w (1) 2 0
(1-1)
0,
(13)
1) < u (1-1) and w (i) < 0
In the above definitions, o (i-1) 1) is a parameter in range [0, 1] and may be fixed or optimized as in (74).
Proof. For the jth ReLUU at the (i 1)th layer, it's result may be bounded as follows:
(i-1) aft 2/ 1i-1) S sz(z)i-1) s u (i-1) (ii (2) (i-1)
-1 1/-11))
(14)
The right-hand side holds as this is the Planet-relaxation defined by equation 10 For the left-hand side, we first consider when 2, (f-1) < 0. For every input in this range, the result of the ReLU
is o(z(1-1) O. ()-1)) 2))) forms line for which inputs in this range will always produce
19

---

non-positive result when o (i-1) E [o, 1]. For inputs in the range 2j is o02)) 2 2 This result is never exceeded by aj (i-1), (i-1)
(f-1)
2 0. the result of the ReLU
when aj (i-1) E [0, 1].
3j
When the result, )()) is multiplied by a scalar such as w/ valid lower-bound of (z)
( requires a lower bound on a(2) ((z))²)) when w 0, and an upper bound on (i(1))) ") when w < O. Such lower and upper bounds are indeed produced by D ((-1) and b ((-1))
oz whose definitions are derived from the inequality displayed in equation (14). This concludes the proof.
já
L
Lemma A.1 suggests recursive approach to bounding neural network as the bounds the 2th layer depends on the bounds of the layer preceding it due to the dependence on 15 and u ((-1) This is indeed the case, and we may define our hyperplane coefficients as (t) (2 w where
(w
D ()-1, i
(15)
I
i i
To collect the remaining terms, we set g = Σx (2 W (8) ((-1)
+ (2)68)))) To
obtain an upper bound, Lemma A.1 and its proof may be adjusted accordingly where appearances of the inequalities ( 2 O and W < 0 are flipped. In doing so, we may repeat this recursive
process in order to obtain A (i) and c())_
Though we have described how a ReLU feedforward network may be bounded, appropriately updating the definitions of (()) and (0) allows feedforward networks with general activation functions (that act stement-wisel to be bounded. Such a general formulation is described in (77) that is similar to the template described above, and goes into further detail how this formulation may be extended to quadratic bound propagation.
A.4 Verification Properties Given as Boolean Logical Formulae
((x) 2 0, Va E X
(16)
Equation (16) referred the canonical formulation [4 13) as it general enough encompass any property involving boolean logical formulas over linear inequalities. To make this idea clear, consider a neural network whose output dimension is n2 3. We may wish verify that the output corresponding to the true label, yo. is always greater than all other outputs, y1 and y2, for every input in X. Explicitly, we want to verify:
yo 91) (go 32), Vo X.
(17)
To represent this formula, we may first introduce a new linear layer whose weight matrix is defined as C, sometimes referred to specification matrix:
0
C
(18)
-1
This specification matrix allows the output neurons to be compared against one another. Applying this matrix to the output vector of the network, denoted as y :- (yo, y1, y/2 results the following new output:
yo y1 y/2
Cy.
(19)
Next, we append a MinPool layer to the network which returns the minimum of these two results. Now, we may define new neural network, (xx which appends the aforementioned MinPool and linear layer to (x), resulting in the final output, min (yo - y1, Yo y2). should now be apparent that if the property described by equation (17) can be verified as true, then the following must hold:
20

---

min (x) 0. øEX
(20)
We may now proceed to produce a lower bound, (x)) and only until [((x) > O, can we formally state that the network will correctly classify all inputs in X. In the scenario that instead want to verify the property (yo > yn V Yo > y2) for all inputs in X, we may simply redefine f'(x) by replacing the MinPool layer with MaxPool layer which would return max (3o 31. 3/ y2
Finally, suppose we want to verify that the output corresponding to the true label is greater than all other outputs with some additional margin such that (y/o y/1 + A 3/u 1/2 + m.) Ve X where m > 0 (i.e. the network should always classify the first label with additional relative confidence defined by m). Then the only modification is also incorporate bias vector, : [-m, -m] the final linear layer where C' was defined. This bias vector is sometimes referred to as the threshold. This results in the final output, [= min y1 m, yo 1/2 m). Hence, equation (16) is general enough to encompass more complex queries.
B Proofs
B.1
Statement and proof of Lemma B.1
We first introduce a preparatory result that establishes closed-form solution for a linear optimization problem over a hyper-rectangulat feasible set.
Lemma B.1 (Dual Norm Concretization for for all i [n]. and define the hyper-rectangular domain:
Domains), Let c E R" with c; > 0
X' fa R. 2
E E
x -
For any vector v E RR,, the following hold:
v
x + 1 Te,,,
v x a 1 T
min
=Ex
where |v| E R4 denotes the component-wise absolute value of v.
Proof. We begin by rewriting the feasible set {ar RM
S x + = ( + e x x ERR, | S 11}
where denotes the Hadamard (component-wise) product. Then, the maximization problem becomes v ② (voc)
vt x max |0
xEX
v a
Σ
- = T l
where the final equality follows from the definition of the dual norm of the oo-nomm. The derivation for the minimization problem follows analogously by replacing the maximization with a minimization, which flips the sign of [v] Thus, the claim follows.
B.2 Proof of Theorem 3.1
Proof. The problem 2 is a linear program over a compact convex set with an additional linear constraint. Let feasible set F = (ær E X g + h < 0} be the feasible set for (2)
Case F = 0, then by definition, L* = +oo. In this case, it implies that for all x E X. T x+ >
Case 2: F is non-empty. Since X' is compact and F is a closed non-empty subset of X (as it's the intersection of with a closed half-space), continuous. Therefore, L* is finite and attained. We introduce the Lagrangian for problem (2) by partially dualizing the constraint g x + h S
also compact. The objective function x + cis
L(x, 3) (a + cc) + 3(g + h) for x X, 3320 0.
21

---

The primal problem can be written as:
L min sup L(x, (e,00) (3)
æEx $20
To swap the min and sup, we can apply Sion's Minimax Theorem. Let K X' (a compact convex set in IR") and M {3 R 3 0} (a closed convex set in RR. The function ((x, () has the following properties: 1) For any fixed thus convex and continuous on K. 2) For any fixed æ E K, L(x, 3) = (g + 1).8 + (a x + c) is linear in 3, and thus concave and continuous on M. Since these conditions are met, Sion't 's Minimax Theorem states:
M, ((x, 3) (a + Bg)
(c+ 3h) is linear in ax and
min sup L(x, 3) sup min C(x, B)) #ek BEM
BE M øER
Therefore,
L = sup min L(x, (3) 820 #EA
Since F is non-empty. L" is finite, implying that the supremum is attained (or is the limit if approached at infinity, but D(3) is continuous), so we can write max instead of sup. Let d(3) = millaex C(x,B). B).
d(3)
=EX min (a T x + c 3g Tg x + Bh)
min ((a + Bg) x) c Bh =EX
The inner minimization is optimizing a linear function (a (g)) To over the hyper-rectangle X. Using Lemma B.1 (with v = a Ag):
min =eX
((a + (g) = (a [g) T - - a $gl
where a + Agl == ビØ= lag + 3gyley. Substituting this into the expression for d(3), we get:
d( = (a + (g)) TT: - -1 3gl E c 3h
This is exactly the dual objective function D(3) defined the theorem statement 3 Thus, we have established that L max320 DB3). Then we analyze the properties of the dual objective D(3):
Concavity: The dual function d(33) is always concave, as it is the pointwise minimum of family of functions that are affine in 3 (indexed by x E X).
2. Piecewise-Linearit:: The term -la /g1" - la; &ggle; involves the absolute value function. Each term -la la, + ,g is concave and piecewise- (a point where the slope changes) at 3 linear in B. Since ((3) is sum of concave niecewise-linear functions and linear functions, it is itself concave and piecewise-linear. The breakpoints of D(3) are the collection of all values 3 -aj/g 2 0 where 9j O.
with breakpoint aj/g; (if g; + 0). The other terms in D are
Thus, we need to maximize the concave, biecewise-linear function D(3) over the interval [0, oo). Since D(3) is concave, its maximum over convex occurs either point where the super- gradient contains zero, or potentially at the boundary point 3 = O. Because D(3) is piecewise- linear, its super-gradient @D) is constant within the linear segments between breakpoints. At breakpoint Sg. the super-gradient is an interval [@D(3 DD (B }} (the range between the left and right derivatives). The maximum occurs at a point 3 such that E @D(33)) This 3 must be either of the breakpoints BR. >> where the
= (if the derivative is non-posinn non-positive for 3 > 0) derivative changes sign from positive to non-positive (i.e., E [aD (3+t)) )] ). or the function increases indefinitely (which corresponds an infeasible or unbounded primal, but we assumed feasibility and the primal is bounded over the compact X, so L is finite, thus the dual maximum is
finite).
Therefore, the maximum L* can found non-iteratively by:
1. Identifying all non-negative breakpoints 8r = -a,/9; 2 0.
22

---

2. Sorting these unique breakpoints 0 = Bu < 31 < 8p.
3. Evaluating the derivative (slope) of ((3) within each segment (Bkr 9k+1) and potentially at
4. Finding the point 3 (either 0 or some 3%) where the slope transitions from non-ne non-negative to non-positive. The value ((3*) is the maximum L*
This process involves finite number of analytical calculations (evaluating slopes and function values at breakpoints) rather than iterative optimization, justifying the claim efficiency.
B.3 Equivalence to the Continuous Knapsack Problem
The primal problem in 2 mathematically equivalent to the continuous (or fractional) knapsack problem. We can demonstrate this equivalence through a change of variables. Let & be the lower bound and 21 + be the upper bound. We transform æ E [rg, Fi to y [0, 1]" using:
T2 20.5
Fi.
(#: -e,)) es)
y1
I3 = Io.s + 26,yi
11. 20,i
2c;
Substituting this into the primal problem min {a x + c g + S 0} gives:
min ve
a (Io + 2(c ④ v)) +c s.t. g0 + 2(c O v) < 0
min vc v.)).
(2c a) y (a xo +c) s.t. (2e y (g xp h)
r = -2e @ a, 2e o g. and t = - (0 E) + h). The problem becomes the standard
knapsack form:
rTy s.t. sTus
max yE|o,1
This problem, even with negative coefficients, be solved with greedy algorithm 37 The efficiency ratios rj/8j used for sorting in the greedy algorithm are:
26,a,
aa//9;
8
2r,9;
These ratios identical the breakpoints in dual objective function D(3). This confirms line-by-line correspondence: our dual optimization algorithm, which sorts breakpoints to find where the super-gradient contains is algorithmically equivalent to the greedy knapsack algorithm, which sorts by efficiency ratios. Both have the same Onn log n) time complexity.
B.4 Proof of Theorem 3.2
Direct Intuitive Proof more direct and intuitive proof for Theorem 3.2 exists. We wish to
solve T (new) = max a TTx + S 0}. Since only x; is in the objective, we can set all other variables 2, (for j # i) to values within their box domain [ Ej. +e,] that make the constraint T c < loose as possible, thereby maximizing the "budget" for T;.
To loosen the constraint, we must minimize the term Ejtr ayæ.. This achieved by setting each to its extreme:
If aj > set Ty its lower bound, Ij = à, - Ej. aj set Ty its upper bound, I,- 4 + Ej.
This worst-case minimum for the can be written compactly as Eju(a - layle;). We substitute this minimum sum back into the constraint:
Σ (afēz layle, +c50
0,44
23

---

Assuming > 0, we can solve for 2; to find its new upper bound:
IJ Eins azãz + Ej lagly -
aj
This value is 24 (clip) value and the original upper bound T;- The case for ag < 0 (updating the lower bound 2,) follows analogously. A detailed proof is shown below:
(new) is the minimum of this
defined in Theorem 3.2 The final bound x;
Proof. We consider the upper bound; the lower bound can be derived analogously. First, rewrite the input region as
X { E R"
S ボ = fx E R" a -6 E S x S á + 6),
Suppose the linear inequality constraint is given by a Tx + b S 0, where a E Rº and b E IR. We note that the intersection X n fo E R" : a T x + b S 0} is nonempty and only if
where é
and E 2
2
0 min T x + b -abb--aa a Σ asle:
=EX
by Lemma B.I Henceforth, we will assume this inequality is satisfied.
We now compute
[new) I,
ma a + b s 0}
max min e, a - 1(a x +
#EX AER
min max e, T A(a x + b)
AER_ sEX
min e, à X(a a + le; Aa c, AER_
where third line follows from Sion's minimax theorem since X is compact set, and the final line follows from Lemma B
Rearranging the term yields
(new) min e, d + X XER
Σ 5slas| -aaa"a TT b + + - -aal- #
(21)
We now analyze three cases for a, and derive closed-form expression for the scalar minimization.
Recall that we have assumed 0 2 a + Ei= 0;6; or equivalently Σ E, s,la,l -e; las. We have:
1. a; > 0: The function 6 Aa, attains its minimum at À = a right and -ca; the left. Thus:
0, with slope 6,a, the
If Ejサi 5 a a bl S. e;a; then the minimum of 21 is attained X and
:; Ejer slal a x Ej ررررر| - Ejær agiz b
x (new)
0;
a;
If 1f //t 5lazl - a aT - b> e;;; then X* = 0 and
(new)
f; + 6; TT.
2. < 0: In this case, the minimizing X = 1 < 0 is infeasible to 21 Hence, A = 0 and (new)
7. F..
24

---

3. = 0: Here, the objective function in 21 becomes affine in X. Since Efet Eslayl a i b 2 O, we again have X 0 and
new) Ft.
In summary, if a| T x
0 then 0 = Xn x E R :a c 0): otherwise,
E ses sslas1
sss ajtj -
(new)
min
Ttd
az > 0 af S 0.
T
Tz
This completes the proof.
B.5 Proof of Order Dependency
Here we briefly introduce Theorem B.2 to demonstrate why sequential processing the constraints for clipping achieving better results.
Theorem B.2 (Order Dependency of Constraint Intersection). Let X = fr E R" 21, S TV) + cj S 0} denote the feasible for the j-th constraint.
be a box domain, and let Fj = {ir E X a x
Define the full feasible set as F = 1 Pj.
Let {I....,m, m) + {1.....m} be a permatation (i.e., reordering) of the constraints. For sequential intersection, define:
p(k) M Fa(t)) k= 1.....,, m,
with F(0) X.
(Order-Independent Bounds): The variable-wise bounds satisfy:
min max and min I; 2 max min Zi. 3 =Ef;
FEF
J zEF,
These bounds are independent of if computed via F クー= FJ-
Refinement): constraints intersected sequentially (i.e., F(k) depends on T), then there exist permutations π1 + T2 such that:
F(m) m
+ p(m)
Proof. Order-Independent Bounds. Same Corollary B.2 The inequalities follow from F Fg for all j. Simultaneous intersection satisfies:
max 24 min max I3 and WEF,
min x; max min Fi: #EF
FEF
3 #EF,
as the intersection F cannot exceed the tightest bound from any Fj-
Order-Dependee Refinement. Let F(k) = n (a(()- For dependent constraints (e.g., Fi bounds 31, F2 depends 21), the sequence fkk) depends A counterexample with Fi :. 22 and F2 21
x2 S shows:
1. Intersecting Fj first gives æ1 < 2 -22, then F2 further tightens 21 S
2. Intersecting F2 first gives æ1 I r2, then Fi tightens rı S 1.
The final bounds differ: x1 < min(2 I2, x2) vs. < 1.
C
Algorithms
C.1 Overview
Fig. shows the pipeline of our algorithm.
25

---

CROWN Bounding Complete Clipping
Bound domainn in parallol
1
Linear
For activation layer and for each domain D
Batch of domains:
For each domain D
= (
1.) Determine critical neurons, C(8)
g(L) = min A c(2))
2.)
Compute 2)
Vj [n:]
Prune and Add Remove verified domains (in green) add back the domain list.
Relaxed (Input) Clipping
Branching
For every subdomain, constraints to clip the input space
Split activation
Input space
{x 10
(2
Update
X
X1
Split
Unaltered Method
X2
X
Added Method
Update Zig
Modifed Method
Figure Full Clip-and- Verify pipeline for (Input and Activation Activation) BaB integration.
(x)
f(x)
(relaxed)
clip
f(x) = +
f(x) T +
2
(klow)
Figure 4: Simple ID visualization of relaxed clipping reducing the input interval, potentially enabling second pass of bound propagation produce tighter bound.
C.2 Sequential Clipping for Multiple Constraints
When several linear constraints are present, we apply Theorem 3.2
sequentially to each row of Ax + c O. @nooiith3Jouthing this procedure: First, for each constraint k. compute & and from the current bounds, æ and žE Then, use Theorem 3.2 to refine æ, and æ; for all i. Finally, proceed the constraint, using the newly clipped bounds the domain. Note that if a. occurs in any dimension, the input region this subproblem infeasible, and we can directly verify this subproblem without performing further verification.
Because the bounds are updated after each constraint, the final domain an over-approximation of the true feasible region under all constraints simultaneously. However, it is still far more efficient than solving a multi-constraint system in one shot, making it well suited for large-scale verification where repeatedly clip domains across many subproblems.
By clipping the domain repeatedly, Algorithm 3 retains enough precision to prune large regions yet remains computationally lightweight enough for repeated invocation on many subdomains during verification. may even be the case that the constraints passed to our domain clipping algorithm reveal the region entirely infeasible. Such scenario may occur when two Activation assignments
26

---

Algorithm 3 Linear Constraint-Driven Relaxed Clipping (sequential)
Require: T: Lower bounds; æ Upper bounds; A Constraint matrix; e Constraint vector. 1: (owss(A), n cols(AA)
2: for for each constraint & E {1.....m) do
3: for each input dimension i (I....,7) n do
4: f-
2
5:
if Ak, F 0 then
6:
(new)
-ize Ae, + -B
Ae,'
7:
if A then
8:
T
(new
f- min Di 2, (now)
9:
else
10:
(new)
max (new)
11:
f- max [ 2 (mew))
12:
0; <- min(2n (2;; .. (
Ensure: Clipped œ2 x:
admit an infeasible domain, or when the desired property admits multiple constraints that produce infeasibility. such scenarios, Algorithm will return clipped bounds where æ will be smaller than E along some dimension(s). In the context of branch-and-boune bound, this subdomain may be effectively pruned, avoiding the process of running bound propagation once more on the domain, avoiding unnecessary computations
C.3 Algorithms for Clip-and-Verite in Input Branch-and-bound Scheme
Algorithm 4 Clip-and- Verify for Input -anuch-and-bound
Require: model to verify; n batch size; timeout time-out threshold
1: Dunknowu: f < [nit(f. 0) (Initialize the set of unknown subdomains D Unknown and global
bound f)
2: while [D (uuknnwn!|
>> 0 and not timed out do St 1 < Batch __cck_iick___ Out (Pnnoonno n) (Pick up to n subdomains X; and
3: A
poos 1 BLOy
their associated hyperplanes (A!thy prey from the previous iteration.)
4: {c.);= & Top-K Heuristic( ((&,, A. A cre in Ii=1) (Determine critical neurons C2 using
top-k heuristic over each domain and its previous hyperplanes.)
5: (fx;; Ax, .x...... Lx, Ax, Cx.)) + Solve Baaldd (f. (&, (Compute bounds
and plane coefficients each subdomain; Refine critical neurons using planes constraints and Complete Clipping.}
6: (2, xxt,, A,, S. } +- Batch_ (( A (. (Split each subdomain; share hyper-
planes with both children.)
7: (x)-), a 1 < Relaxed cliiperr__errrrreeeeee (X, Xx+ A, c.
(Refine input box each
child subdomain using the plane coefficients.)
8: (XT,2t)
- + Momain_Updaatee (( (, 00 pmm
(+) (t)
(Update each child subdomain's 's in-
put bounds.)
9: Dunknown Dunknown Doamain_Filtce (LLx,
Pf (Filter out veri-
fied/infeasible subdomains. Retain unknowns and their bounding hyper-planes.)
Ensure: UNSAT if (Dunknowal 0 else Unknown
Algorithm describes our modifications to standard BaB procedure. When all subproblems can be verified, then the verification problem is referred to as UNSAT (i.e., the complementary property, Ba X, (a)) < 0, unsatisfiable). and the network is safe from counter-examples. Otherwise, insufficient to determine if the property is UNSAT without further refinement or falsification.
27

---

C.4 Algorithms for Soo--an--Verff in Activation Branch-and-boum Scheme
Algorithm 5 Clip-and-Verity for Activation Branch-and-boul
Require: f: model to verify; n batch size; timeout: time-out threshoid
Dunknown: f Init[f, 0) {Initialize the set of unknown subdomains Unknown and global
bound f}
2: (A(), cli), A () c( unstable neuron(idx)
Get Constraints(f) [Retrieve the set of coefficients and biases for each unstable neurons' upper and lower bound and get the indices of unstable neurons during Bound Propagation.)
3: Dornann_llipper <- Inii_ ( (9) _c A (1) e iir,iix (/x1)))/z1) (Initialize the Domain Clipper with the set constraints information.]
4: while 'Dunknown| > 0 and not timed out do
5:
{2,)²=1 + Batch Pick Out Out(PUnknoww: r2) (Pick at most n subdomains from the unknown sct.)
6: 1,, ,/ + Batch Batch_SSlit
(Split each subdomain (e.g., Activation split or imput split) into two child subdomains.)
7: (cf-), ,e Di=1= t-
(ouuristio((2:]])) (Determine critical neurons using a top-k heuristic (e.g. BaBSR) over each domain.)
8: {xf interm bds(") xx(+) iinterm bds, 1
}
j=1 + Domain Clipiin___ippreeelee ((2, , ,,,,c/=' (.fT..((t)p )/=1)
c(
(Apply Relaxed Clipping to child subdomain s input and Complete Clipping on the critical neurons. Constraints are the Activation splits.)
9: 12, 22,2,,2 } + Domain_
interm_bdse bds, (-)
x inntenm_mbbl (ds(+t))s)))))) )m
(+)
(Update each child subdomain's input and intermediate bounds.)
(L.,...., L2t) Solve_Bound (f, {x,, interm interm_bounds;, bounds; z (Compute bounds on
10:
each newly clipped subdomain using a bound propagation solver.)
11:
Unkkown +- Dukknwwn
Comain__Filten [Le; .......) (Filter out verified/infeasible
subdomains. Keep remaining unknown subdomains in D Unkknown-)
Ensure: UNSAT if Uuuknowal 0 else Unknown
Algorithm begins by initializing the verification procedure. First, we call Init () to obtain an empty set of partial Activation assignments (or subdomains) along with an initial global lower bound for the property to be checked. This global lower bound can, for example, be the result of a quick bounding pass. The set DUnknown is then populated with a single "root" subdomain representing the entire input domain.
Next, we retrieve the constraint information for all neurons (Line 2). Specifically, Get_Constraints(f returns the linear coefficients and biases used to bound each neuron's 's acti-
vation, distinguishing between the lower-bounding (A)), c(u)) and upper-bounding (A (i) el
linear functions. It also identifies indices of "unstable" Activation neurons whose ranges straddle zero. These constraints will later be used to restrict the feasible input region using both our Relaxed Clipping and Complete Clipping algorithms.
We then initialize the Domain Clipper (Line 3) with the gathered linear constraints. This Clipper component will be invoked whenever branch Activation neuron, so that the corresponding
partial assignment (c.g., x 2 0) is "pushed back" onto the input domain. In doing so, we clip the subdomain's 's input box by applying Theorem 3.2 (or its extensions) to incorporate these newly introduced constraints, thus discarding parts of the input space that violate them. In addition, when given set of critical neurons, these Activation split constraints will be used to directly refine the intermediate neurons using Theorem 3.1
The main loop (Lines 5-11) iterates until either no subdomains remain unknown or time-out is reached. In each iteration, we pick up to unknown subdomains from DUnknown (Line 5) for batched parallel processing. Each subdomain 2, is then split (Line 6) along one or more unstable Activation neurons, creating child subdomains in which each split neuron is fixed to either the active (2 0) or inactive (5 0) regime.
28

---

At Line 7, we invoke top-k heuristic (e.g. BaBSR) in order to determine the set of "critical neurons" that would contribute the most to providing stronger convex relaxation if their bounds were be refined.
At Lines 8-9, invoke the Domain Clipper these newly formed child subdomains. The Clipper translates each Activation assignment into a linear constraint on the input, then refines (or "clips") the child subdomain's 's imput bounds, and the bounds of the "critical neurons" in each subdomain with respect to the heuristic choices from the step prior. This ensures that any portion of the parent domain that contradicts the new constraint removed. Once clipped, the child subdomains' intermediate bounds are also updated (Line 10) so that subsequent bounding calculations reflect the tighter input ranges.
We then compute bounds on the newly clipped subdomains (11) using a chosen method-often a fast hound-propagationn tool such CROWN or lightweight LP solver. This step yields lower bounds Lzz on the network outputs for each subdomain. If these bounds confirm that the property holds (e.g., robustness margin remains non-negative), the subdomain is verified and can be pruned. If the subdomain is infeasible (e.g., constraints are contradictory), it is also removed. All remaining subdomains (still "unknown") return to Unkknown for further splitting.
Finally, the loop terminates once there are no unknown subdomains left or the time-out is reached. If DUnknown becomes empty, we conclude UNSAT, signifying that no violating input (counterexample) exists within any subdomain. Otherwise, we return "Unknown," indicating that verification was not completed in time.
Overall, this procedure reflects a standard Activation BaB flow, except that an additional "domain clipping" step (Lines 8-9) is inserted after each split, leveraging partial Activation assignments to refine the input domain and select intermediate neurons before the next bounding pass. By applying our linear constraint-driven clipping algorithms whenever new constraints appear, gain significantly tighter intermediate-layee bounds and thus reduce the branching burden throughout the verification process.
C.5
2D Toy Example
To illustrate our clipping verification approach, we consider a simple two-layer ReLU feed-forward network defined as
f(x) (2) a ( x + b()), (2)T
(22)
where (²)), 6()) R.? (1)) E 2 and a(.) denotes the element- ReLU activation. We aim to verify the property
f(x) 2 0, Va E X.
The input domain X' is defined as an -bx centered = [0.5, 0.5] with half-widths e [1.5, 1.5) T_ Equivalently, the domain be expressed using its endpoints [-1, - and
[2, _J. The network parameters specified
11 1
[ -7 b - [ [
[
(
(2)
(23)
CROWN Bound. As a warm up. let's bound the network using the CROWN algorithm without utilizing relaxed nor complete clipping. We begin by computing the pre-activation bounds of the intermediate layer which are obtained by concretizing the first layer's 's affine transformation:
min ( =EX
x + 00,
max (1)) =
x + ()
(24a)
z =
W (1) c
W
| c (
= w (1) é + (1)
E + ((1)
(24b)
Substituting the parameters into equation 24b yields 2 = [-2,-13] and - T2 These neurons are then passed to a ReLU activation Tunction, and one should notice that for each input, we have that 2 unstable, meaning that we cannot bound the non-linearity exactly, however, we can still get sound linear bounds on the output of the ReLU activation. Using Lemma A.I. we construct the diagonal matrices and corresponding vectors,
1 and Σ₂ < 0 < Σz. In this scenario, we have that the ReLU neurons are
On
0
D
(25a)
0
0.2
0
29

---

31
0
11
Z1-21
(25b)
22
D and b are used to create lower bounding planes on the output of the ReLU activation where on and 02 are real numbers limited to the range [o, 1]. These values may be optimized, however will always fix a1 0: 1 when lower bounding unstable neurons in this toy example. D and d are
upper bounding planes on the output of the Rel.U activation, and its construction is derived from the Planet relaxation [2 It may be verified that for inputs in the range 2/.
Dz + b 2 (z)) 2 Dz +
(26)
We next lower bound the network output. Because the post-activation vector (z) is passed through the final linear layer, a coordinate- wise sign on the final-layer weights determines whether to use upper or lower affine bounds for each neuron. Concretely,
(w 2 w + (z));; ; 2 w (D.,iz+bi,)
if 2 0 w < 0
(27)
so that the final-layer lower bound with respect to x is
w (2)T oxz) 2 (w(2)++) DD + b) + (2) (2), ((2=
(D
(28)
where ((2)+ zeros out entries which are negative and (2), zeros out entries which are positive. In
our example, these vectors are (2)))+ = [1. 0] and w = [0, -T]_ The final step is to produce a lower bounding hyperplane of the final layer with respect to the network's input. So far, we've only
related this lower bound to the intermediate input, z. Our final step is quite simple as we know that
( + (()) Using this relation, we can "back-propagade our affine relaxations to the input as follows.
(w)))+) DD +b (20()))))(D
(Dx b)
(29a)
= (w)() D W - b()) + b) + (w) D (w x + +b(1) + 5)
(29b)
= =(((w(()t) D (2) D w x (ww D + (2) ((1)
+ +ww( 1 (2)
(29c)
Let us introduce the following variables,
a ((m()))+) D (wn(2)-)) D) w())
(30)
c = (ww()) D + (w) D) 6() + (2)++ + (w (2)- )b
By construction, we have that the output of the network is lower bounded by the following linear relaxation,
f()) 2 a x + c.
T
x Z...
(31)
Using Hölder's inequality, we can solve for the minima of this lower bounding plane,
19
min ((x 2 min a x + g- a a aa T xEX
(32)
øEx
6
As this lower bound is too loose, we cannot verify our desired property. f(x) 2 0, Vo e X.
Relaxed Clipping, We first tackle this example using our efficient yet approximate clipping algorithm termed relaxed clipping. Given set of constraints, the objective of relaxed clipping is to compute the smallest input box representation that satisfies those constraints. This step is performed once per round of branch-and-boule concretization step. Consequently, this refinement has the potential to tighten bounds across multiple neurons, including those in the final layer.
and the resulting refined input box is shared by all neurons during the
Consider a propaddrppaattinnbaaeeeee verifier executing branch-and-bowe by splitting over the activation space. For the remainder of this subsection, focus on the case where the first ReLU
30

---

neuron is split into its non-positive (inactive) region, i.e., 21 S 0. This split decision can be reinterpreted as a linear constraint on the imput,
Te 0.
(33)
Since the input is two do-dimensional, our goal is tighten the lower and upper bounds of each input dimension under this constraint. Formally, we solve the following optimization problems:
(rc) min s.L.
(WI.)) + bb S 0,
(34a)
(nc)
max æ1
(W(.) (2) b1y < 0,
(34b)
#EA
222
(ne)
min D2 xEX
s.t.
(W(() T x + b()) < 0, s.t. ( x x + (()) < O.
(34c)
22
(ne)
max
22 =EX
(34d)
From Theorem 3.2 one potential solution along each dimension is given by
W 53
I (1)
(clip)
(35)
w 1.8
Each dimension is then updated follows:
(re)
(clip)
if W (1) 1,1
T
min
0
a
max
a
(clip)
L.
if W 1,2 <0
(36)
no change
otherwise
For the first dimension (i = 1), since ( > 0, the upper limit may be refined if x < T1
1.1
For the second dimension (i = 2), where (!)) < 0, the lower limit may be refined if æ Substituting the given parameters yields:
(clip)
1.2
22.
( 1.2 22 + ( 1.2 - (
+ -
(alip)
(37a)
w!ll)
(dip)
w
(1) 21 + (W
1,1 61 60)
(1)
-1)(1/2)+ -
5 7
22
(37b)
-7
1,2
is indeed the case that (clip)
1 and (clip) > Z. so the limits of the refined input domain are
az
now,
a (re) = [-1,5/7]
( [1, T
(38)
The new box representation may also be characterized by its center and half-widths:
* (I( + xz (r2)
c (re) (m(re) (r0))/2
(39)
yielding the refined input domain
x (re)
{(2 [|
201100 <((r))
m (re) < x((c)
(40)
We proceed to bound the network using the CROWN algorithm under (re) in place of the original domain,
X. Substituting this domain into Eq. (24) produces z! -(re) 1 -13] and
x(re) = [2, -5/22/11 Both neurons exhibit tighter bounds, and notably, z(re) < 0. which ensures that the input to the second ReLU neuron is strictly non-poss non-positive across (re). Since the ReLU function is piecewise linear, this implies exact post-activation bound:
((x) (x)) (2)) 0, Yz E (re).
(41)
One interesting observation to point out is that with this clipped domain, 2 (rc) improves dramatically from the original upper bound, 22. However, because constraint originated
31

---

from 21 S O. the true maximum is in fact zero. In this case, one could enforce this upper bound to be zero, but keep in mind that relaxed clipping algorithm is designed for generality, thus constraints may arise from split decisions at any neuron in the network where forcing x(re) = 0 would not be valid. This example illustrates that relaxed clipping, while lightweight and compatible with CROWN, remains an approximation and may yield suboptimal yet informative bounds. Rather than enforcing
the true maximum, retain the relaxed clipping result, z(-e) = 2.
Applying Lemma A.1 we derive the linear post-activation bounds with respect to the pre-activation inputs:
(re)
Q11
0
(re))
0
(42a)
0
0
(re)
(ro)
0
b (re)
- 2 (re)
(mc)
D
(42b)
For simplicity, let 1. Notice that for the second neuron, we have that,
(D!r.)) +
b (re) az)) = (D (me) T + b2 (rc) = O, VE2 E [2] (rc) )
(43)
confirming that this ReLU neuron is inactive and its output can be exactly bounded as zero
Finally, performing the same backpropagation procedure as before yields
min f(x) min a (re)T x + c(re) = (ne) ( - la (re) e(re) + c(re) = 22
(44)
x
This represents an improvement over the previous bound, although the property remains unverified.
Complete Clipping. Relaxed clipping can be viewed an indirect approach towards refining the bounds of the neural network as a smaller input representation can potentially yield improvement in the concretization step when forming the neurons' bounds. Complete clipping on the other hand is a direct approach towards refining the bounds on the network as the optimization objective specifically targets the neuron's 's bounds rather than the shared input representation.
In practice, relaxed clipping is extremely lightweight, and its operations are well-suited for GPUs. Thus, it is often sensible to combine relaxed and complete clipping in the verification pipeline. In this example, however, we aim to clearly distinguish the two methods. Therefore, we use the original input domain, X, rather than the refined one, ((rr), and retain the ReLU split constraint x1 I O.
Complete clipping operates directly on the bounds of each neuron, refining them via constrained optimization. The first step is to bound the preactivation bounds which may be formulated as:
(ec) min ( xEA
+ (1)
(cc) max W (1)
#EA
S.L.
x
+ b1
0 0
(45a)
s.t.
T x
b (1)
00
(45b)
For this two-dimensional problem, this amounts to targeting the lower and upper bound of both neurons at the intermediate layer, resulting in a total of four constrained optimization subproblems. However, we will only focus on refining the upper bounds as we will soon see that this will be sufficient for verifying our desired property in this toy example.
As discussed earlier, the split constraint on the first neuron implies that its true upper bound is trivially 3 = O. With single constraint, Theorem 3.1 guarantees optimality, i.c., x((r) क 0, which can be verified using Algorithm M For single constraint, complete clipping attains the exact optimal solution through enumeration, without relying on projected gradient methods or LP solvers, no longer serving an approximation such as the case with relaxed clipping. Even when multiple constraints are present (where optimality is not guaranteed), this targeted refinement remains powerful mechanism for improving intermediate-layee bounds.
AAlgorithm i performs coordinate ascent the dual objective when the primal is minimization problem. Since (456) is a maximization problem. we can negate the primal objective to minimize it, then negate the resulting solution. Furthermore, the algorithm assumes constraints of the form Gx + h < O. For constraints of the opposite form, Ga + h 2 O, one may simply negate them. Hence, the algorithm is used without loss of generality.
32

---

Next, we consider the upper bound 2 we derive analytically via Algorithm According to Theorem 3.1, the dual form of this problem and its solution is given by
(ec) Complete clipping yields the optimal solution zg. which
(W!!) BW T
-²= min SER+
W 2.
3w (1) 1.
6, + +62 - 1b6(
(46)
j=1
The dual objective is minimized with respect to the Lagrange multiplier, 3 E R+.. One possible solution occurs B = -, but since relaxed clipping already improved this bound, we expect that 3* #0. 0.
Before solving for 3*, it helpful examine the structure of the dual objective D(3). Because the primal objective maximizes z2, minimizing the dual objective is equivalent. The function ( is convex and piece-wise linear, so we analyze its sub-gradient, & D(3):
2B
1. D(B)),
a + Ej= sign (W - -WW1)) (- W (1)
1.j 13)
bl
B q
(47)
8 03
A DY D(
3 E q
where q the vector of breakpoints ((W,) (3 //2///WW// = 1/7]. defined on the intervals / E (o,,,117)) (1/7,5). and (5, oc). Because D is convex, its sub- gradient is negative on the leftmost interval and positive the rightmost one. The optimal 8 occurs at the break-point where the sub- oob-gradient changes sign from negative to positive, i.e., the break-point whose sub-gradient interval contains zero. The sub- uub-gradients in each region are:
Thus, the gradient uniquely
w la |w
(1)
(w(!) 1,
a 60)h -42 ,B
E2
W [ +
|
(
T
a - bl =-1
< <<< <
(48)
1.2
62
T
HW [
[WQ]
62
(w!!.) a (
3B5.
Note that when transitioning from the case where 8 E (- 1/7) to 3 5), the term W lez switches sign while (Iw((3)
1,1 C1 remains negative. This ordering follows because in break-point point vector, we have that 92 < q1, and this ensures the sub- gradient is correctly calculated in each sub-interval, providing intuition the sign change occurs at B = 5, giving the minimum of the dual objective at 3 and the solution
to why argsort(q) is necessary in Algorithm I For this example,
<(c)) 23 = L -3
After performing complete clipping at the intermediate layer, we discover that the optimal upper bounds under our split constraint are given as z" [0, -3] There is clearly an inter-neuron depen- dency between the two ReLU neurons such that forcing the first neuron to be in-active subsequently causes the the second neuron to also become in-active. Consequently, the post-activation neurons can be exactly bounded using the CROWN algorithm, and in particular, o O for all E [z* 2*). Since the last layer contains no bias vector, is not necessary to perform complete clipping again, and we have finally verified our desired property for this subproblem.
min f()) = (2)T (2) 2 0, xE
subject to 2 S 0.
(49)
D Experiments
D.I Experiments Settings
To allow for comparability of results, all tools for input BaB were evaluated on equal-cost hardware with 32-vcore CPU, one NVIDIA RTX 4090 GPU with 24 GB memory, and 256 GB CPU memory. For ReLU based BaB experiment, we use cluster with one AMD EPYC 9534 64-core CPU and the GPU is one NVIDIA RTX 5090 GPU with 32 GB memory and 512 GB CPU memory. Our implementation is based on the open-source a, g.B-CROWN verifier with Clip-and- Verrify related
33

---

code added. For input bab, three different set-ups of Clip-and- -er-ff are tested: Relaxed, Relaxed + Reorder, and Complete. Here Relaxed. Reorder and Complete refers to the methodology discussed
in 3.2 and 3.3, All experiments use 32 CPU cores and GPU. The MIP cuts are acquired by the cplex 34 solver (version 22.1.0.0). We use the Adam optimizer [38 to solve both ax f. μ.. T. For the SDP-FO benchmarks, we optimize those parameters for 20 iterations with a learning rate of 0.1 for a and 0.02 for 3. μu, T. We decay the learning rates with a factor of 0.98 per iteration. The timeout is 200s per instance. For the VNN-COMP benchmarks, we use the same configuration as a.3-CROWN used in the respective competition and the same timeouts. For NN control systems, task details in [42] Appendix CJ. For the Lyapunov function level set, we verify on V(x) [0.2, 0.20001] for CartPole and Quadrotor- -oooor--10 -DD, and on V(x) E [2.0, 2.1] for Quadrotor- 2D LeDD-arge-Roe ROA. Let Qanal denote the resulting (expanded) box used for training/evaluation once the generator stabilizes. Concretely (all "+'-'" are per-coordinate half-widths), for CartPole, Riimal = + +4.8, 3.6, 13.2, 13.2].
For Quadrotor-201 Rimal + [12, 13.2, 12, 19.2, 20.4, 88.8).
D.2 Ablation Studies
We conduct a detailed ablation study on multiple adversarially-trainn models spanning MNIST, CIFAR, and larger VNN-COMP benchmarks to evaluate Clip-and- Verify and its variants against three baselines: 8-CROWN, GCP-CROWN, and BICCOS. Tables hand[lhhhhhh three key metries: verified accuracy (Ver. %), average per-example verification time (Time), and average per-verified- example domain visited V.). Domain visited V.) is a metric specific to branch-and-bound (BaB) methods, indicating how many subproblems (domains) are explored to fully verify instance. Crucially, a higher D. count may reflect verifying more difficult instances or a larger overall coverage, rather than inefficiency in the verification process. We also provide Figures 5 and that visualize these metrics across all benchmarks.
Overall Verified Accuracy and Time From Table 4 Clip-and- variants nearly always achieve higher verified accuracy than the baselines. For instance, on CNN-B-Adv (CIFAR). Clip- with BICCOS reaches 51.5% verified accuracy- surpassing the 47. 47.0% (8-CROWN), 49.5% (GCP-CROWN with MIP cuts), and 51.0% (BICCOS alone) of the baselines. On cifar 10- resnet, Clip-and- Verify (with MIP cuts or with BICCOS) achieves up to 88. 88.89 verified accuracy (outperforming the 83.33% 87.5% range from baselines). In terms of verification time on this benchmark, Clip-and-Verify with 3-CROWN the fastest overall (6. (6.06s), and Clip-and- with BICCOS (11 1808)) remains competitive with standalone BICCOS (16. 73s) and GCP-CROWN (17.99s). When scaling to deeper networks such as sifar100-209 and tinyimagenet-200 2024, Clip-and- Veriffy with BICCOS maintains the leading verified accuracy (65.5% and 72.0%, respectively) while sustaining moderate average verification times (c.g., 8.17s for cifar 100-2024 and 10.48s for tinyimagenet-20244 underscoring its suitability for larger-scale verification tasks.
Domain Visited (D.V. ys. Difficulty In Table we further examine the average domain visited (D.V.) across verified examples. While Clip-and- Verify variants may sometimes visit more domains (e.g., on oval22, Clip-and siii-and-Verify with MIP cuts visits 18891.25 domains compared to 16614.72 for with MIP cuts), this often correlates with achieving higher verified accuracy (90.00% vs 83.33% in this case). This suggests that the method is effectively exploring the space to verify more challenging instances or a broader set of inputs, leading For example, on CNN-A-Ady (CIFAR), Clip-and- Verify with MIP cuts visits 3704.86 domains on average and attains 48.5% verified accuracy. While its D. V. is slightly higher than standalone BICCOS (3622.71 D.V. for 48.5 555%% accuracy), it's notably lower than 3-CROWN (12621.33 D. for 45.5% accuracy) and GCP-CROWN with MIP cuts (8186.1 11 D.V. for 48.5% accuracy). while achieving comparable or better accuracy. In other scenarios (c.g., CNN-A-Ady-4 on CIFAR), Clip-and- Clip-and-Verify with BICCOS achieves 48.5% accuracy with a D.V. of only 843.47. This is the same or higher accuracy with a significantly smaller D.V. compared to standalone 3-CROWN (46.5%, 2066.39 D. GCP-CROWN with MIP cuts (48.5% 3907.30 D. V.), and BICCOS (48.5% 1319.56 D.V.) This illustrates that when Clip-and- Verify effectively prunes the search space, verification efficiency can improve even while tackling similarly challenging problems and achieving high accuracy.
net increase in verified accuracy.
A Breakdown Comparison between Verifiers Table 5 eexhibits the instance-wise comparison on acasxu benchmark, as also illustrated in Figure 2a Most of the instances in acasxu benchmark are easy to verify. On these instances, all the verifiers share similar verification time and D.V. Instances
34

---

Table 5: Instance- wise breakdown comparison acasxu benchmark between o, B B-CROWN and Clip-and-Veriee
Avg. on simpler instances
65
73
Method
Time
D.V.
Time
D.V.
Time
D.V.
a, R.B-CCOWN
1.0287
12615.35
timeout
19.1899
5474527
relaxed
1.0087
6759.11
9.1839
1876495
2.7422
291855
relaxed + reorder
1.0283
6467.96
7.6514
1416479
2.6385
229755
complete
1.0991
6350.11
6.8963
531381
3.5677
112431
Table 6: Ablation Studies on Verified accuracy Var%%) avg. per-verificd-exampll domain visited number (D. analysis for all method verified instances on different Clip-and- Verify components,
Datazet
Model
CROWN
GCP CROWN
BICCOS
Clip and Verify with (-CROWN
Clip and Veniy
Clip and Verify
Upper
with MIP cuts
with MIP cuts
with BICCOS
bound
and - 2/255
Ver:5
D.V.
Ver.5
D.W.
Ver.5
D.V.
Ver.5
D.V.
Ver:5
D.V.
Ver.#
D.V.
bound
MNIST
CNN-A-Ads
71.81
2712.72
71.5
4447.54
76.0
3051.50
74.0
2395.966
73.5
1495.07
76.0
2656.99
76.5
CNN-A-Ad
45.5
176211 38
48.5
618h 11
48.5
36:2.71
45.5
1037 1n
48.5
48.3
1073.56
5015
CNN-A-Adh-
46.5
2056. 99
48.5
5007 5g
48.5
1310.55
46.5
708.80
48.5
2306 36
48.5
843.47
49.5
CIFAR
CNN A Mix
M-i---Mix-4
$1.0
42.0
6108.57
482.43
55.0
47.5
17609.35 84
8922.50
48.0
56.0
2015.12
3319.90
51.0
43.0
4462.48
150.06
47.5
55.0
9836.06
4301.32
48.0
56.5
3501.06
4189.92
57.5
$3.0
CNN-B-Ad
47.0
7255. 68
49.5
9546.32
51.00
5758.00
49
4951.07
51.5
69775.27
51.5
2677. 94
65.0
CNN-B B-A-B
55.0
1776.66
58.5
4688 22
59.5
2711.15
56.5
649.92
50.0
3565.74
68.5
1055,30
63.5
Gifar Ii-ronel
83.31
2100 76
87.5
7091 30
67.5
5428 893
36.11
47%.0
KR.W9
2545.25
88.39
3641.15
ovai22
66.66
30549 95
$3.33
16614.72
83.35
12730.05
73.33
20191.23
90.00
18801.25
90.80
14052.81
96.67
c:aa 100-2004 2024
59.5
1535 60
60.5
768 17
63.0
152.96
65.5
122.00
84.0
tinyimapme--- 2014
67.5
830.92
66.0
497.52
70.0
188.02
72.0
118.34
78.5
73 and 65 stand out as they're re significantly harder to verify. For instance 73, clipping is able to cut down over 94% D. and over 80% verification time. While a, 3-CROWN is unable to verify instance 65 within given timeout, Clip-and- Verify is able to verify it within 10 seconds. Cactus plots Figures 5 and are also able to give a mnstance-wise comparison. Please see the following paragraph for more detailed explanation.
Interpretation of the Cactus Plot Figures 5 and 6 illustrate the number of instances verified as runtime varies. Each line represents a method, with the x-axis showing the cumulative verified instances under given timeout (y-axis). This style, used in VNN-COMP reports captures the trade- off between subproblem difficulty and runtime performance. The curve's right end indicates total solved instances-furtie
right means more instances verified within the timeout. A flat initial curve fragment reflects many easy instances solved quickly. curve below and to the right of another shows consistently faster solving. The x-axis ordering reflects instance difficulty, from easy (left) to hard (right). For example, on the tinyimagenet benchmark (Figure 5d), 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.
Overall, these results show that Clip-and- Clip-and-Verify's framework of enhanced linear bounding and "clipping" robustly scales across varying network depths and adversarial training schemes. The additional integration of MIP cuts or BICCOS bounding routines consistently pushes verified accuracy closer to each benchmark's upper bound while balancing verification time and domain exploration. We plot and analyze these ablation studies across all benchmarks in Appendix D.2, confirming that our method not only raises coverage (Ver. %) but also leverages clipping and cutting plane methods to verify some of the hardest instances encountered.
D.3 Detailed Comparison with LP Solvers
To validate our claim that coordinate ascent is more efficient than LP solvers for our task, we integrated I.P solvers directly into our BaB algorithm to solve the clipping optimization problem. We compared our method ("Clip (ours)") against the Gurobi solver using dual simplex with varying
35

---

iteration limits. The experiment was run on the acasxu benchmark instance 65, and we report the average time and bound error over 30 million LP calls during the entire BaB process. We report only Gurobi's optimize( () time, ignoring all Python overhead for problem creation, giving an advantage to the I.P solver.
As shown in Table 7 our method is 740x faster than l-iteration LP heuristic and 880x faster than 10-iteration LP, while achieving comparable accuracy (0.00085 vs. 0.0007 mean error). The LP solver only achieves near-zero eπror with 10+ iterations, at which point it is intractably slow. The high fixed cost of LP solvers (even for iteration) comes from presolve and initial basis factorization routines, which are far more expensive than our simple O(n log n) sort.
Table 7: Comparison of our coordinate ascent ("Clip") vs. Gurobi dual simplex with iteration limits on acasxu (instance 65). Time and error are averaged over 30M calls.
Method
Avg. Time per Call avg. Bounds Error std. Bounds Error
Limsplxeex (1 iter)
2.08s
0.401
1.45
Limsixp (10 iter)
2.47s
0,0007
0.0018
LP-simplex (20 iter)
2.49s
0.0
0.0
Clip (ours)
0.0028s
0.00085
0.0019
L.-full (ground truth)
2.50s
0.0
0.0
We also investigated modern GPU-based LP solvers, specifically Google's PDLP B which uses a Primal-Dual Hybrid Gradient (PDHG) algorithm. As shown in Table 8 while PDLP achieves high accuracy when it converges, it is not suitable for our use case. PDHG does not maintain a feasible solution during iterations. Under strict iteration limits, it has very high failure rate, returning a NOT HOT_SOLVED status and thus failing to provide a valid dual bound for our sound verification procedure. contrast, dual simplex (Gurobi) and our method always return valid, feasible bound. PDLP is designed for single, massive LPs, whereas our framework requires solving millions of independent, small LPs parallel, setting where our specialized GPU solver excels.
Table Comparison with Google's PDLP. Our method is dramatically faster and, critically, always returns a valid bound, unlike PDLP which frequently fails under iteration limits. B.E. means Bound Error.
Method
Avg. Time per Call
avg. B.E
std. B.E
Failure Rate (%)
PDLP (1 iter)
2.23s
2e-8
4e-8
81.31%
PDLP (10 iter)
4.21s
1.4e-8
2.3e-8
48.26%
PDLP (20 iter)
6.02s
5.5e-8
1e-8
38.38%
Clip (ours)
0.0028s
0.00085
0.0019
0.0%
Gurobi-full
2.50s
0.0
0.0
0.0%
D.4 Details of Heuristics
Neuron Selection Heuristic. The performance of Complete Clipping can be sensitive to the choice of which intermediate neurons refine. To guide this selection, we employ a heuristic based on the Branch-and- Bound for Split Recommendation (BaBSR) score, originally designed to select which neuron branch on during BaB [13. Specifically, we use the intercept score from BaBSR, which estimates the potential impact of refining a neuron's 's bounds on the final output relaxation. The score for neuron & calculated as:
Score; max(0, (0, -4+) max(0, up).
max -mean
uk 1
where 4 and ug are the neuron's 's pre-activation lower and upper bounds, and mean relates to the intercept of the neuron's linear lower bound. A higher score indicates a looser relaxation and greater potential for improvement. For each layer, we compute this score for all unstable neurons and select the top-k neurons for refinement with Complete Clipping.
36

---

To validate this choice, we conducted an ablation study on the tinyimagenet-202 and cifar100-2024 benchmarks, comparing BaBSR against three alternative heuristics: random se- lection, prioritizing neurons with the largest bound gap (U I.), and prioritizing neurons with the largest bound product (-U x L). As shown Tables 9 and 10, the BaBSR heuristic consistently achieves the best verification time and explores the fewest subdomains, especially for the balanced top-20 setting. This confirms that BaBSR makes more effective choices, leading to earlier pruning and more efficient search.
Table 9: Average verification time (s) per instance for different top-k heuristics.
Benchmark
Top-k Setting
Random
-U x
U-L
BaBSR
Top-10 per layer
16.3
16.5
16.8
16.2
tinyimagenet
Top-20 per layer
18.1
17.9
17.2
15.1
All neurons
22.4
22.4
22.3
22.7
Top-10 per layer
26.2
26.6
27.0
26.1
cifar100
Top-20 per layer
29.1
28.8
27.7
24.3
All neurons
36.5
36.4
36.4
36.5
Table 10: Average number of visited domains instance for different top-k heuristics.
Benchmark
Top-k Setting
Random
x
U-L
BaBSR
Top-10 per layer
485
453
420
388
tinyimagenet
Top-20 per layer
381
370
365
342
All neurons
278
278
278
278
Top- 10 per layer
907
847
785
726
cifar100
Top-20 per layer
712
692
682
640
All neurons
521
521
521
521
Table 11: Ablation Study on Top-k Neuron Selection on
Top-k
Verified
Avg. # Domain Visited
Avg. Time (s)
0 (reduce to 3-CROWN)
84
6108.57
4.20
20
86
4462.47
4.24
50
86
4372.79
4.83
(1 timeout)
1881.77
8.23
Table I1 shows the ablation study on the top-k neuron selection heuristic on cifar_ cnn__ a_mix benchmark, reveals that strategically prioritizing neurons based on their FSB intercept scores sig- nificantly enhances verification efficiency. Employing a moderate & (specifically top-k 20 and 50) leads to the best outcomes, successfully verifying more properties (86) while substantially reducing both the number of domains visited (by up to 28% compared to heuristic) and the overall time (by up to 19%). In contrast, not using the heuristic (top-k 0) results in less efficient search, while applying it to all unstable neurons (top-k "all") drastically cuts down visited domains but incurs prohibitive time cost and a timeout, indicating that the overhead of processing too many prioritized neurons outweighs the benefits of more targeted branching. This demonstrates crucial trade-off, with intermediate values striking an optimal balance between guided search and computational overhead.
Constraint Importance Heuristic The constraint importance heuristic is to sort the constraints for better performance. The constraints corresponding to hyperplanes closer to the center of the current input domain might be more immediately relevant or impactful for tightening the bounds or for cutting off significant portion of the current feasible region X'.
First, for the current input box domain X, determine its centroid á. We can calculate g T + h En lgsle; > 0 (there is no X' satisfy the constraint in (2) to check the infcasibility and
37

---

Table 12: Ablation Study on Top-k Neuron Selection on 1snc
Ratio of selected neurons Total time (s)
Domains visited
0/6
13.37
18,073,174
1/6
11.25
7,254,214
2/6
10.54
4,914,243
3/6
9.70
3,072,863
4/6
9.23
2,088, 1988
5/6
8.69
1,739,412
6/6
7.66
871,14
g lg S 0 (for all x X' satisfy the constraint in ②2 to remove redundancy.
Second, for each available linear constraint g² h 0, calculate the geometric distance from the centroid & to this hyperplane:
g Tn h
|
Then, sort the constraints in ascending order based on these calculated distances to prioritize con- straints that are closer the centroid. In methods like Algorithm] (Compleet Clipping), processing more impactful constraints earlier might lead to faster convergence or more significant bound im- provements in the coordinate ascent. Such important metrie could also be relevant to Algorithm (Relaxed Clipping).
We tested the bound tightness improvement from the heuristic acasxu instance 65. Clip-and- Verify improves the intermediate bounds for 470,772,542 times during input BaB, and 3.962% of them can be further tightened with constraint importance heuristic. For all these further improved bounds, we computed the empirical quantiles of the relative improvements, shown in Table D.4
Percentile problems
Max
0.1th
5th
10th
25th
50th
90th
Bound Improvement
4242.6%
270.79%
3.07%
0.64%
0.29%
0.10%
0.03%
0.01%
0.002%
These results reveal that the head the distribution contains substantial refinements, with the maximum observed improvement reaching up 4000%. This indicates that the heuristic produce tightened bounds, potentially leading to earlier branch pruning or faster convergence.
E Limitation and Broader Impacts
Limitation. Our framework's effectiveness is influenced by the trade-off between the precision of clipping and its computational overhead. While Complete Clipping utilizes GPU acceleration, its scalability can be impacted when networks have very large hidden layers combined with high number of unstable neurons and sparse constraints. The memory complexity scales as O(B x N x M.) where B is the number of BaB subproblems, N is the number of neurons in the largest layer, and M the number of linear constraints. To mitigate this, our top-k neuron selection heuristic (Appendix D.3) strategically prioritizes the most critical neurons, balancing precision and cost.
Conversely, while Relaxed Clipping is highly efficient with a complexity of O(n) per input di- mension, its effectiveness diminish in very high-dimensional input spaces due to the curse of dimensionality, where axis-aligned relaxations may become looser.
However, the ultimate scalability of our method is not fundamentally limited by input dimensionality or layer width, but rather by the intrinsic difficulty of the verification query, which is an NP. hard problem. As demonstrated by our experiments small networks with low-dimensional inputs can pose immense verification challenges. Clip-and- Verify proved essential in solving these hard instances. 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.
neural network control systems 2 even
38

---

300
700
FCROWN
P-CROWN
GCP COP-CROWN cuts
600
GCI-CROWN + mip cuts
BICCOS
BICCOS
200
Saip-and-Verity
Clip-and-Verity
Clip-and-Neree mip
400
Clip Seip-aud-errily- mip cuts
150
Hlip-and-Verily BICCOS
Clip and San-Vrrify BICCOS
Time Limit (300)
Time Linit (720)
100
200
100
40
45
50
55
60
0
10
15
20
25
Namber of Instances Verified
Namber Instances Verified
(a) cifarl0-resnet
(b) oval22
B-CROWN
100
B-CROWN
BICCOS
BICCOS
Clip-and-Verift
Clip-and-Verity
Clppaad-Verilyy BICCOS
Clip-and-eeityy BICCOS
Time
Time Limit (100)
Time Limit (100)
40
20
100
105
115
120
125
130
110
115
120
125
130
135
140
Number of Instances Verified
Verified
(c) cifar100
(d) cinyimagenet
Figure 5: Plots for hard instances need to be solved by BaB in VNN-COMP benchmarks. It is important to note that in large-scale models with numerous properties to verify, the cutting plane method often incurs significant overhead. This is because batches, whereas the cutting plane method handles each property individually. Consequently, when addressing datasets like CIFAR- 100 (99 properties) and TinylmageNe (199 properties), integrating with BICCOS introduces additional overhead.
current approach processes all properties
Broader Impacts Neural network verification is crucial for ensuring the safety and reliability of Al systems in critical applications such as autonomous vehicles, medical diagnosis, and financial trading. By significantly accelerating the verification process through efficient domain reduction, our work makes formal verification more practical for larger and more complex neural networks. This advancement enables broader adoption of verification techniques in real-world applications, potentially preventing catastrophic failures and building trust in Al systems. Clip-and- Verify's integration with existing frameworks ensures immediate applicability, allowing organizations to implement stronger safety guarantees without substantial overhead. While this work strengthens the safety of AI systems, it important to note that verification tools should be part an approach to AI safety, including robust testing interpretabiliity and ethical guidelines.
39

---

BCCOWNN
B-COWNN
GCP-CROWN cuts
GCP.CROWN mip cuts
150
BICGOS
150
BICGOS
Clip- and Verity
Cliip and Vertty
Timt
Clip-and-Verifyy mip
Clip Slip-and-Veriily mip
100
Clip-and-Verite BICCOS
100
Clip anp-aan-Woel Veri-f BICCOS
Time Limit (200)
Time Limit (200)
50
50
70
75
80
85
90
95
80
82
84
86
88
90
92
94
96
Namber of Instances Verified
Namber Instances Verified
(a) cifar__cpprr enn adv
(b) cifar enn a_adv4
200
I-CROWN
200
B-CROWN
GCE-CROWN cuts
GCP-CROWN mip cuts
BICCOS
150
BIACOS
Clip-and-Verity
Clip-and-Verity
Time
Clip-and-Vesse mip cuts
Clp-and-Verity
100
Clip-and Veriff BICCOS
100
Clip-and.Verify- BICCOS
Time Linit
Time Limit (200)
50
60
65
70
75
80
85
90
95
0
110.0 112.5
Number
Verified
Number Verified
(c) cifar enn mix
(d) cifar enn mix4
200
200
B-CROWN
B-CROWN
GCP-CROWN mip BICCOS
GCP-CROWN mip BICCOS
150
150
Clip-and-Verityy
Clip-and-Verity
Time
Clip-and Veiiifyd-eriily mip cuts
Clip and Deriifyd-eerify- mip cuts
Aip-aand-eriify BICCOS
Clip-and-Verifyy + BICCOS
Time Limit (200)
Thme Limit (200)
90 Number of Instances Verified
90 95
100
Number Instances Verified
(e) cifar can adv
(l) cifar can b. adv4
B-CROWN
GCP-CROWN mip cuts BICCOS
150
Clip-and-Verity
Time
Clip-atu-Verilly mip
100
Clip and Vertiy BICCOS
Time Limit (200)
50
110
120
130
140
150
Number of lastances Verified
(g) mmist_cnn_a__t_etm
Figure 6: Plots for hard instances need to be solved by BaB in SDP henchmarks.
40

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: Our claims match theoretical and empirical results. We present results across several benchmarks to demonstrate that they can generalize to other settings.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification:
Limitations have been explicitly discussed in Appendix B
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
the paper. The authors should use their best
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
41

---

Justification:
Theoretical results have been proven.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated referenced in the statement of any theorems.
The proof' can either appear the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should properly referenced.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
Justification: Algorithms have been clearly described with technical details discussed. Parameters for experiments have been included in the appendix. The code will be open- sourced.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, it may be necessary either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, or other means that appropriate to the research performed.
While NeurlPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) the contribution is primarily a new algorithm, the paper should make clear how reproduce that algorithm. (b) If the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
42

---

Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
Justification:
Code will be open-sourced.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips.cr
for more details.
While we encourage the release of code and data, we understand that this might not be possible, "No" an acceptable answer. Papers cannot be rejected simply for including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https
/ prijps.cc/ubblicgguudeee CoodeSumeeieeeeee ssi iessonPolll mollicyy for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: Experimental details have been discussed in the Experiments section and also in the Appendix.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to a level of detail that is necessary appreciate the results and make sense of them.
The full details can provided either with the code, in appendix, or as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [NA]
Justification: Verification results are deterministic on the benchmarks, and no error bars need to be provided.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
43

---

The method for calculating the error bars should be explained (closed form formula, call a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful figures symmetric error bars that would yield results that are out of range (e.g. negative rates).
show in tables or
error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: Time has been reported in tables and we only need one machine and one GPU to run all experiments. The specific hardware details reported in the Appendix.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code of ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics
Answer: [Yes]
Justification:
We have read and acknowledged the NeurlPS Code of Ethics.
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive socictal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: Societal impacts have been discussed explicitly in Appendix E
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
44

---

Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), faireess considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [Yes]
Justification:
No data models released.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g.. code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
We've cited the sources of the benchmarks used, such those from the VNN-COMP
Justification:
Guidelines:
The answer NA means that the paper does use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
45

---

If assets are released, the license, copyright information, and terms of use in the thcode has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
package should be provided. For popular datasets, paperswi
latasets.paperssit
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information not available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification:
No new assets are introduced in this paper.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/moodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsoureing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or equivalent approval/review based the requirements of your country institution) were obtained?
Answer: [NA]
Justification: The paper does not involve crowdsoureing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
46

---

We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Question:
Answer: [NA]
The paper does not use LLMs for important, original, non- non-standard compo- nent of the core methods in this research.
Justification:
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, non-standard components.
Please refer to our LLM for what should or should not be described.
hatoes//herriig.cc/ooffrrrreeeee
47


Reviews:
[{"review_id": "HRsqtCVHL9", "reviewer": "Reviewer_BXrA", "summary": "The paper puts forward a method for tightening intermediate bounds in symbolic bound propagation frameworks for neural network verification. The method uses constraints already derived from the bound propagation passes (final-layer constraints and ReLU split constraints) to optimise the bounds of hidden neurons expressed as linear functions over the input domain. The overhead of the method is discussed and more efficient alternatives are given (relaxed clipping) when it becomes significant. The empirical evaluation shows performance improvements over the state-of-the-art for a wide range of benchmarks. Still the scalability of the method with respect to input dimensionality and layer sizes is not shown.", "questions": "Can you please specify the input dimensionality and layer sizes for which the efficacy of the proposed method may weakened?", "limitations": "The limitations and potential negative societal impact of the work are adequately discussed.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 3, "originality": 3, "strengths_and_weaknesses": "I think that the main a advantage of the proposed method is that the further optimisation of the intermediate bounds is done efficiently, with overall verification performance improvements that are demonstrated across a wider range of benchmarks. The optimisation can of course have a significant overhead with an increasing number of unstable nodes, a shortcoming however that the paper addresses with relaxed clipping.\n\nWhile the performance improvements appear marginal, I think that it is only natural for performance jumps to gradually weaken with the evolution of a research area. Although the work is of course incremental to an existing verification framework, said framework exhibits leading performance and its improvement is therefore significant. Still, this means that the proposed method is only applicable to verification queries that the underlying framework is already applicable (thereby accelerating verification as the title accurately describes), rather than scaling verification to bigger models/harder verification queries.\n\nThe paper is superbly written!", "was_revised": true, "final_justification": "The paper puts forward novel methods that facilitate performance gains in neural network verification across a wide range of benchmarks as demonstrated by an extensive empirical evaluation.", "rebuttal": "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.\n\n> **W1: scaling verification to bigger models/harder verification queries**\n\nThank you for your question. For our response to the scalability concern, please look into our response to question 1.\n\nBesides 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]\n\nThe 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.\nThese 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.\n\nHere’s the total run time on these three verification tasks:\n\n|  | cartpole | Quadrator-2D | Quadrator-2D-larger-ROA |\n| --- | --- | --- | --- |\n| α,β-CROWN [1] | 460s |  209504 s | timeout |\n| Ours | 126s | 78818s | 104614s |\n\nHere’s the total visited domains on these three tasks\n\n|  | cartpole | Quadrator-2D | Quadrator-2D-larger-ROA  |\n| --- | --- | --- | --- |\n| α,β-CROWN [1] | 19,736,971 |  2,630,043,050 | timeout |\n| Ours | 2,797,411 | 1,112,917,436 | 1,472,433,971 |\n\n\nThe 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.\n\nReferences:\n[1] arxiv:2506.01356\n\n\n> **Q1 Can you please specify the input dimensionality and layer sizes for which the efficacy of the proposed method may weaken?**\n\nThank 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:\n\n|benchmark| Method | # verified | ratio | avg. time | domain visited|\n|:-:|:-:|:-:|:-:|:-:|:-:|\n|VIT| base|118.0| 0.59| 22.04| 149.75|\n|VIT| clip n verify|121.0| 0.61| 10.81| 84.84|\n\nOur 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.\nSince 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.\nOur 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.\n\nAnonymous Authors"}, {"review_id": "H4r4rTWLgV", "reviewer": "Reviewer_RvvA", "summary": "This paper proposes a lightweight domain clipping framework to improve neural network verification in branch-and-bound (BaB). \nIt introduces two key methods, i.e., Relaxed Clipping to shrink input domains and Complete Clipping to tighten intermediate bounds, \nboth using linear constraints efficiently. \nBy integrating into BaB, this approach reduces subproblems and improves verification accuracy without expensive solvers.", "questions": "1. How does Complete Clipping determine the top-k key neurons using the BABSR intercept score, and what criteria are used in this heuristic?\n2. In line 787-788, what are the main limitations of Complete Clipping in handling networks with large hidden layers and sparse constraints?\n3. Why is the proposed method restricted to ReLU activation functions, and what challenges arise if other activations are used?", "limitations": "Yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n1. The method is lightweight and efficient, relying only on simple arithmetic operations without LP or external solvers.\n2. It improves both input and intermediate bounds by combining Relaxed Clipping for domain refinement and Complete Clipping for internal bound tightening.\n3. The approach integrates easily into existing BaB-based verifiers such as \\alpha-  \\beta-CROWN with minimal modification.\n4. By clipping irrelevant input regions, it significantly reduces the number of subproblems and BaB splits required.\n5. Subdomains in BaB can inherit linear constraints from their parent, enabling efficient incremental clipping and avoiding redundant computation.\n6. The experiments are comprehensive, and the ablation study is also well-designed.\n\nWeaknesses:\n1. The method is only applicable to ReLU activation functions.\n2. The paper provides few running examples, which limits intuitive understanding.\n3. 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.", "was_revised": true, "final_justification": "I would like to keep my original score for the paper. The authors have provided a clear response to my concerns. The additional experimental results in the responses were convincing.", "rebuttal": "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.\n\n> **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?**\n\nRe: 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. \nEquation 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:\n$$\nL^\\star = \\min_{\\mathbf{x}\\in\\mathcal{X}} \\{ \\mathbf{a}^\\top\\mathbf{x} + c :  \\mathbf{g}^\\top\\mathbf{x} + h \\leq s \\} \n$$\nWe 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. \nTo demonstrate the efficacy of our approach on non-ReLU networks, we present results on the ViT benchmark which constraints transformer layers.\n\n|benchmark| Method | # verified | ratio | avg. time | domain visited|\n|-|-|-|-|-|-|\n|VIT| base|118.0| 0.59| 22.04| 149.75|\n|VIT| clip n verify|121.0| 0.61| 10.81| 84.84|\n\nReferences: [1] arXiv:2405.21063\n\n> **W2 The paper provides few running examples, which limits intuitive understanding.**\n\nRe: 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.\n\n> **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.**\n\n**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.\n\n> **Q1 How does Complete Clipping determine the top-k key neurons using the BABSR intercept score, and what criteria are used in this heuristic?.**\n\n**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]. \nWe 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:\n\n* BaBSR: Strategic selection based on estimated bound impact [1].\n* 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.\n* Random: Baseline without strategic selection.\n\nFor the **top-k values**, we expect a trade-off between computational cost and verification effectiveness:\n- **All neurons refined** does complete clipping on every neuron, maximizing bound tightness but requiring the most computation\n- **Top-20** provides a balanced middle ground\n- **Top-10** uses minimal computation but may miss some important neurons\n\n\nTable for Time\n| Heuristic | Random | -U $\\times$ L | U-L| BaBSR|\n|-|-|-|-|-|\n| **Top-10 per layer (tinyimagenet)** | 16.3s | 16.5 |16.8s | 16.2s |\n| **Top-20 per layer (tinyimagenet)** | 18.1s | 17.9s |17.2s | 15.1s |\n| **All neurons refined (tinyimagenet)** | 22.4s | 22.4s |22.3s | 22.7s |\n| **Top-10 per layer (cifar100)** | 26.2s | 26.6s | 27.0s | 26.1s |\n| **Top-20 per layer (cifar100)** | 29.1s | 28.8s | 27.7s | 24.3s |\n| **All neurons refined (cifar100)** | 36.5s | 36.4s | 36.4s | 36.5s |\n\nTable for Domain Visited:\n| Heuristic | Random | -U $\\times$ L| U-L| BaBSR|\n|-|-|-|-|-|\n| **Top-10 per layer (tinyimagenet)** | 485 | 453 |420 | 388 |\n| **Top-20  per layer (tinyimagenet)** | 381 | 370 |365 | 342 |\n| **All neurons refined (tinyimagenet)** | 278 | 278 |278 | 278 |\n| **Top-10 per layer (cifar100)** | 907 | 847 | 785 | 726 |\n| **Top-20 per layer (cifar100)** | 712 | 692 | 682 | 640 |\n| **All neurons refined (cifar100)** | 521 | 521 | 521 | 521 |\n\nNote 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.\n\nReferences: \n[1] arXiv:1909.06588\n\n**> Q2: In line 787-788, what are the main limitations of Complete Clipping in handling networks with large hidden layers and sparse constraints**\n\nRe: 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.\n\n**> Q3: Why is the proposed method restricted to ReLU activation functions, and what challenges arise if other activations are used?**\n\nRe: 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. \nEquation 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:\n$$\nL^\\star = \\min_{\\mathbf{x}\\in\\mathcal{X}} \\{ \\mathbf{a}^\\top\\mathbf{x} + c :  \\mathbf{g}^\\top\\mathbf{x} + h \\leq s \\} \n$$\nWe 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. \nTo demonstrate the efficacy of our approach on non-ReLU networks, we present results on the ViT benchmark (VNN-COMP 2023) which constraints transformer layers.\n\n|benchmark| Method | # verified | ratio | avg. time | domain visited|\n|-|-|-|-|-|-|\n|VIT| base|118.0| 0.59| 22.04| 149.75|\n|VIT| clip n verify|121.0| 0.61| 10.81| 84.84|\n\nReferences: \n[1] arXiv:1909.06588"}, {"review_id": "6NlVY0BaSr", "reviewer": "Reviewer_XvZp", "summary": "This paper presents Clip-and-Verify, a framework that enhances branch-and-bound neural network verifiers by using linear constraints to tighten intermediate bounds and reduce subproblems. It introduces two clipping algorithms, i.e., complete clipping (direct optimization of intermediate bounds) and relaxed clipping (input domain refinement), and integrates them with existing verifiers. The method claims a reduction of up to 96% in subproblems (although a 96% reduction does not necessarily correspond to improved performance) and improved verification performance on several verification benchmarks.", "questions": "1. Could the authors provide a (clear) justification for using the BABSR intercept score as the basis for selecting neurons? Additionally, have the authors conducted any ablation studies to evaluate alternative heuristics? Understanding the impact of this choice is important, as neuron selection can significantly influence the efficiency of the solver.\n\n2. 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.\n\n3. For verified instances that are also solvable by existing verifiers, how does the solving time under the proposed method compare? Tables 2 and 3 report overall verified results, but it would be helpful to separate the solving time of instances verified by both methods versus those uniquely verified by the proposed framework.\n\n4. For the results presented in Tables 2 and 3, as well as Figure 2, which variant of Clip-and-Verify is used? Relaxed + Reorder?\n\nI may revise my score based on the authors' responses.", "limitations": "Heuristic Sensitivity: The reliance on a top-k heuristic for selecting critical neurons introduces variability; performance may degrade if the heuristic fails to identify impactful neurons.", "rating": 4, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strength:\n\n- The framework repurposes linear constraints from BaB to refine intermediate layers, addressing a gap in prior work that underutilizes such constraints.\n- Experiments on VNN-COMP benchmarks show consistent reductions in subproblems, outperforming existing verifiers in most benchmarks (w.r.t. the verified tasks).\n\nWeaknesses:\n\n- The paper uses a \"top-k objective selection heuristic based on BABSR intercept score\" to choose critical neurons for clipping, but provides little justification. It is unclear how this heuristic ensures consistent performance across networks or input regions. In my view, the selection of objective neurons plays a crucial role in influencing the overall solving efficiency. The paper lacks ablation studies or comparisons with alternative heuristics.\n\n- While the proposed method reduces the number of subproblems, this reduction does not seem to translate into proportional runtime savings, and in some cases, even results in longer total solving time (for example, nn4sys in Table 1), suggesting non-trivial overhead from the clipping framework proposed in the paper. This discrepancy likely stems from the computational costs inherent to the clipping procedures themselves, and the paper does not systematically evaluate this trade-off. This gap hinders a clear understanding of when the clipping procedures provide benefits versus when their overhead outweighs subproblem reductions. \n\n- Figure 1 is not intuitive and difficult to understand.", "was_revised": true, "final_justification": "The authors have addressed my concerns as proposed in the reviews. For the revised version, please add these discussions to the paper.", "rebuttal": "We thank the reviewer for the thorough review and insightful suggestions. We address each concern in detail below.\n>**W1 & Q1: Justifications for top-k heuristics and additional ablation studies/comparisons**\n\nWe 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.\nWe 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:\n**BaBSR**  Strategic selection based on estimated bound impact [1].\n**U-L** and **-(U $\\times$ L)** Proxies that prioritize neurons with wide bound gaps. \n**Random selection** Baseline without strategic selection.\nFor the **top-k values**, we expect a trade-off between computational cost and verification effectiveness:\n- **All neurons refined** does complete clipping on every neuron, maximizing bound tightness but requiring the most computation\n- **Top-20** provides a balanced middle ground\n- **Top-10** uses minimal computation but may miss some important neurons\nTable for Time\n| Heuristic | Random | -U $\\times$ L | U-L| BaBSR|\n|-|-|-|-|-|\n| **Top-10 per layer (tinyimagenet)** | 16.3s | 16.5 |16.8s | 16.2s |\n| **Top-20 per layer (tinyimagenet)** | 18.1s | 17.9s |17.2s | 15.1s |\n| **All neurons refined (tinyimagenet)** | 22.4s | 22.4s |22.3s | 22.7s |\n| **Top-10 per layer (cifar100)** | 26.2s | 26.6s | 27.0s | 26.1s |\n| **Top-20 per layer (cifar100)** | 29.1s | 28.8s | 27.7s | 24.3s |\n| **All neurons refined (cifar100)** | 36.5s | 36.4s | 36.4s | 36.5s |\n\nTable for Domain Visited:\n| Heuristic | Random | -U $\\times$ L| U-L| BaBSR|\n|-|-|-|-|-|\n| **Top-10 per layer (tinyimagenet)** | 485 | 453 |420 | 388 |\n| **Top-20  per layer (tinyimagenet)** | 381 | 370 |365 | 342 |\n| **All neurons refined (tinyimagenet)** | 278 | 278 |278 | 278 |\n| **Top-10 per layer (cifar100)** | 907 | 847 | 785 | 726 |\n| **Top-20 per layer (cifar100)** | 712 | 692 | 682 | 640 |\n| **All neurons refined (cifar100)** | 521 | 521 | 521 | 521 |\n\n\nWhen 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.\nReferences:\n[1] arXiv:1909.06588\n\n>**W2**: Evaluation of the trade-off\n\nYou 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.\nTo 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:\n|Ratio of selected neurons|Total time (s)|Domains visited|\n|-|-|-|\n|0/6|13.37|18,073,174|\n|1/6|11.25|7,254,214|\n|2/6|10.54|4,914,243|\n|3/6|9.70|3,072,863|\n|4/6|9.23|2,088,198|\n|5/6|8.69|1,739,412|\n|6/6|7.66|871,14|\n\nComplete 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.\nThis 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:\n* **Cartpole invariant set**\n* **Quadrotor-2D \\[0.2, 0.2+1e-5] invariant set**\n* **Quadrotor-2D \\[0.2, 0.21] invariant set (larger ROA)**\n**Total runtime (seconds):**\n|Method|Cartpole|Quadrotor-2D|Quadrotor-2D (larger ROA)|\n|-|-|-|-|\n|Relaxed clipping|460|209,504|Timeout|\n|Complete clipping|126|78,818|104,614|\n\n**Total domains visited:**\n\n|Method|Cartpole|Quadrotor-2D|Quadrotor-2D (larger ROA)|\n|-|-|-|-|\n|Relaxed clipping|19,736,971|2,630,043,050|Timeout|\n|Complete clipping|2,797,411|1,112,917,436|1,472,433,971|\n\nComplete 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.\nReferences: \n[1] arXiv:2506.01356 \n[2] arXiv:2208.05740\n\n>**W3: Figure 1 is not intuitive and difficult to understand.**\n\n 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:\n* 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.\n* 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.\n\n>**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.**\n\nRe: 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.\nKey interpretations:\nThe curve’s right end indicates total solved instances—further right means more instances verified within the timeout.\n\n\nA steep initial rise reflects many easy instances solved quickly.\n\n\nA curve below and to the right of another shows consistently faster or earlier solving.\n\n\nThe x-axis ordering reflects instance difficulty, from easy (left) to hard (right).\n\nFor example, on the tinyimagenet benchmark (Fig. 2f), our Complete Clipping + BICCOS variant solves easy instances faster and solves more hard instances.\nAcross 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. \nReferences:\n[1] arXiv:1909.06588\n[2] arXiv:2103.06624 \n[3] arXiv:2109.00498 \n[4] arXiv:2212.10376 \n\n**>Q3: Lack of breakdown comparison on solving time for instances commonly verified by both the proposed method and existing baselines.**\nRe: 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.\n| Instance id | average on simpler instances | 65 | 73 |\n| - |- | -| -|\n| α,β-CROWN | 12615.3496 | timeout | 5474527 |\n| relaxed clipping | 6759.10569 | 1876495 | 291855 |\n| reoder | 6467.95935 | 1416479 | 229755 |\n| complete | 6350.11382 | 531381 | 112431 |\n\nFor 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.\n\n Here’s the instance-wise verification time on acasxu\n\n| Instance id   | simpler instances | 65| 73|\n|-|-|-|-|\n| α,β-CROWN| 1.02872195| timeout| 19.1899|\n| relaxed clipping | 1.00872358| 9.1839| 2.7422|\n| reorder| 1.02828293| 7.6514| 2.6385|\n| complete| 1.09907317| 6.8963| 3.5677|\n\nThe 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.\n\n**>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?**\n**Re:** We used solely complete clipping with reorder in the results presented in these tables. We will make this more clear in the paper."}, {"review_id": "9V2HvXR4Ih", "reviewer": "Reviewer_vsjp", "summary": "The focus of this work is to improve bound tightening within the context of branch-and-bound-based neural network verification, especially bounds for intermediate layers. These bounds are derived from pre-existing linear constraints that are available during typical verification methods, either when using input splitting or ReLU splitting. The paper proposes two methods, \"complete clipping\", which performs coordinate ascent over the dual problem to find tighter bounds, and \"relaxed clipping\", which is a simpler and faster method that considers each linear constraint independently. Experiments are performed on benchmarks from past neural network verification competitions, showing that these bounds help reduce the number of subproblems and improve the number of verified cases.", "questions": "**Optimization methodology**\n\n1. **Sec. 3.2: Complete Clipping, Exact Bound Refinement**\n\n    For the case where $\\\\mathcal{X}$ is a box domain as in Theorem 3.1, then this is exactly an LP with bounded variables and a single inequality constraint. This can be solved with a greedy algorithm. I originally thought that this would be a textbook result, but this might not be the case: I tried to find a clean reference but unfortunately I could not find it. The closest I got was Kellerer, Pferschy, Pisinger, \"Knapsack Problems\", but you would need to look at both Sec. 1.4 and Sec. 2.2. Specifically, this is a continuous knapsack problem, with the difference that the variable bounds are arbitrary instead of $[0, 1]$ and the objective coefficients and weights can be negative. However, these two differences can be easily resolved via transformation: if $l \\\\leq x \\\\leq u$, then just shift and scale $x$ to $x' = (x - l) / u$ so that $0 \\\\leq x' \\\\leq 1$. Furthermore, following Sec. 1.4 of the above book, we can set $x'$ to 0 or 1 if the objective and weight have different signs, or if they are both negative, we can simply flip the sign of $x'$. Then this is exactly the continuous knapsack problem, and it is well known that it can be solved via a greedy algorithm (Sec. 2.2 of the book above).\n\n    The implication here is that the machinery from Theorem 3.1, while it is a nice alternative way to solve the problem, feels unnecessary. Reading Appendix B.2, your algorithm is possibly equivalent (or almost equivalent) to the greedy algorithm above. I believe your $\\\\beta$s are equivalent to the ratios from the greedy algorithm and you are searching for the breakpoint where you can no longer add to the knapsack.\n\n    **What's actionable:** If you agree with the above discussion, then at the minimum, you would need to incorporate the above context, but it does substantially diminish this part of the paper's contribution and perhaps should be rewritten. It is ok if you want to keep the method along with the above context (especially since it could be a way to generalize to other $\\\\mathcal{X}$), but I would not consider it to be a contribution significantly beyond existing literature. That said, I do not think that diminishing this contribution is too bad for the paper, given that the paper has other interesting contributions.\n\n2. **Sec. 3.2: Complete Clipping, Coordinate Ascent for Multiple Constraints**\n\n   In this section, your problem is exactly an LP, so you seem to be proposing an algorithm for general LPs. However, the difference here is that you are actually proposing a dual heuristic for LPs via coordinate ascent, since your algorithm does not solve the LP to optimality. It is plausible that a dual heuristic would work well here, since you want a fast way to obtain dual bounds. That said, the claim that \"coordinate ascent is significantly efficient compared to LP solvers\" is unfounded since you are assuming the LP solver would be used as an exact solver and not as a heuristic. If you are proposing a new dual heuristic for LPs and claiming that it works better than LPs, then you need to compare it with a standard dual heuristic for LPs. In this case, the most straightforward baseline is simply running dual simplex with a time or iteration limit. By stopping dual simplex early, you still have a dual feasible solution and thus a dual bound for your problem. It is plausible that your algorithm does better specifically for verification than limited dual simplex for some reason, but evidence needs to be presented.\n\n   **What's actionable:** I do not believe you can make the claim that your coordinate ascent heuristic works better than a typical LP solver with a time/iteration limit without a proper experimental comparison. Please make that comparison. If your algorithm outperforms the LP solver, then that is great, you have a very nice contribution here. If it does not, then I do not see the value of the proposed algorithm.\n\n3. **Sec. 3.3: Relaxed Clipping**\n\n   Since Theorem 3.2 is a specific case of Theorem 3.1, the same discussion above applies, and it is possible to obtain a simpler proof without resorting to duality. The argument here is even simpler: since only $x_i$ appears in the objective, you can set all other variables to their lower or upper bounds as to loosen the constraint as much as possible, then set $x_i$.\n\n   The clipping to multiple constraints subsection makes sense: this is a very fast way to tighten your bounds. I would have expected these bounds to be rather weak, but it seems that they are still useful in your computational experiments, so that is good.\n\n   **What's actionable:** Similarly to my first comment, you should discuss the simpler approach here. This one is less important, however, and I do not think that adding contextualization diminishes the contribution much in this case.\n\n**Minor comments**\n\n4. For input splits, critical neurons are selected via a top-k heuristic. Could you please include in the paper what metric exactly is the top-k heuristic looking at? BaBSR is mentioned for ReLU splits, but for input splits this is not explicitly mentioned.\n\n5. Do I understand correctly in that for ReLU splits, you only do complete clipping and not relaxed clipping? This is what I understand from Sec. 3.5, but I am not sure about this. Please make sure that is clearer in the paper.", "limitations": "Adequately addressed.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 3, "originality": 3, "strengths_and_weaknesses": "This paper provides an effective way to incrementally improve the performance of branch-and-bound verifiers, whether they branch on the input or on the ReLUs. The end-to-end results are significant and the computational setup, including baselines and benchmarks, seems sound. The general idea of tightening bounds based on pre-existing linear constraints from the verifier is interesting and relatively simple, especially if you can produce very fast ways to do so. The overall writing and quality of the paper look solid to me.\n\nHowever, the proposed optimization methodology has a couple of major issues: 1, it is not as novel as it may initially seem due to some connections that the paper seems to miss, and 2, the paper claims that the coordinate ascent algorithm is better than an LP solver without a proper comparison, particularly since the context is to only produce a dual bound rather than solving the problem to optimality. I will go into details in the \"Questions\" section below.\n\nIn my opinion, the optimization portion of the paper needs significant reworking, and thus at the current state, I cannot recommend acceptance. That said, methodology aside, I believe that this work offers a valuable key message: that efficient-but-weak bound tightening techniques for subproblem bounds are helpful in practice. Therefore, I believe that this can be a solid paper if its issues can be resolved, and thus my current recommendation is borderline.", "was_revised": true, "final_justification": "I originally had major concerns regarding the optimization section, in that they appeared to be reinventing methods without connecting to existing work. While the paper still reinvents methodology to some extent, they provided an excellent rebuttal pointing out the exact mapping between their approach and existing work, and computationally showed that their lightweight dual bound heuristic is superior to out-of-the-box LP-based methods in the specific context of verification, where they require very fast dual bounds at smaller scales than usual. My only major concern was on this topic, and the remainder of the paper looks solid to me as discussed in my review. For this reason, I increased my score from 3 to 5.", "rebuttal": "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.\n\n\n> **Q1. Connections to the continuous knapsack problem**\n\n\n**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.\n\n\nFirst, 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:\n   $$\n   \\min_{x \\in [x_0 - \\epsilon,\\, x_0 + \\epsilon]} \\quad a^\\top x \\quad \\text{s.t.} \\quad g^\\top x + h \\leq 0\n   $$\n   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:\n   $$ D(\\beta) = (a + \\beta g)^\\top x_0 - \\|a + \\beta g\\|_1 \\cdot \\epsilon + \\beta h, \\quad \\beta \\geq 0$$\n\n\n   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.\n\n\nTo **demonstrate equivalence** to the continuous (fractional) knapsack problem, we perform the change of variables:\n   $$ y_i = \\frac{x_i - (x_{0,i} - \\epsilon_i)}{2\\epsilon_i} $$\n   This transforms the primal problem into the standard knapsack form:\n   $$ \\max_{y \\in [0, 1]^n} \\quad r^\\top y \\quad \\text{s.t.} \\quad s^\\top y \\leq t$$\n   where $r = -2\\epsilon \\odot a, s = 2\\epsilon \\odot g, t = -\\left(g^\\top (x_0 - \\epsilon) + h\\right)$.\n   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:\n   * If $r_i \\geq 0$ and $s_i \\leq 0$: Set $y_i = 1$\n   * If $r_i \\leq 0$ and $s_i \\geq 0$: Set $y_i = 0$\n\n\n   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:\n\n\n   * 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.\n   * Both algorithms have **identical time complexity**: $\\mathcal{O}(n \\log n)$ (due to sorting).\n\n\n   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.\n\n\nWe 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.\n\n\nFinally, 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:\n   * 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;\n   * 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.\n\n\n[1] Kellerer, Pferschy, and Pisinger. \"Knapsack Problems\"\n\n\n> Q2. Comprehensive Comparison with LP Solvers\n\n\n**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.\nWe 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:\n\n\n| Method| Avg. Time per BaB Round | Bounds Error (mean) | Bounds Error (std) |\n|-|-|-|-|\n| LP (1 iter) | 2.08s| 0.401| 1.45|\n| LP (10 iter)| 2.47s| 0.0007| 0.0018|\n| LP (20 iter)| 2.49s|0.0| 0.0|\n| Clip (ours)| 0.0028s 0.00085| 0.0019|\n| LP-w\\o iteration limitation (ground truth) |2.50s| 0.0| 0.0|\n\n\nThe reported bounds and time are averaged over 30M LP calls during the entire BaB process, so the numbers are statistically significant. \nNoted 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})$\n\n\nThese results demonstrate that our coordinate ascent method achieves:\n\n\n1. 740× speedup over even the most limited LP heuristic (1 iteration)\n2. Comparable accuracy to 10-iteration LP while being 880× faster\n3. Near-optimal bounds (error of only avg. 0.00085 compared to full LP solution)\n\n\nThe performance difference stems from fundamental architectural considerations in neural network verification:\n\n**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.\n\n\n**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.\n\n\nWe 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.\n\n\n[22, 52]: in our reference\n\n\n> Q3. Direct Proof for Relaxed Clipping\n\n\n**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.\n\n\n> Q4. Top-k Heuristic Details for input split\n\n\n**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).\nHowever, 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).\n> Q5 ReLU Splits and Relaxed Clipping\n\n\n**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."}, {"review_id": "Eth2HCmlSV", "reviewer": "Reviewer_wsa3", "summary": "Neural network verification is critical for mission-critical applications, where branch-and-bound (BaB) with bound propagation is a state-of-the-art approach. However, loose intermediate layer bounds in BaB lead to exponential subproblem growth and inefficient verification. This paper introduces Clip-and-Verify, a linear constraint-driven domain clipping framework to enhance bound propagation verifiers.  \n\nThe framework comprises two novel algorithms:  \n1. **Complete Clipping** directly optimizes intermediate layer bounds using Lagrangian duality, transforming high-dimensional linear programs into efficient 1D concave maximization problems. It handles multiple constraints via coordinate ascent, tightening bounds and identifying infeasible regions.  \n2. **Relaxed Clipping** refines the input domain using linear constraints (e.g., from ReLU splits or final-layer bounds), updating input bounds in closed-form to avoid complex polyhedral operations. The clipped domain tightens intermediate bounds globally.  \n\nBoth algorithms integrate seamlessly into BaB-based verifiers (e.g., α, β-CROWN), leveraging existing linear constraints without extra computation. They reduce redundant subproblems by pruning infeasible input regions and improving bound tightness.  \n\n### Key Contributions  \n1. **Innovative Framework**: A scalable linear constraint-driven clipping framework that enhances intermediate layer bounds without expensive solvers, via Complete and Relaxed Clipping.  \n2. **Efficient Integration**: Algorithms adapt to input and activation BaB, reusing constraints from BaB splits to tighten domains and bounds with minimal overhead.  \n3. **State-of-the-Art Performance**: Reduces BaB subproblems by up to 96% on VNN-COMP benchmarks, achieving superior verified accuracy across diverse networks and verification scenarios.", "questions": "#### **Question1：** Scalability in Extremely Large Neural Networks.  \nThe paper demonstrates efficiency on VNN-COMP benchmarks, but how does Clip-and-Verify perform on extremely large networks (e.g., with millions of neurons or complex architectures like transformers)? \n\n#### **Question2：** Generalization to Non-Standard Network Architectures. \nThe experiments focus on VNN-COMP benchmarks with ReLU networks. How does the framework handle non-standard activations (e.g., Swish, Mish) or specialized layers (e.g., attention mechanisms)?  \n\n#### **Question3：** Real-World Application Scenarios.  \nWhile VNN-COMP benchmarks are standard, how does Clip-and-Verify perform in practical safety-critical applications (e.g., autonomous driving perception networks or medical diagnosis systems)?", "limitations": "No, the authors have not adequately addressed potential negative societal impacts in the provided document. \n\n**Constructive suggestions for improvement:**  \n1. **Address computational resource implications**: Discuss whether the framework’s efficiency gains could inadvertently exacerbate computational resource disparities in academia/industry, potentially limiting access to verification tools.  \n2. **Safety-critical application risks**: Acknowledge that even improved verification might not guarantee 100% safety in mission-critical systems (e.g., autonomous vehicles), and outline strategies to mitigate false negatives/positives.  \n3. **Ethical considerations in verification**: Explore how the framework might influence neural network design (e.g., prioritizing verifiability over performance) and whether this could introduce biases or restrict innovation.  \n\nIncluding such discussions would demonstrate a comprehensive understanding of the research’s limitations and societal role, enhancing the paper’s rigor and responsibility.", "rating": 5, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 2, "strengths_and_weaknesses": "*Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification* presents a novel approach to enhance neural network verification. Here is an assessment of its strengths and weaknesses across the dimensions of Quality, Clarity, Significance, and Originality:\n### Strengths\n1. **Quality**\n    - **Methodological Rigor**: The paper demonstrates high methodological quality. It formulates the problem of tightening intermediate layer bounds in neural network verification as a problem within the linear constraint - driven clipping framework. The two proposed algorithms, Complete Clipping and Relaxed Clipping, are well - defined with detailed mathematical derivations. \n    - **Experimental Validation**: The experiments are comprehensive and well - designed. The authors evaluate Clip - and - Verify on a wide range of benchmarks from VNN - COMP 2021 - 2024, including input BaB and ReLU split BaB benchmarks.\n2. **Clarity**\n    - **Structured Presentation**: The overall structure of the paper is logical and well - organized. It follows a standard academic paper format, with sections on Preliminaries, the proposed method, experiments, related work, and conclusion. Each section builds on the previous one, guiding the reader through the research process in a clear and coherent manner.\n3. **Significance**\n    - **Advancing Neural Network Verification**: The research has significant implications for the field of neural network verification. By improving the efficiency of bound propagation verifiers, it can potentially enable the verification of larger and more complex neural networks. This is crucial for mission - critical applications where the safety and robustness of neural networks need to be formally proven.\n    - **Practical Impact**: The reduction in the number of subproblems during the BaB process and the improvement in verification speed can lead to more practical and scalable verification tools. This can have a direct impact on industries that rely on neural network verification, such as autonomous systems, healthcare, and finance.\n4. **Originality**\n    - **Novel Framework and Algorithms**: The linear constraint - driven clipping framework and the two associated algorithms are novel contributions. While previous work has focused on bound propagation and BaB in neural network verification, this paper introduces a new way of leveraging linear constraints to optimize intermediate layer bounds and input domains.\n\n### Weaknesses\n1. **Quality**\n    - **Scalability in Extreme Cases**: Although the paper claims to preserve the scalability of state - of - the - art neural network verifiers, it is not entirely clear how the proposed algorithms will perform in extremely large - scale neural networks with a vast number of neurons and complex architectures.\n    - **Limited Generalization to Non - Standard Networks**: The experiments are mainly conducted on benchmarks from VNN - COMP, which may not cover all types of neural networks. The performance of Clip - and - Verify on non - standard or emerging network architectures, such as those with novel activation functions or complex topological structures, remains untested.\n2. **Significance**\n    - **Dependency on Benchmark Datasets**: The significance of the results may be somewhat limited by the reliance on specific benchmark datasets. The improvements observed on VNN - COMP benchmarks may not directly translate to real - world scenarios or other types of verification tasks. There is a need to further explore the generalizability of the method in more diverse and realistic settings.\n4. **Originality**\n    - **Conceptual Similarities to Related Work**: Although the proposed framework is novel, there are some conceptual similarities to related work.", "was_revised": true, "final_justification": "All my concerns have been addressed.", "rebuttal": "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. \n\n>**W1 & Q1: Unclear scalability of the proposed method on extremely large or complex neural networks.**\n\nThank 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:\n* 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.\nWe 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%.\n\n|benchmark| Method | # verified (more is better) | ratio | avg. time | domain visited (less is better) |\n|---|---|---|---|---|---|\n|VIT| base|118.0| 0.59| 22.04| 149.75|\n|VIT| clip n verify|121.0| 0.61| 10.81| 84.84|\n\nIn 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.\n\nReferences: \n[1]: arXiv:2312.16760\n[2]: arXiv:2412.19985\n>**W2 & Q2: Limited evaluation on non-standard architectures and activation functions beyond VNN-COMP ReLU networks.**\n\nWe emphasize that our framework is activation-agnostic. In particular, any neuron split of the form:\n$$\nz_j^{(i)} \\leq 0 \\qquad \\text{and } z_j^{(i)} \\geq 0,\n$$\ncan 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. \nReferences:\n[1] arXiv:2405.21063\n\n>**W3 & Q3: Dependence on benchmark datasets raises concerns about the method’s generalizability to real-world, safety-critical applications.**\n\nThank 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.\n\nTo 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].\nThe 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.\nThese 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.\n\nHere’s the total run time on these three verification tasks:\n\n|  | cartpole | Quadrator-2D | Quadrator-2D-larger-ROA |\n| --- | --- | --- | --- |\n| α,β-CROWN [1] | 460s |  209504 s | timeout |\n| Ours | 126s | 78818s | 104614s |\n\nHere’s the total visited domains on these three tasks\n\n|  | cartpole | Quadrator-2D | Quadrator-2D-larger-ROA  |\n| --- | --- | --- | --- |\n| α,β-CROWN [1] | 19,736,971 |  2,630,043,050 | timeout |\n| Ours | 2,797,411 | 1,112,917,436 | 1,472,433,971 |\n\n\nThe 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.\n\nReferences:\n[1] arXiv:2506.01356\n[2] arXiv:2404.07956\n[3] arXiv:2201.06626\n\n>**W4: Conceptual Similarities to Related Work: Although the proposed framework is novel, there are some conceptual similarities to related work.**\n\nWe 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.\nReferences: \n[1] arXiv:2103.06624\n[2] arXiv:2208.05740\n[3] arXiv:2501.00200"}]

Author rebuttal:

Meta-review: This paper introduces a novel and lightweight framework designed to accelerate neural network verification by efficiently tightening bounds within the branch-and-bound process. The reviewers reached a strong consensus on several key strengths of the work. They unanimously praised the method's efficiency, its seamless integration into existing state-of-the-art verifiers, and its demonstrated ability to significantly reduce the number of subproblems across a wide range of benchmarks, improving verification performance. The comprehensive experimental validation was also highlighted as a major strength. Initial concerns were raised regarding the justification for the heuristic used to select neurons for clipping, the trade-off between the method's overhead and its performance gains, and its applicability to non-ReLU architectures. However, the authors provided a thorough and convincing rebuttal, including new ablation studies comparing different heuristics, detailed runtime analysis on difficult problems showing a clear net benefit, and new experiments demonstrating the method's effectiveness on Vision Transformers. The authors have committed to incorporating these additional results and clarifications into the final paper, which will address the main limitations identified during the review process.
Decision: Accept (poster)