Compositional Neural Network Verification via Assume-Guarantee Reasoning
Authors: Hai Duong
David Shriver
ThanhVu Nguyen
Matthew B. Dwyer
Venue: NeurIPS 2025 spotlight ()
Keywords: DNN Verification
Compositional Verification
Assume-Guarantee Reasoning
Primary area: deep_learning
TL;DR: We propose an assume-guarantee compositional framework, CoVeNN, to scale verification to large networks. CoVeNN can verify nearly 7 times more problems than state-of-the-art verifiers.

Abstract: Verifying the behavior of neural networks is necessary if developers
are to confidently deploy them as parts of mission-critical systems.
Toward this end, researchers have been actively developing a range of increasingly sophisticated and scalable neural network verifiers.
However, scaling verification to large networks is challenging, at least in part due to the significant memory requirements of verification algorithms. 
In this paper, we propose an assume-guarantee compositional framework, CoVeNN, that is parameterized by an underlying verifier to generate a sequence of verification sub-problems to address this challenge.
We present an iterative refinement-based strategy for computing assumptions
that allow sub-problems to retain sufficient accuracy. 
An evaluation using 7 neural networks and a total of 140 property specifications demonstrates that CoVeNN can verify nearly 7 times more problems than state-of-the-art verifiers.
CoVeNN is part of the NeuralSAT verification project: https://github.com/dynaroars/neuralsat.

Compositional Neural Network Verification via Assume-Guarante Reasoning
Hai Duong
David Shriver Carnegie Mellon University Pittsburgh, PA 15213
George Mason University Fairfax, VA 22030 hduong228gmu. edu
dshriver@andrew cmu. edu
Thanh Vu Nguyen George Mason University Fairfax, VA 22030 tvn0gmu. edu edu
Matthew B. Dwyer
University of Virginia Charlottesville, VA 22904
matchesbbdyyarrriiginnl.cc
Abstract
Verifying the behavior of neural networks is necessary if developers are con- fidently deploy them as parts of mission-critical systems. Toward this end, re- searchers have been actively developing a range of increasingly sophisticated and scalable neural network verifiers. However, scaling verification to large networks is challenging, least in part due the significant memory requirements of verifi- cation algorithms. In this paper, we propose framework, CoVeNN, that parameterized by an underlying verifier generate a sequence of verification sub-problems to address this challenge. We present an iter- ative refinement- baseed strategy for computing assumptions that allow sub-problems to retain sufficient accuracy. An evaluation using 7 neural networks and a total of 140 property specifications demonstrates that CoVeNN can verify nearly 7 times more problems than state-of-the -hr---r verifiers. CoVeNN is part of the NeuralSAT verification project: http://sttbb.coom//m//ooohhraaat
Sesume-guarante compositional
1 Introduction
Machine learning (ML) techniques are advancing rapidly and have reached a level of performance across range of challenging tasks, e.g., in the medical [ 2 and autonomous driving ( 4 5 domains, that has led developers of critical systems to include ML models as components. To assure that such systems are fit for deployment, researchers have developed variety of formal verification techniques to prove correctness properties of ML models, e.g., [6
12]
Advances in neural network verification (NNV) have been dramatic since the landmark paper by Katz al. (6] which verified properties of models comprised of linear layers. VNN-COMP [13 14]
[6] has chronicled those advances by documenting the growth of benchmarks and verifiers. The largest benehmark in the competition, as measured by the number of layers, has grown from 21; where all but 2-3 of those layers are convolutional. Although these networks present are challenging for verifiers, they do reflect the complexity of modern ML models.
While the number of layers in network is not the only factor that contributes to the difficulty of verification problem, it is directly related its exponential complexity (6) For SoTA verifiers, like CROWN [8) NeuralSAT (17), and PyRAT [18), the worst-case involves each layer generating multiple states which each serve as the starting point for verification the suffix of the network from
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

that state forward. These verifiers perform variety of optimizations to mitigate such state splitting, e.g., by tightening state encodings [9 [0], but complexity grows with the depth of the model.
This complexity is manifest hoth in increased runtime and, perhaps more importantly, in memory uti- lization. SoTA NNV tools make use of GPUs to efficiently manipulate high-dimensional abstractions of model states and GPU memory is generally more limited than CPU memory-in our evaluation ($4) GPU VRAM is limited 24 GB. If verification requires more GPU memory than is available, then the verifier will abort with an out-of-memory (OOM) error. Fig. 1 shows the memory-consumppion of the two top performing verifiers in VNN-COMP a-3-CRON and NeuralSAT, as they check 10 randomly generated local robustness properties of ResNet models trained on CIFAR1O 10, with an increasing number of residual blocks in each model. The x-axis corresponds the number of blocks within the model (c.g., 16 corresponds to ResNet-50 (20]). The y-axis plots the maximum memory consumed, as a percentage of 24 GB, by the verifier across the 10 verification problems. point in the plot is shown if the verifier returns normally on any problem, regardless of whether the result is serified or unknown. a.B-CROWN and NeuralSAT are able to verify all problems up to blocks, but beyond that they exhaust memory. While GPU memory has grown slowly over time, the pace of that growth cannot be relied on for scaling to large neural network verification problems.
In this paper, we introduce a framework for Compositional Verification of Neural Networks (CoVeNN) that can be pa- rameterized by an underlying NNV tool, like a-3-CRWN and NeuralSAT. CoVeNN works by decomposing a neural network into subnetworks that are then verified indepen- dently. As depicted Fig. 1] this allows CoVeNN scale to larger networks than the underlying verifier.
100
Memory (%)
75-
30-
CoVeNN
NeuralSAT
The key CoVeNN the ability to encode the verification of the subnetworks as a series of assume-guarante rea- soning steps. After verifying each subnetwork. CoVeNN merges relevant verifier states, such as approximation bounds, into a compact summary that serves as the as- sumption for the next subnetworks. The corresponding guarantee ensures that, under this assumption, the subnet- work behaves correctly. Together, these assume-guaranter pairs are composed to establish the correctness of the full network.
25
a3-CROWN
10
15
20 # #Boocks
30
35
Fig. 1: Tools' scalability on ResNet-based instances. Maximum memory usage across 10 CIFAR 10-based properties and ResNet- based networks with increasing numbers of blocks, comprised of 3 CNNs with ReLUs.
State merging is classic approach for managing the cost of analysis and verification 211] but risks introducing overapproximation that may prevent properties from being proven. To mitigate this, CoVeNN incorporates multiple refinement strategies that sharpen the precision of assumptions. As detailed in Tab. 4| CoVeNN matches the ability of underlying verifiers on problems for which they complete and the refinement strategies allow to prove properties when scaling to much larger networks. CoVeNN does introduce overhead relative to the underlying verifier, but our evaluation ($4) on a set of challenging verification problems shows that substantial reduction in memory consumption translates to significant increase in the ability to verify problems without an exorbitant time penalty.
Related Work NNV is still a relatively young field, and few lines of work have explored composi- tional NN verification [22 23). However, no prior technique can handle the scale or complexity of networks like RESNET36. We discuss these work and others in more detail in Apdx. D
Contributions The primary contribution of this paper lies in the definition of verifier- infffeerendd framework for compositional assume- guarantte verification of neural network properties. We imple- ment and evaluate CoVeNN's 's ability to reduce verifier memory consumption and increase the number of properties proven (84) and assess overall performance of CoVeNN relative to SoTA DNN verifiers on verification problems formulated over variants of neural network architectures.
Background
DNN Verification Verification of networks using piecewise-linear activation (e.g., ReLUU can be represented satisfiability problem [6] [ 24 [0]. For an L-layer ReLU-based network V with

---

Ni neurons in layer I, the formula:
A
Va. max Σ kEIL.Nd
(Wi-1.j. U2-1,k) big.
1E JEIL,N
defines the network. Given and property = Pin Dout DNN verification problem is formulated by checking the satisfiabilityy a A din A -oout. If it is unsatisfiable, then Φ is a valid property of N. Otherwise, is not valid and counterexample- a witness that Ø is not valid-is satisfying assignment to the input variables in Pin.
[9] adopt techniques from abstract interpretation 22] for efficiency. Since most properties studied in previous work can be expressed as a Boolean expression over linear equation of A'ss outputs, where @ can be merged as the last layer of A to produce an objective function f := Pout oN [19 the final goal reduces to prove: Vz2 E din [(z) 2 O. Solving millse f(x) is challenging due to the non-linearity of DNNs. Modern DNN verifiers overapproximate nonlinear computations of A' to efficiently estimate the lower bound of f(z), denoted as (b, i.c., Vz E Hin lb < (z), then providing lb is sufficient to formally prove f(x) 2 0. This allows abstraction- based DNN verifiers to side-step the disjunctive splitting that is the performance bottleneck of constraint- based DNN verifiers.
DNN Verifiers Modern DNN verifiers 18
Compositional Verification For more than four decades researchers have been investigating compositional methods to scale verification of complex systems [26]. One widely used compositional approach, termed rely- guarantae or assume-guarann system M with specification á), the goal is to prove oin. M - @out-We denote such proof goal with the triple (din: M, dout). Compositional reasoning divides system into parts, { {M,,... M& }. and formulates a set of local verification problems (Ai, M,, G+) such that the guarantees of one component implics the assumptions of another and oin and Øout are the assumption of the first and guarantee of the final components, respectively.
reasoning, was introduced by Stark [27]. For
The promise of compositional methods is that they can reduce the complexity of verification by replacing reasoning about the product of the M; with reasoning about their sum. However, realizing such a framework non-trivial: requires suitable rules to relate the guarantees of one component to the assumptions of another, careful selection of decomposition strategies to achieve cost-effective verification [28), and the identification of appropriate assumptions A, [29]. CoVeNN addresses these challenges by exploiting the inherent sequential structure of neural architectures to define composi- tional proof rules tailored to layer-wise reasoning, adaptively selecting the degree decomposition to maximize proof completion, and iteratively refining assumptions to support verification. Our approach builds on recent work in neural network verification by leveraging modern verifiers' ability to compute tight overapproximations of intermediate outputs, which we then use as assumptions for verifying subsequent layers.
Compositional Verification of Neural Networks
Alg.
shows the CoVeNN algorithm, which takes as input the DNN N, the formulae din = pout representing the property to be proven, the factor indicating the number of generating assumptions, the scale factor F for constructing assumptions, and the number of iterative rounds CoVeNN returns unsat if Φ is a valid property of N, and unknown otherwise.
CoVeNN consists of three main phases: (i) decomposing the original network into subnetworks (lie (ii) computing a coarse overapproximation of intermediate assumptions (line 2 line 4). then checking the last subnetwork (line 5). and (iii) refining the assumptions iteratively until the problem can be verified (line line 18). The following sections describe each phase in detail.
3.1 Decomposition
CoVeNN starts by splitting the original network into K subnetworks (N (N1...,,Ns Nk) line where K internally inferred by CoVeNN using the heuristics described below. This step reduces verification complexity by enabling the sequential verification of smaller, more manageable subnetworks.
More formally, decomposition works follows. A network, NV, is defined by computation graph, GN. whose nodes define computations, e.g., matrix multiplication, and whose edges describe data flow between computations. We restrict our attention acyclic computation graphs, which are common
3

---

Alg. 1: CoVeNN algorithm.
input :eerifirr V. DNN N. property Oin * Oout, number of neurons P, scale factor F and rounds output tunsat the property valid and unknown otherwise
(N1, (Ni,.., decomposelletworkk // automatically split N into K subnetworks
Jover [9mn]
for i E [1...., K] do // initialize coarse overapproxination for each subnetsork
L Yover wwwpppnnooorrppppoxxiattcc.m
Yover 1]))
Ib +- V. w...ecc(Youer [ doat) // check lest subaetwork overapproxination w.r.t. output property if aal((lb 2 0) then check laet subaetwork is verified
L return unsat // (din, dous) is valid
while > do for fo (1; K do attempt varify rirst --1
Jassume generatekssumptionn// 1b VV+..veriyyNN, Yover [1 1], Yossume) // verify assumptions (Di N Taazume)
Yover 1), Tover P) see Apdx.
11
(Lover, Uover) <- Tover extract bounds to refine (tighten)
for [(i.rhs, direction): lt) zip(Tnssume: 1b) do refine assumption neuron i-th then // assune Y, guarentee rbs
if direction
Lover [1] <- rhs li
clse
assune rhs, guarantee -Y, U Uover t rhs
18
Yover [i] +- (Lover, Uover) ) // update refined (tightened) bounds Ib <- V.VVV.Veev veriiy((NW K, Yover [K 1], Dout) verify last aubnetuork
19
20
all((Ib 0) then check if last subaetwork is verified L return unsat // (Bin dout) in valid
r-r-1
return unknown
in many classes of ML models. Our approach supports any decomposition into h subnetworks such that: /' == N e N o .... W1, and the input nodes of each Ni, define cut of Gv [30]. Given such a decomposition a simple proof rule for sequential composition can be defined:
(A,N,,
(I,N
(A,Ns+1 N.
For a k-way decomposed network, the rule is applied h times with carefully chosen intermediate assumptions each serving as the guarantee of one step and the assumption of the next. If the first assumption is A = din and the final guarantee is G = @out, then verifying all subnetworks implies that the original network satisfies din- hout-
Decomposing Heuristics neural network can be decomposed into k subnetworks various ways, and the success of compositional reasoning depends largely on how it is decomposed (28). CoVeNN uses four heuristics to automatically guide this choice. We prioritize (1) cuts that define the inputs of layers in the network, because this leads subnetworks that have input/output shapes that well-supported by existing verifiers; (2) minimum cuts, because these reduce the dimensionality of the intermediate assumption, I; (3) cuts that later in the network cut, C2 is later than cut, C₁ if all vertices in are dominated by some node in C₁, because this reduces imprecision in computation of I; and (4) cuts that yield the largest subnetworks that are amenable verification by existing verifiers, because this minimizes the number of subnetworks that need to be verified.
3.2 Bound Approximations and Verification
CoVeNN next performs an initial, coarse overapproximation for each subnetwork sequentially (line line 4). This is done using an off-the-shelf verifier y-typically a modern BaB-based tool such as a;3-CRONN or NeuralSAT(2] [24 which returns conservative output bounds based on the current property. CoVeNN leverages the computed bounds to verify properties and guide the
iterative refinement discussed in $3.

---

Once the overapproximations are computed, CoVeNN simply checks whether the approximation of the last subnetwork satisfies the output property (line 5). As described [2] if V returns lower bound lb 2 0 (line 6) the property is verified and CoVeNN concludes unsat. Otherwise, it proceeds with refinement to sharpen the result.
Although only the last subnetwork is being verified (since it directly relates to the original output property), this verification depends on the approximations computed for the earlier K-1 subnetworks. These serve as assumptions in chain of assume- -uaaaneee obligations. Each intermediate bound acts as both a guarantee for its originating subnetwork and an assumption for the next. We will discuss more about these assumptions and their refinement in the next section.
3.3 Iterative Refinement
In most cases, the initial approximation in $3.2 is too coarse to verify the property of interest. Thus, CoVeNN enters the refinement phase (line 9 line 18). which iteratively tightens the approximations until the problem can be verified (e.g., returns unsat) or CoVeNN exceeds the maximum predefined rounds r (e.g., returns unknown). CoVeNN's 's refinement has three main steps: (1) generating assumptions, (2) verifying assumptions, (3) refining assumptions. The algorithm makes up to r iterations comprised of sequentially verifying each subnetwork.
Generate Assumptions For each subnetwork Wr, assumptions Yassume are generated (line 10)
based on its input conditions and pre-computed overapproximation following the procedure in Alg. CoVeNN automates the generation of assumptions by systematically interpolating between coarse overapproximations and tight sample-driven bounds on subnetwork outputs, as detailed in [Apdx. C These assumptions reflect the possible output behavior of Ni given the input property "ii-
CoVeNN attempts to verify Tassume of the subnetwork Ni or (Tin, SnnnNNi Tassume), using the verifier V (line 11). As described above, CoVeNN extracts the lower bound lb from the verifier to facilitate this task. If verify an assumption fails (i.e., lb 0), Tassume is invalid and CoVeNN refines them using verified 1b (line line 18).
Verify Assumptions
Refine Assumptions This refinement adjusts the assumptions to eliminate unverified regions, making them hold for the current preconditions and subnetwork. Refined assumptions then are propagated forward serving as input property for the next subnetwork.
When an estimated assumption Tassume Tine 10p cannot be verified, we need to refine so that becomes valid. Particularly, [[ne line 18 outlines CoVeNN's 's refinement method, which adjusts Tassume using the formally verified lower bounds 1b. CoVeNN first identifies the direction of the inequality to decide the appropriate refinement strategy. If the direction is ">", the assumption being verified is of the form Y. 2 rhs (line 14p. The verifier V has only formally confirmed that Y, rhs 2 li, where li O. meaning that Y, greater than equal to rhs adjusted by the lower bound li. Therefore, to make that assumption valid, the right-hand side value is loosened as rhs + li (line 15). A dual of this process is used to refine the upper bounds.
3.4 Example
We illustrate CoVeNN by verifying that Ms depicted in Fig. 2a has the property:
(2) When given the network '' and the property Φ. CoVeNN first attempts to prove N F= d. denoted by the triple (oin, , Pont), using an underlying verifier V. Suppose V fails verify the property due to memory exhaustion.
din
Pout = (-2 S x < 2 A -1 S 22 $ 1) + (y1 > y2)
CoVeNN now decomposes N into two subnetworks Inne 1. .N1 and N/2 such that = N2 Mi as shown in Fig. 2a Next, CoVeNN uses V to compute an output overapproximation for the K - 1 subnetworks from the input condition din <line iine 4). We call the computed constraint an assumption and use 7/2 to denote the assumption computed for network i. For this example, ? = -5 S 7221 < 5 A -10 < n22 S 10. Since this assumption initially is overapproximation, consequence of this is that V has produced proof of No. inherently.
Once CoVeNN reaches the final subnetwork, it uses V to check the last overapproximation w.r.t. the output property (Tine 5). e.g., Povt- If this succeeds then we have a proof that (0in; N, @out). this case, this does not succeed, so CoVeNN attempts to refine the assumption [ine 8 line 22
5

---

2:
21
22
>
Sampled Reglon
Trasmpic
U Unangia
Liint
Interpolated Region
U
[-1;1]
N
[-1]1]
N1
N3
Lover
Over Approsimation
U Useer
(a)
(b)
Fig. 2: (a) Example of a decomposed FC network with three hidden layers and (b) Regions of hidden ReLU.
Refinement proceeds by sampling the behavior of N1, 1, subject to Pin- and computes hyperrectangle that tightly approximates sampled outputs: Fig. 2b depicts this sampled region in red. In the example, let this sampled assumption be 01 2 < 721 2 -4 T222 I 4. Since this tight approximation of the sampled behavior the likelihood that is a valid postcondition of Ni is low. We address this by interpolating between it and the overapproximating region determine new assumption (line 10j, 7í such that "1 2 2n 2 01. With hyperrectangulaa constraints one approach is to simply scale the sampled region,
(71 σ1) + F1, by some predefined factor, s E [o, 1]. Fig. 2b) depicts an interpolated region in green with scaling factor of 0.5. In our example, this new assumption is 7/ = -3 n21 33A A -5 S 1222 S 5 and we use V to verify (Pin, 11, N,,71 71) (line 1Tp.
If this succeeds, then CoVeNN uses V to attempt to verify (2, Dou) llne 19). If it fails we exploit the output bounds computed by V generate valid assumption line 1ine 18); >
(-4 S T221 S 4-777 7222 S 7) and CoVeNN then seeks to verify (71 N2, Pout) qline 19 In this example that verification succeeds, thereby completely the proof of (din, Pout) through sequence of simpler verification problems.
3.5 Formal Correctness
The correctness of CoVeNN is based on the soundness of the assume-guarantee decomposition 1
and the iterative refinement of the assumptions (3.33). Note that assume that the underlying verifier V is sound, i.e., its overapproximations are valid $3.2) Below we provide the theorems and proof sketches for the soundness of CoVeNN, the full proofs are provided in/Apdx. B
Compusitional Verification The following states that the chain of assumptions and guarantees of subnetworks (3.1) proves the original property din Dout of the entire network N.
Thm. (Compositional Verification via Assume- Assume-Guarantee Reasoning). Given neural network
N T - Rm decomposed into K subnetworks such that N =N a ... o NN, a property din Sout, and intermediate predicates -1-,, where " Din and 7 @out, the global specification holds whenever the every local property is valid:
A (7x (2k-1.Nk,77))
(DingN Pout)
Proof Sketch. For each pair of adjacent networks shown in Eq. assume-guarantee obligations proved, establishing that each intermediate predicate "Yk is preserved under corresponding subnetwork Nt. Composing these local guarantees forms chain from the input property din the output property Pout: showing that the global specification holds for the entire network.
The following states that the refinement process $3.3) states that each refinement step always results in bounds that are formally valid, thereby ensuring that the iterative tightening of assumptions preserves correctness throughout the verification chain.
Refinement Process
Thm. (Soundness of Iterative Bound Refinement). Suppose the base verifier V soundly establishes, for neuron Y, right-ham side rhs, a direction xE (2, S} and a corresponding verifier bound

---

Tab. 1: Benchmark instances.
Benchmark
Layers
Neurons
Parameters
Instances (U/S/?)
VAE BASE
20
43K
10K
20/0/0
VAE_ WIDE
20
86K
39K
20/0/0
VAE. DEEP
28
44K
15K
7/0/
RESNET6
20
283K
113K
11/0/9
RESNET12
38
627K
230K
9/0/11
RESNETIS
56
700K
348K
18/0/2
RESNET36
110
1032K
706K
13/0/7
Total
98/0 42
ò (where d 0fror "2" and 0.for "S"), that rhs * 8. Then, the refined inequality
Y, (rhs +
verified. Therefore, updating the right-hand side to rhs 8 yields a verified assumption by V.
Proof Sketch. Given that the verifier soundly proves Y, - rhs 5, it follows that Y, x (rhs + 5) holds. Updating the bound accordingly yields a refined assumption that remains sound.
Soundness of CoVeNN The following combines the previous two theorems show that CoVeNN sound: all local subproblems generated during decomposition are either formally verified or refined, then the global property holds for the original network.
Thm. (Soundness of CoVeNN). Let N be neural network and Oin Pout be input/output properties such that Co VeNy verifies N satisfies Φin = Oout. CoNeNN applies Thmm. 1to decompose N and assume all local subproblems are formally verified by a sound underlying verifier V or formally refined as Thm. 2. Then N indeed satisfies din = Pout-
Proof Sketch. CoVeNN decomposes the network into subnetworks and verifies a sequence of assume- guarantee obligations using sound verifier. By composing these verified local implications, the global property om = Oout follows.
L
Non-Linear Activations While our discussion has primarily focused on ReLU activations, CoVeNN extends naturally to networks with other non-linear activations such as tanh and sigmoid. The support for non-Rel.U is specific to the underlying verifier that we use to obtain bounds, e.g., a:R-CROWN and NeuralSAT both support Ron- activations via abstract interpretation techniques. CoVeNN extracts interval bounds from these verifiers as intermediate assumptions rather than discrete neuron status (c.g., on/off). These interval bounds remain valid regardless of the activation function and preserve soundness during refinement.
Evaluation
We evaluate the scalability and cost-effectiveness of CoVeNN based three research questions CoVeNN's performance compared to state-of-the-ar verifiers (RQ1); the effectiveness refinement ($3.3) (RQ2); CoVeNN's robustness variations in the underlying verifier (RQ3); and the impact of parameter tuning on CoVeNN's performance (RQ4).
Underlying Verifiers We experiment with two variants of CoVeNN, each configured with a different underlying verifier: NeuralSAT and Q.3-CROwN Both tools are state-of-the-an in DNN verification and allow us to extract the lower bound estimates needed for CoVeNN's refinement process.
Benchmarks We use two scalable families of benchmarks (Apdx. E. Tab. provides details on the
variants of the ResNet and VAE benchmarks used in our experiments. For each network, we generated 20 robustness properties. For ResNets these are local robustness classification properties and for VAEs these are local reconstruction robustness properties (Apdx. A). Across the 140 combinations
See results in the VNN-COMP'24 report 15
Tab. 35). PyRAT commercial and has available code.

---

Tab, 2: Comparing CoVeNN SoTA verifiers; solved problems in bold.
VAE BASE
VAE WIDE
VAE
DEEP
RESNET6 RESNETI2
RESNETIS
RESNET36
Overall
Verifier
K
K
V
%
K
K
% K
CoVellllss
20
100.0
1-2
95.0
2
5
25.0
11 55.0
45.0
2
18 90.0
13 65.0 3
95 67.9
4 20.0
2
6
30.0
10 50.0
45.0
2
17 85.0
13
65.0
3
[9 42.1
CoVeNNxeem'
3 15.0
1
11 55.0
45.0
2
45.0
13
65.0
3
45 32.1
NeuralSAT
3 15.0
1
11
55.0
14 10.0
a.3-CROWN
5.0
50.0
NaurdSAT
125
ReaNet
2000
+&-CROWN
VAB
CoVeNNNi
2500
CoViNNNaeeaa
Memorr (%)
100
Ruatines
CoVeNN,a
75
1000
30-
1000
10
40
3.0
70
90
100
NeuralSAT
a/-CROWN
CoVisNNgs
(a) Solved problems sorted by runtime.
(b) Average memory usage per verifier.
Fig. 3: CoVeNN performance compared to SoTA verifiers.
of networks and properties: 98 are known be unsat (U), none of them sat (S), and of the remaining 42 instances no verifier in our study was able to solve the problem (?). Note that robustness properties can vary significantly in complexity based on the centerpoint and e, e.g., 31 Fig. 2].
Setup Our experiments were run on a Linux machine with an AMD Ryzen Threadripper PRO 5975WX 32-Core, 128 GB RAM, and an NVIDIA GeForce RTX 4090 GPU with 24 GB VRAM. Timeout for a single instance is set to 3600 seconds or the maximum number of rounds r is 4. Note that our results deterministic and random process is involved. We describe detailed configuration and model information for our experiments in Apdx. E
4.1 RQ1: Comparing to Non-Compositional SoTA Verifiers
Tab. 2 presents the results of running both CoVeNN variants (CoVeNNNs and CoVeNNa,), CoVeNNuetma" a naive version of CoVeNN without refinement using the NeuralSAT backend, and the standalone NeuralSAT and a:3- CROWN verifiers the benchmarks. Column V shows the number of prob- lems verified with the percentage solved shown in column %. Column K shows the number of decompositions inferred
CoVeNN. Tools that indicated with a "." (e.g., NeuralSAT cannot solve any instances of RESNET12 and VAF_DEEP, etc.). Across the benchmarks CoVeNN solves more than times the number of problems than the best non-compositional solver. We note that neither NeuralSAT nor Q.3-CROWN could solve any instances of VIE_WIDE, CoVeNN to scale verification beyond the state-of-the-art RESNET36, which is comprised of 110 convolutional layers, requires the most aggressive decomposition (K 3). but even for such large network CoVeNN is able to verify 65% of the properties. CoVeNNuenmt performs better than standalone verifiers, but falls short of any CoVeNN variants, demonstrating the importance of refinement ($4.2).
of memory or time
benchmark
RESNETI2 and beyond, which demonstrates the ability of
Fig. 3a and Fig. 3b provide additional details on runtime and memory usage. Fig. 3a shows that regardless of the underlying solver whether CoVeNN uses its refinement strategy ($.3)) it can solve many more problems than MeuralSAT and 0:3-CROWN within the same time constraints. While NeuralSAT and a-3-CROWN reach their limits after solving 14 problems, CoVeNN solves as many as 95 instances.
Fig. 3b shows that CoVeNNN consumes significantly less memory than NeuralSAT
"Messured by the internal function torch. cuda. mem_ sate__ee_iimmmm info in Pn Porch.. Detailed calculation Eq. 10

---

100
10
Tightened
Neuton Outpat Reduction
70
Rediveement Rounds
60
N Nanabee
300
20-
21.0
0-
VAE BASE
VAE WIDE
VAE DEEP
RESNETI2
RESNETIS
RESNET36
Fig. 4: Percentage of neurons tightened and percentage of their output range reduction.
and 1.3-CROWN, which often encounter OOM errors. $4.4 reports on a more detailed parameter and ablation study of CoVeNN on these benchmarks.
4.2 RQ2: On the Effectiveness of Assumption Refinement
Fig. 3a shows that even without refinement, CoVeNNReent solves nearly 4 times as many problems as SoTA methods and that this rises to nearly 7 times with refinement enabled. To explore how refinement achieves this we recorded additional data on the refinement process. Fig. 4 reports, for each problem where > 1, the percentage of neurons that were tightened in some round of refinement (red); the percentage by which the output ranges of those neurons were reduced (blue); and number of rounds of refinement performed (green on the 2nd y-axis).
For the VAE benchmarks, 17 of the BASE problems and all of the other problems involved refinement. There were more rounds of refinement and, except for the DEEP benchmark, this resulted in high percentage of tightened neurons and significant output range reduction. For the DEEP benchmark, rounds of refinement continued until the timeout was reached on 15 of the 20 problems. For the RESNET benchmarks, we observe a very different profile. Fewer rounds of refinement were needed, especially for RESNETI8 which was able to prove 18 of the 20 problems. This more than double the amount that could be proven with refinement disabled. The verification problems are randomly sampled across all benchmarks which leads different performance profiles. The data for RESNETI2 and RESNET36 demonstrate that for some problems the compositional nature of CoVeNN alone can lead to verification improvements (see the CoVeNNRennE row in Tab. 2). but additional effort of refinement does not yield further improvements.
4.3
RQ3: Robustness to Underlying Veritiers
Tab. clearly indicates that CoVeNN significantly increase the number of solved problems regardless of the underlying verifier. While CoVeNNNs outperforms CoVeNN ag, our analysis suggests that this is a fundamental limitation of either CoVeNN or a,8-CRWW
We analyzed the performance of CoVeNN on VAE BASE and VAE_WIDE, the cases where there substantial performance gap. We found that aR3-CRWNN does not support ConvTransposs layers in several of its heuristics for applying optimizations. This means that its performance both verifying assumptions line and verifying the final subnetwork line 19 suffer. We conjecture that better support for this layer type could ameliorate this issue, but we acknowledge that QB-CROWN has numerous hyperparameters and we did not perform the type of expert tuning that the developers of a:3-CRON apply when running benchmarks. The reduced performance on VAE benchmarks could be due to this well.
The RESNET benchmarks show a clearer trend. a,3-CROWN comes with hyperparameter settings for this architecture which reuse, and we very consistent degrees of improved scalability regardless of the underlying verifier.
4.4
RQ4: CoVeNN's Performance with Parameter Tuning
Fig. 5 compares CoVeNN's performance across different parameter configurations using NeuralSAT as the underlying verifier. We explore variations in (number of assumptions per round) and F (interpolation factor) against basclines including NeuralSAT, CRONN and CoVeNNRRenms.

---

3500
NeuraSAT
3000
aJ-CROWN
CoVeNNNs (P=61, F=1/3)
2500
CoVeNNNs (P=128, F=
Runhiimes
2000
CoVeNNNs (P=256, F- 1/3)
CoVeNNNs (P (P-128, F 1/2)
1500
CoVeNNNs (P=256, F= 1/2)
1000
NoV (P-128, F-1/3)
CoVeNNawtn
500
20
30
50
60
90
100
Fig. S: Ablation study different parameters of CoVeNN.
CoVeNN exhibits dependencies on P. which determines how many neurons are selected for refinement in each round. When P is small (P 64), CoVeNN refines fewer neurons per iteration, limiting its ability to tighten bounds and solving only 83 problems. Conversely, when P is large (P = 256), CoVeNN attempts to refine many neurons simultancously, increasing computational overhead and often causing timeouts before properties can be proven. The optimal P 128 strikes balance between refinement coverage and computational efficiency.
In contrast, CoVeNN demonstrates robustness to the interpolation factor F. The performance difference between F 1/3 and f P= 1/2 marginal (e.g., single problem when P = 128), indicating that CoVeNN's iterative refinement process can effectively compensate for initially coarse assumptions regardless of the interpolation strategy.
In summary, (RQ1) CoVeNN verifies over 6x more problems than SOTA verifiers and scales to deeper networks with less memory, highlighting the effectiveness decomposition. (RQ2) Refinement significantly boosts performance: CoVeNNRaMm already outperforms SoTA by 4x. and refinement raises this to nearly 7x. (RQ3) CoVeNN significantly improves verification regardless underlying solvers (performance gaps depend the backends, not from CoVeNN itself). (RQ4) CoVeNN's performance depends on the number of neurons selected for refinement but robust to the interpolation factor.
Conclusion
NNV has scaled tremendously in recent years, but networks continue grow in complexity which limits the applicability of SoTA NNV techniques to real-world networks. Our work on CoVeNN is first step in realizing the promise of compositional neural network verification, and preliminary results show that CoVeNN can scale significantly beyond SoTA verifiers.
Limitations This work focuses on compositional verification, not falsification. Compositional falsification is more difficult because over-approximation favors verification rather than finding counterexamples. However, CoVeNN to compute under-approximations of inputs reachable from the violated output space. If the under- approximated input region is a subset of the specified precondition, the violation can be confirmed.
potentially incorporate backward analysis methods [32]
CoVeNN supports acyelic networks, e.g., feedforward structures, by finding appropriate "cuts" in the computation graph. For RNNs, CoVeNN can use unrolling [33 to create natural decomposition points after each timestep. For general cyclic graphs, handling cycles requires more sophisticated circular assume- guarantee proof rules 34
Finally, CoVeNN does dimensions within an assumption that must be tightened to climinate violations.
feedhack from counterexamples, but plan them to identify the
Potential Negative Societal Impact The techniques developed in this work can reveal flaws in sensitive applications that may be exploited for malicious intent. However, these same methods also allow developers to identify such attacks and fix them prior to model deployment.
10

---

Acknowledgments and Disclosure of Funding
We thank the anonymous reviewers for their helpful comments. This work was supported part by funds provided by the National Science Foundation awards 2129824, 2217071, 2501059, 2422036, 2319131, 2238133, and 2200621, and by an Amazon Research Award and an NVIDIA Academic Grant.
References
[1] R. Wang, T. Lei, R. Cui, B. Zhang, H. Meng, and A. Nandi, "Medical image segmentation using deep learning; A survey," IET Image Processing, vol. 16, no. 5, pp. 1243-1267, 2022.
[2] B. Kovatchev, A. Castillo, E. Pryor, L. Kollar, C. L. Barnett, M. D. DeBoer, S. A. Brown, and N. S. Team, "Neural-net artificial pancreas: a randomized crossover trial of a first-in-class automated insulin delivery algorithm," Diabetes Technology & Therapeuties, vol. 26, no. 6, pp. 375-382, 2024.
[3] L. Zhang, A. Yang. Y. Xiong, S. Casas, B. Yang, M. Ren, and R. Urtasun, "Towards unsupervised object detection from lidar point clouds," in Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pp. 9317-9328, 2023.
[4] P. Wu, X. Jia, L. Chen, J. Yan, H. Li, and Y. Qiao, "Trajectory-guided control prediction for end-to-end autonomous driving: A simple yet strong baseline," Advances in Neural Information Processing Systems, vol. 35, pp. 61 19-6132, 2022.
[5] H. Shao, L. Wang, R. Chen, H. Li, and Y. Liu, "Safety- -Safety-enhanced autonomous driving using interpretable sensor fusion transformer," in Conference Robot Learning, pp. 726-737, PMLR, 2023.
[6] G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, "Reluplex: An efficient SMT solver for verifying deep neural networks," in International Conference on Computer Aided Verification, pp. 97-117, Springer, 2017.
[7] R. Bunel, P. Mudigonda, I. Turkaslan, P. Torr, J. Lu, and P. Kohli, "Branch and bound for piecewise linear neural network verification," Journal of Machine Learning Research, vol. 21,
no. 2020, 2020.
[8] D. Zhou, C. Brix, G. A. Hanasusanto, and H. Zhang, "Scalable neural network verification with branch-an and bound inferred cutting planes," arXiv preprint arXiv:2501.0022: 2024.
[9] C. Ferrari, M. N. Mueller, N. Jovanović, and M. Vechev, "Complete Verification via Multi- Neuron Relaxation Guided Banchhandd-ounde Representations, 2022.
International Conference on Learning
[10] H. Duong, D. Xu, T. Nguyen, and M. B. Dwyer, "Hamessing neuron stability to improve dnn verification," " Proc. ACM Softw. Eng., vol. 1, no. FSE, 2024.
[11] H. Wu, O. Isac, A. Zeljić, T. Tagomori, M. Daggitt, W. Kokke, I. Refaeli, G. Amir, K. Julian, Bassan, et al., "Marabou 2.0: a versatile formal analyzer of neural networks," in International Conference on Computer Aided Verification, pp. 249-264, Springer, 2024.
[12] S. Bak, "nnenum: Verification of ReI.U Neural Networks with Optimized Abstraction Refine- ment," in NASA Formal Methods Symposium, pp. 19-36, Springer, 2021.
[13] C. Brix, M. N. Müller, S. Bak, T. T. Johnson, and C. Liu, "First three years of the international verification of neural networks competition (VNN-COMP)" International Journal on Software Tools for Technology Transfer, pp. 1-11, 2023.
[14] C. Brix, S. Bak, C. Liu, and T. T. Johnson, "The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results," 2023.
[15] C. Brix, S. Bak, T. T. Johnson, and Wu, "The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results," arXiv preprint 1:Xi::2412.119883 2024.
[16] S. Bak, C. Liu, and T. Johnson, "The Second International verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results," arXiv preprint arXiv:2109.000 2021.
11

---

[17] H. Duong, T. Nguyen, and M. B. Dwyer, "Neuralsat: A per-ooerformance verification tool for deep neural networks," " in International Conference on Computer Aided Verification. pp. 409- 423, Springer, 2025.
[18) A. Lemesle, J. Lehmann, T. I.. Gall, and Z. Chihani, "Verifying neural networks with pyrat," in International Static Analysis Symposium, pp. 11-33, Springer, 2025.
[19] H. Zhang, Wang, K. Xu, L. Li, B. Li, Jana, C.-J. Hsieh, and J. 7. Kolter, "General neural network verification," Proceedings of the 36th International Conference on Neural Information Processing Systems, 2022.
cutting planes for bound-propp poweidddpropgattonbaaaeeee
[20] K. He, X. Zhang, S. Ren, and J. Sun, "Deep residual learning for image recognition." " in Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 770-778, 2016.
[21] F. Nielson, H. R. Nielson, and C. Hankin, Principles of Program Analysis. Springer, 1999.
[22] D. Gopinath, H. Converse, C. Pasareanu, and A. Taly, "Property inference for deep neural net- works," in 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 797-809, IEEE, 2019.
[23] R. Ivanov, K. Jothimurugan, S. Hsu, S. Vaidya, R. Alur, and O. Bastani, "Compositional learning and verification of neural network controllers," ACM Transactions Embedded Computing Systems (TECS), vol. 20, no. 5s, pp. 1-26, 2021.
[24] H. Duong, T. Nguyen, and M. Dwyer, "A DPLL(T) Framework for Verifying Deep Neural Networks," arXiiv preprint arXivv2307.10266. 2024.
[25] P. Cousot and R. Cousot, "Abstract interpretation: unified lattice model for static analysis of programs by construction or approximation of fixpoints." " in Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 238 252, 1977.
[26] J. Misra and K. M. Chandy, "Proofs of networks of processes." IEEE transactions on software engineering, no. 4, pp. 417-426, 1981.
[27] E. W. Stark, "A proof technique for rely/guarantee properties." in Foundations of Software Technology and Theoretical Computer Science: Fifth Conference, New Delhi, India December 16-18, 1985 Proceedings 5, pp. 369-391, Springer, 1985.
[28] J. M. Cobleigh, G. S. Avrunin, and L. A. Clarke, "Breaking up is hard to do: An evaluation of automated assume-guaaante reasoning," ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 17, no. 2. pp. 1-52, 2008.
[29] C. S. Pāsäreanu, D. Giannakopoulou, M. G. Bobaru, J. M. Cobleigh, and H. Barringer, "Learning to divide and conquer: applying the 1* algorithm automate assume-guarantee reasoning," Formal Methods in System Design, vol. 32, pp. 175-205, 2008
[30] T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to algorithms. MIT press, 2022.
[31] D. Xu, J. J. Mozumder, H. Duong, and M. Dwyer, "Training for verification: Increasing neuron stability to scale DNN verification," in Tools and Algorithms for the Construction and Analysis of Systems- 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, to appear, Springer, 2024.
[32] X. Zhang, B. Wang, M. Kwiatkowska, and H. Zhang, "Premap: A unifying preimage approxima- tion framework for neural networks," Journal of Machine Learning Research, vol. 26, no. 133, pp. 1 1-44, 2025.
[33] Y. Jacoby, C. Barrett, and G. Katz, "Verifying recurrent neural networks using invariant in- ference." in International Symposium on Automated Technology for Verification and Analysis, pp. 57-74, Springer, 2020.
[34] K. Abd Elkader, O. Grumberg, C. S. Päsäreanu, and S. Shoham, "Automated circular assume- guarantee reasoning," " Formal Aspects of Computing, vol. 30, no. 5, pp. 571-595, 2018
[35] Toledo, D. Shriver, S. Elbaum, and M. B. Dwyer, "Deeper notions of correctness in image- based dnns: Lifting properties from pixel to entities." in Proceedings of the 31 ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 2122-21266 2023.
12

---

[36] K. Ahmed, K.-W. Chang, and G. Van den Broeck, "A pseudo-semantis loss for autoregressive models with logical constraints, Advances Neural Information Processing Systems, vol. 36, 2024.
[37] J. K. Christopher, S. Baek, and F. Fioretto, "Constrained synthesis with projected diffusion models," in The Thirtt-eighth Annual Conference on Neural Information Processing Systems, 2024.
[38] D. Kingma, "Auto-eneoding variational bayes," arXiv preprint arXiv:1312.6114, 2013.
[39] R. Rombach, A. Blattmann, D. Lorenz, P. Esser, and B. Ommer, "High-resolution image synthesis with latent diffusion models," " in Proceedings the IEEE/CVF conference on computer vision and pattern recognition, pp. 10684-10695 2022.
[40] S.-i. Amari, "Backpropagation and stochastic gradient descent method." Neurocomputiing vol. 5, no. 4-5, pp. 185-196, 1993.
[41] D. Xu, D. Shriver, Dwyer, and S. Elbaum, "Systematic Generation of Diverse Benchmarks for DNN Verification," in International Conference on Computer Aided Verification, pp. 97-121, Springer, 2020.
[42] A. Loquercio, A. I. Maqueda, C. Del-Blanco, and Scaramuzza, "Dronet: Learning to fly by driving," IEEE Robotics and Automation Letters, vol. 3, no. 2, pp. 1088-1095, 2018.
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 our theoretical and empirical results problems than SoTA NNV tools across benchmarks.
CoVeNN solved more
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 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 of the work performed by the authors?
Answer:
[Yes]
Justification:
The limitations are explicitly mentioned in $
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 on 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 a few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
13

---

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 or 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 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 be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?
Answer: [Yes]
Justification:
The theorems and their proof sketches are listed in $3.5 and detailed in Apdx. B
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 or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proof' 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 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: Apdx. E
The model architectures and configurations used are provided in
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, No answer 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 to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make 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 to 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 are appropriate to the research performed.
14

---

reproducible, they While NeurIPS 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) If the contribution is primarily new algorithm, the paper should make it clear how to reproduce that algorithm. (b) the contribution is primarily a new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is 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 or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome to describe the particular way they provide for reproducibility. the case of closed-source models, may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
The data and code with instructions to reproduce the results have been uploaded to an anonymized repo.
Justification:
Guidelines:
The answer NA means that paper does not include experiments requiring code. Please see the NeurIPS code and data submission guidelines (httpss/nnips.c//pbbicc guiddssCCoeeubbiisiioooooo
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not 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 reproduce the results. See the NeurlPS code and data submission guidelines (https) for more details.
//ips.cc/publice httplii/ggiiiee/ooSSSeiiisseeees
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 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 as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
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?
Question:
Answer: [Yes]
Justification: Experimental details have been provided in Apdx. E Guidelines:
The answer NA means that the paper does include experiments.
The experimental setting should be presented the core the paper to level of detail
that is necessary to appreciate the results and make sense of them.
15

---

The full details can be 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 deterministic the benchmarks, and no error bars need to be provided.
Guidelines:
The answer NA means that the paper does include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, at least for the experiments that support 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, overall
run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call a library function, bootstrap, etc.)
The assumptions made should given (e.g.. Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
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 not to show in tables or figures symmetric error bars that would yield results that out of range (e.g. negative eтror rates).
If error bars are reported in tables or plots, The authors should explain in 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 com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification: Detailed hardware resources are provided in and Apdx. Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU 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 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 failed experiments that didn't make into the paper).
9. Code ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics
Answer: [Yes]
Justification:
We have acknowledged the NeurIPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
16

---

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: They have been discussed in 35
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 or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g.. deploymentt of technologics 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 partieular applications, let alone deployments. However, if there is direct path any negative applications, the authors should point it out. For example, it is legitimate point that 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 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 technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Question:
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)?
Answer: [NA]
Justification: No data or models are 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 or 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 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
Question: 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?
17

---

Answer: [Yes]
We cited both a-3-CRWN and NeuralSAT, and libraries used for experimental evaluation.
Justification:
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version asset used and, 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.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode. com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re- re-packaged, both the original license and the license of the derived asset (if has changed) should be provided.
this information is not available online, the authors are encouraged to reach out to the asset'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 assets 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/model part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing 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 paper does 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 the main paper.
According to the NeurIPS Code Ethics, workers involved in data collection, curation, other labor should be paid at least the minimum wage in the country of the data collector.
Institutional review board (IRB) approvals or equivalent for research with human subjects
18

---

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 on the requirements of your country or 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 nor research with
human subjects.
Depending on 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.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors to adhere to 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
Question: Does the paper describe the usage of LLMs if it is important, original, or non-standard component of the core methods this research? Note that the LLM used only for writing, editing, or formatting purposes and does not impact the core methodology. scientific rigorousness, or originality of the research, declaration is not required.
Answer: [NA]
Justification: LLM only used for revising writing and suggesting words.
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 policy (ttpss//eeurr..coooommeeeee/e/// for what should or should not be described.
19

---

A DNN Properties
For neural network, . Rº + RR specifications of functional properties constrain the output of N based on its input. Specifying such necessary conditions for DNN input-output relations is topic of great interest with applications test oracles in DNN testing 335
training objectives to maximize [36], and biasing generative models to produce outputs that conform property [37]. broad class of properties can be formulated using pairs of half-space polytopes each specified as the conjunction of cutting planes where one set defines the pre-condition, Pin. and another the post-condition, Poout A variety of different properties can formulated using such pre-post condition pairs but we focus two popular classes of properties below.
network property conformance
Classification Robustness
A well-studied class of properties express local robustness properties of
the form:
dp E [0,c]:N(<>) = NNx p),
where is specific seed input, often chosen from the held out test dataset. These express that network inference is invariant for perturbations within the convex e-ball, x = p, for the seed input. A variant of this, with post-condition of the form [[V(x) - (x = p)ll s can be defined for regression networks.
Reconstruction Robustness Generative models are formulated as neural networks, N R + R" and are trained to approximate the identify function [38 39). For such, models one can adapt the regression robustness property above, to define local reconstruction robustness property of the form:
Vp E [0,c] [= + - 21100 S 3,
for seed input The 8 parameter expresses the expected agreement between input and its reconstruction.
B Correctness Proofs of CoVeNN
Let. E" + R denote neural network, and let din (2) and @ouc(y) be input and output property of interest, respectively. The global verification objective is to prove:
Vx E R" din (x)
@ouc(N(x))
Chain of Proofs. Given N, decompose into K sequential subnetworks: N NR o N ... Ni, where each N& Rdd-1 - IRd with do = n and dx m.
Let no din and YKK douti seek to synthesize K intermediate predicates (assumptions) "....., "i....,7K- -K-1 over intermediate network states.
Following the classical assume-guaa guarantee (sequential composition) proof principle, the global property entailed by the following chain of K local obligations:
Vk 1,...,K K
(7 nk)
(4)
If all these obligations hold, we have:
V (Nk-1,
(Dins Dout)
(5)
Thus global verification is reduced to a finite sequence of smaller verification problems.
Automated Synthesis of Intermediate Assumptions. Given subnetwork N input constraint Tins an overapproximate output bound Tover = (Toonrr, Uover); ), number of neurons P, and scale factor F [0, 1J, synthesize the candidate assumption "assume follows.
First, CoVeNN computes the sampled output region by solving:
Lisample
min N& (z)
U Usample max Nx(x)
(6)
ze
20

---

where each minimization and maximization is performed through backpropagation.
Next, CoVeNN interpolates between the overapproximate and sampled bounds to obtain:
Lint Lsample F- (Leample- - Lover) Vint = F. (Uones - -Usapple) + Usampte
Let Select Lint, Uint: P) denote selection of P neuron indices for which the interval [Line[e], Unn [i]] is top-P largest. The synthesized assumption Yassume for No is then the set of inequalities:
Yassume -xx: y,
S Uillli e Delect(Lins. Unnt PI}
Linel],,
(8)
where Y; denotes the i-th output of N
Iterative Refinement. For each refinement round r. and for each subnetwork (i -i= LK. -)),,
let the current overapproximate bound for its output be denoted by (L _,!T)). Given assumption Tassume (constructed as above) and the formally verified lowerbounds extracted from the underlying verifier, consider all neurons selected for tightening. For each such with assumption direction ("22" or "<") and associated right-hand side rhs, let 1j be the corresponding lower bound from lb. The refined bounds are updated by:
L 1(+1 [1] = rhs + ly. if direction is "Z"
rhs - 4, if direction is "<"
D(+tD =
T otherwise
U []. otherwise
All other coordinates are left unchanged. The updated tuple (L(*+1) -.(+tt) forms the new tightened overapproximation for the next refinement round, and subsequent rounds proceed analogously unless the verification succeeds or the allowed number of rounds is exhausted.
B.1 Chain of Proofs
Thm. (Compositional Verification via Guaunn-ee Reasoning) Given a neural network N E + R.T decomposed into K subnetworks such that N N k a o N,,, a property oin + @out, and intermediate predicates ?1..... .......K-11. where "fo = Φin and 7/K Pout. the global specification holds whenever every local property is valid:
A (0 (n.-1.Nk:71l
(Bm, Pout)
Proof. Let = NK o.... o N1 denote the decomposition into K composed subnetworks. Let the intermediate predicates be yo, ....., 7K with "io = Pin and уK = Pout- We are given that for every h: = 1,.... K,
Vz E 1 76-1(2) = (N)))²)))
(TK-1, 7ik)
or
We show that:
Vx R" (z)(2) Doue (N()))
(Din, dout))
Let x E I." such that (in(x) holds. That is, (z(x).
Base (I 1): By the first obligation, (0(x)) (Wii(z)) so (21)) holds for 21 = (z).
Induction step: Assume for some < l K that 7k- 7k-1 (2x-1) holds for some 2 Then, by the k-th obligation, 7x (>((==1)) holds for N
By unrolling, starting from 70(x), we obtain via repeated application:
(=1), 72(22), .... (x(=x), where =1. -N 1); 20 In this case, zх (-NK----Wi = (xx) and (x(2)) means dont (N(()) Therefore, for any satisfying din(2)) we have dont (N)))) That is,
Vx (x)(x) = Dont (N()))
Thus, the global specification holds.
21

---

Alg. 2: Generate assumptions.
input :DNN N, input property Yin, overapproximation "Yover, number of neurons P. and scale factor output :Assumptions "asssue
(Lover, Uover) t- Yover
Luample Minimize (6x) ) minimize output N samples from "iin
Usample f- Maximize (e Mnn) // naximize output of N for samples from Tii Lint & Liaample F sammlle Lawer) // interpolate output lower bounds of W Uint F. (Uover U sample) ) Usample // interpolate output upper bounda of
JaaRume - []
for i Select(Tint Uine: P) do select top-P
Yassume dassume-append(( Lint 2)) // tighten asaumption Line Vaasume Yoxxameeepperdl Unnt [i 5) // tighten assumption S (ca[ii]
10 return Yassume
B.2 Soundness of Iterative Bound Refinement
Thm. (Soundness of Iterative Bound Refinement) Suppose the base verifter V soundly establishes, for a neuron Y,, right-hand side rhs, a direction E (2.5), and a corresponding verifier bound (where 8 ffr "z" and for "S"), that Y; rhs $ 8. Then, the refined inequality
Y, x (rhs 5)
soundly verified. Therefore, updating the right-hand side to rhs + 8 yields an assumption formally verified by V.
Proof. Consider the case when the direction is "2" The assumption being verified takes the form Y, 2 rhs (line 14). V soundly verifies that Y; rhs 6, where 5 = li and 5 < 0. This implies Y; 2 rhs + Therefore, to ensure this assumption is valid, we update the right-hand side to rhs + (line 15). confirming Y; rhs + holds. Similarly, dual of this process is used refine the upper bounds. In both cases, replacing the original bound rhs with rhs - yields an assumption that is formally validated by the verifier. Thus, the refinement procedure produces sound bounds.
This theorem formalizes the soundness of our bound refinement procedure, which is critical component of our iterative assumption generation. Specifically, it ensures that each refinement step, guided by the verifier's output, always results in bounds that are formally valid, thereby guaranteeing that the iterative tightening of assumptions preserves correctness throughout the verification chain.
B.3 Soundness of CoVeNN
(Soundness of CoVellt) Let N be neural network and than Dont be input/output properties such that CoVeNN verifies N satisfies diin = Dout- Assume all local subproblems are formally
Thm. 3
verified by sound underlying verifier V or formally refined as Thm. 2 Then N indeed satisfies
din Dout.
Proof. Follow the arguments in BB.1 for any with din (x), have
Din( (x) m (x)
(2((2(W _ ... (ove(N(x)))
Thus, A satisfies tinn = Dout- The correctness of CoVeNN is thus relative the soundness of the underlying verifier: if the verifier establishes each local property, then the global specification holds.
The algorithm terminates because only finitely many refinement rounds are permitted for each 7 However, completeness is not guaranteed: the verifier may fail to establish some obligations or the refinement limit may be reached, in which case CoVeNN may output unknown.
22

---

C Constructing Assumptions
We seek to automate the generation of assumptions for the second obligation in InE.q. 1, T, by adapting the verification of the first rule to approximate them. Alg. 2 outllnees systematic method to estimate and construct these assumptions. We use 7 to denote the values of intermediate steps in the process of computing / 7ox is the assumption for N, and Tassume is the computed assumption for the subsequent network. The underlying verifier is able to compute a sound overapproximation of a given subnetwork's 'ssee output for Yin- which we denote with "over- These bounds, (Lovers Uover): are often too imprecise to allow verification of the overall problem.
We construct tighter assumptions, Yassume. by interpolating between the overapproximation and space defined by sampling the behavior of N Fig. 26 2bjittustsss three distinct types of regions. The solid red line represents the actual operational region of a hidden ReLU within DNN. Due to the inherent non-linearity of DNNs, calculating this exact region for hidden neurons is computationally infeasible. Instead, verification processes commonly use sound overapproximations to capture the behavior of each neuron, such as the triangular area bounded by (Lover. Uover). However, this introduces imprecision which accumulate during verification of the layers of DNN.
We compute sampling region by minimizing (maximizing) the output of for a set of sample inputs from Tin (line 2 line 3). This process uses backpropagation which requires that the minimization and maximization be performed separately 40). These samples offer tighter, more realistic representation of the network output bounds by considering adversarial conditions. The sampled region, aamppee, U ). is likely to disprove subsequent verification sub-problems, since there is high probability of counterexamples existing close to these bounds Laaple and U Usample. To mitigate this risk, we compute an interpolated region, (Lint: Uint), between the sampled region and the overapproximation (line 4 line 5): the degree of interpolation can be controlled by F.
Rather than attempt to prove the full hypercube of an assumption, modern DNN verifiers 19 I0 have been engineered to prove subsets of clauses of the DNF encoding of the negation of the assumption this is significantly faster in practice. We select the P' neurons with the largest interval size as determined by sampling to tighten (line 7). Selected constraints are then tightened by using the upper/lower bounds from Yint (line line 9p. Selective tightening allows us to mitigate the cost of downstream verification, since after the initial verification pass, only assumptions for tightened neurons need to be re-verified.
D Related Work
SoTA tools in DNN verification, such as those evaluated in VNN-COMP, integrating multiple techniques to improve scalability and efficiency. Leading verifiers, including NeuralSAT [24 [0] and a,3-CROWN 19 g split problems into smaller subproblems and refine bounds on subprob- lems. NeuralSAT and a--CROWN leverage GPU-accelerated linear bound propagation alongside advanced BaB techniques, such as cutting planes and neuron stabilizing, to handle harder networks. Marabou M encodes verification constraint problems and employs parallelized split-and-conquee strategies to improve scalability. nnenum [12 achieves impressive performance on low dimensional networks using star sets and zonotope abstractions. CoVeNN can be viewed as a meta-verifier that decompose large verification problems into smaller subproblems, and leverage these existing SoTA verifiers to solve them.
There are two notable prior works addressing on compositional verification of DNNs. Ivanov et al. 24 introduces a compositional framework to break high-level task into subtasks or subcom- ponents, such as breaking down car navigation task into track segment, each representing a distinct system mode (c.g., going straight turning). Unlike CoVeNN, which focuses on decomposing the DNN itself, this work decomposes the task that may rely on DNNs.
Prophecy 22 uses an expensive decision tree algorithm to infer intermediate specifications. Their approach (1) is exponentially with the number of neurons, (2) records only activation patterns for ReLUs at one single layer (layer pattern) which is selected by hand, (3) does not support iterative refinements, and (4) and depends on training data. CoVeNN addresses these by inferring specifications by recording computed bounds for neurons which (1) scales along with DNN verifier algorichms, (2) records richer intermediate specifications that record ranges of activation palues-which essential for handling non- activations and automatically infers decompositions, (3) allows intermediate
23

---

specifications to be refined based on the property being checked, and (4) does not require training data. Lastly, Prophecy explicitly does not support Resnet and reports results on a few samples of small networks (e.g., ACAS Xu) which are not representative of modern DNNs
E More Details on Experiments
E.1 Experimental Setup, Solver Selection, and Benchmarks
Setup Our experiments are conducted on desktop with an AMD Ryzen Threadripper PRO 5975WX 32-Core, 128 GB RAM, and an NVIDIA GeForce RTX 4090 GPU with 24 GB VRAM. Our implementation is based on the open-source NeuralSAT verifie with decomposition related code added. For RQI and RQ2, NeuralSAT was used as the backend verifier, while both a-3-ROWN and NeuralSAT were used in RQ3. Timeout for single instance is set 3600 seconds. The maximum number of rounds r is set to 4. Note that these parameters can be changed easily by CoVeNN's user.
Underlying Solver Selection We tried several CPU-based verifiers, such nnenum [2 and Marabou [TT]. but none of them could solve any instance of the benchmarks and their results would be all "_" if added to Tab. 2 In addition, with instances that they got OOM errors and they all ended up being killed by the operating system or took more than 30 minutes even for single abstraction pass. This is not surprising as our work is explicitly designed to solve problems that are beyond what can be solved by current NNV tools.
also tried running o:3- 0-3-CROWN and NeuralSAT CPU
Benchmark Selection The VNN-COMP benchmark suite is a useful starting point, but prior notes that its benchmarks are often too easy for best verifiers. Our goal is to find benchmarks that go beyond what can be solved. We approached this from two directions: (1) scaling an existing VNN-COMP benchmark and (2) introducing a new challenging benchmark family.
work 13 41
Most VNN-COMP benchmarks lack clear path for scaling, but the ResNet benchmark is an exception: increasing the number residual blocks aligns with real-world models like DroNet 42] (2)]. We used this scaling strategy, adapting the training setup from Pytorch Image Models (timm)
and ResNet- 152
To complement ResNet, we added new benchmark family based on variational autoencoders (VAEs), which are naturally decomposable at their latent bottleneck layer. We adapted the encoder/decoder from Stable Diffusior reduced its complexity for tool compatibility, and trained it on CIFARIO using the simplified version of the original training code.
Memory Usage We use information reported by CUDA to compute memory consumption, which represents the total memory demand/available memory. When the verifier attempts to allocate more memory than the system could provide, this exceeds 100% and causes OOM. In particular, we extract memory metrics: current memory usage (memcar)) free memory (memfree)) and memory requested for the operation that caused the OOM (memreeg). The memory usage calculation is:
(mem + memreg mrmfrre)
mcMussge
(10)
meMootal
E.2 Model architectures
We summarize the model structures in experiments in Tab. 3
Let Conv(a, b, c) be conven- tional convolutional layer with a input channel, b output channels and kernel size of c x Let ConeTranna, b, c) be a transposed convolutional layer with a input channel, b output channels and a kernel size of è x The stride and padding sizes are intentionally omitted for simplicity. Let Lin(a, b, c) be fully-connected layer with a input features and output features. Let Resckl,k b) stands for a residual block that has a imput channels and b output channels. A Block is comprised of paths, where the main path contains Conv and the residual path contains I Conv, All networks use ReL.U activation only.
Torch Pyrrch
24

---

Tab. Model architectures used in experiments.
Network
Architecture
Params
Encoder: Cone(3, 8),), ResBBock(8, 8), Cone(8, 8,4) ReaBlock(S, 8), Cone(8, 1,33, Conv(1, 1,1)
VAE_ BASE
Docdder: C1nne 1), Conu((, 8,3), RexBloock(S, Cons/rant8, 4), ReaBlock(S, 8), Conv(8, 3.33
10K
Encoler: Cone( 16, 3), ResBBock(16. 16). Cons(16, 16, 4), (esSBoock(,,, 16). Conv(16, 1,3), Cone(1, 1,
VAE, WIDE
Decoder: Cone(L, 1, 1), Conu(1, 1), ReaBlock(16, 16), Conc1 16, 4). ResBlock(16, 16), C1,
39K
Encoder: Cone(3, 3), ReaBlock(S. 8), Conu(8, 4), RexBlook(8 8)
Conn(8, 1,3), Come(I, 1,1)
WEE
15K
Dasader: Cone(), 1, 1), Conu() (1, 8,3). (RssBlock( 8), Cowe/Trann.. 8.44)
ResBlookk(, 8), Cone(8,3,
RESNET6
Conur(3 16, 3), Rea B1, 32), 05 x ReaBlock(32. (32, 32). Lan(32, 10)
113K
RESNET12
Cono(3, 16, 3), ResBBookk 32), RosBloock (12. 32). Lan(32
230K
RESNETI8
Cono(3. (3, 16, 3). 116 32),
Rea 32, 32), Lin(32,10)
348K
RESNET36
Cono( 16, 3), Rea (10 32), 35 x Rea ReaBlook 32). Lan[32, 10)
206K
Tab. 4: Number of completed jobs for each verifier (verified, unknown); " means that the verifier aborted with an OOM error on all 10 properties.
#Blocks
a--CRRWN
NeuralSAT
CoVeNNNs
(6, 4)
(6, 4)
(6, 4)
(5, 5)
(5, 5)
(5, 5)
(8, 2)
(9, I)
(9, 1)
(7,3)
(8.2)
36
(6, 4)
E.3 Tools Scalability
Tools' scalability of the two top performing verifiers in VNN-COMP'24 a,3-CROWN and NeuralSAT, and CoVeNN on ResNet-based instances is shown in Tab. 4 Number of completed jobs for each verifier (verified, unknown) where "_" means that the verifier aborted with an OOM error on all 10 properties.
As detailed Tab. 4 CoVeNN matches the ability of underlying verifiers on problems for which they complete and the refinement strategies allow it to prove properties when scaling to much larger networks.
25


Reviews:
[{"review_id": "pU9GDfVZH9", "reviewer": "Reviewer_qN2F", "summary": "The paper proposes CoVeNN, a methodology for the compositional verification of neural networks.\nThe approach first decomposes a neural network into multiple blocks and then verifies these blocks individually\nin an assume-guarantee manner. If a property is not verifiable, the approach refines the intermediate assumptions\nto achieve verification.\nTo this end, a number of heuristics are proposed.", "questions": "- **(O1)** Regarding (O1): The coarse over-approximation certainly provides guarantees for a much wider part of the input space than what is verified for a given robustness property.\n\t\t  Have you inspected the inner contracts? Maybe they could be reused? Especially for image NNs it is also conceivable,\n\t\t  that it might be possible to derive some interpretable information from them (something like if these nodes are in range [l,u] the NN is recognizing a wheel of a car)\n- **(O2)** It is commonly believed that the internal representations of ResNets and VAEs correspond to higher-level features of the provided inputs (e.g. image components) which seems to be\n  particularly well suited for compositional verification. Have you made any observations in this direction? Do you expect this approach to work equally well for other NN architectures?\n- **(O3)** On a more practical level: Do you have any indication whether compositional verification works so well \"only\" because it yields significant memory savings\n  (i.e. given larger RAM NeuralSat could solve the same problem) or does it also provide a significant benefit in terms of computation time (i.e. even with more memory NeuralSAT would be much slower)?", "limitations": "yes", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 4, "significance": 4, "originality": 4, "strengths_and_weaknesses": "**Strengths:**\n- **(S10)**\tThe novel, innovative approach convincingly demonstrates that compositional verification for neural networks is A) achievable\n\t\tand B) increases the scale of NNs that can be processed. \n- **(S20)**\tThe approach is agnostic to the underlying verifier and can thus scale as NN verification technology develops further.\n\t\tThis is particularly exciting, because it hints at the fact that speedups from further improvements in NN verification technology\n\t\tmight multiply with the speedups achievable via decomposition (rather than these effects cancelling each other out).\n- **(S30)**\tThe evaluation demonstrates that the approach can solve problems that are much larger than what the current State of the Art can achieve.\n- **(S40)**\tThe paper does a good job explaining the approach and provides helpful illustrations and examples.\n\t\t\n\n**Minor Opportunities for Improvement:**\n- **(O1)**\tI am under the impression that work on shared certificates in NN verification [A] is another related technique that might warrant discussion in Appendix D.\n\t\tWhile the approach has a slightly different objective (reusing contracts for verification of other properties), it also leverages assume-guarantee reasoning about intermediate values.\n\t\tMoreover, it might be interesting to combine these techniques in future work: Maybe derived guarantees about intermediate blocks by COVeNN could equally be reused for other (robustness) properties?\n- **(O2)**\tThe approach's performance is still dependent on a number of hyperparameters which must be tuned correctly. However, this is also transparently discussed by the authors.\n\t\tWhile this is a limitation of the appraoch at the current stage, I believe the major contribution of the paper is to demonstrate how compositional verification can, in general, be achieved.\n\t\tThis contribution is not lessened by the need for more engineering concerning these hyperparameters.\n\n**Minor:**\n- Line 82f: Typo in the formula: I belive it should read $\\max\\left( [...] \\cdot v_{i-1,k} [...] \\right)$ (replace j with k)\n- Line 210: The text seems to indicate, that the interpolation is happening with $s=0.5$, but the numbers of $\\gamma_1'$ do not seem to match a 0.5 interpolation between $\\gamma_1$ and $\\sigma_1$.\n- Line 262: \"none of them are sat\" -- is it known that the unknown benchmarks are unsatisfiable or do we simply not know their status yet, because no tool solved them so far?\n\n[A] Fischer, Marc, et al. \"Shared certificates for neural network verification.\" International Conference on Computer Aided Verification. Cham: Springer International Publishing, 2022.", "was_revised": true, "final_justification": "Overall, I find this paper to be novel, interesting, and a step forward in handling memory-intensive verification tasks.\nI found the authors' answers to be satisfactory and hence strongly believe this paper should be accepted for the reasons outlined in my review above.\nIn particular, I believe there are good reasons why the paper does not evaluate on VNN COMP benchmarks as outlined in the rebuttal to GNvQ.\nMoreover, verification of recursive architectures is a highly complex topic of its own, and I view this approach as significant independently of whether it can be generalized to such architectures (although the authors even claim it can be extended in this direction in the rebuttal to  2aSz).", "rebuttal": "Thank you for the encouraging review and thoughtful comments. Please find our responses below.\n\n1. Reuse intermediate assumptions and interpretability\n\nIndeed the computed over-approximation can be reused, and we exploited a bit of that in our implementation (for the same precondition but different postconditions, e.g., a robustness property on an image with the same input constraints but different output specifications like disjunctions over multiple output classes, we avoid recomputing intermediate bounds). We haven’t explored more general cases as you suggested and will do so in future work,  e.g., after verifying a property with intermediate bounds [l, u] at a given layer, these verified contracts can be cached and reused for future verification tasks where the intermediate bounds are subsets of [l, u], providing significant computational savings.\n\nWhile we haven't considered interpretability to date, your question suggests an approach as follows. For image classification networks like ResNets, the intermediate bounds computed by CoVeNN at different layers could potentially correspond to semantic features (e.g., edges, textures, object parts). The compositional nature of our approach naturally aligns with the hierarchical feature learning in CNNs, where early layers capture low-level features and deeper layers capture high-level semantic concepts. By inspecting these intermediate contracts, perhaps using concept activations, we could potentially gain insights into which feature representations are being verified.\n\n\n2. Internal representation of ResNets/VAEs well-suited for decomposition\n\nYes, we observe that for VAEs, the bottleneck layers create natural bottlenecks where intermediate assumptions can be compactly represented, leading to more effective decomposition. For ResNets, however, the observation is not as clear due to their large internal dimensions (32x32x32) which requires CoVeNN to select only a subset of neurons for refinement. Our current selection strategy depends solely on bound tightness, but selecting neurons using heuristics that reflect neuron-feature associations might improve solving capability further.\n\nWe expect CoVeNN to work well on other architectures, though the degree of benefit may vary. In particular, Diffusion Models (or unrolled RNNs) where a model is executed in K steps,  CoVeNN would be able to decompose the problem where existing verifiers might not be able to handle large K.\n\n\n3. Improve solving time\n\nCoVeNN works well primarily because of memory savings and might not improve solving time. When the underlying verifier can successfully solve a problem, decomposition is less useful because it would introduce overhead in decomposition, refinement, and multiple rounds of verification"}, {"review_id": "CPJXolXiaj", "reviewer": "Reviewer_2aSz", "summary": "This paper introduces CoVeNN, a framework for verifying DNNs using assume-guarantee compositional reasoning. CoVeNN decomposes large networks into smaller subnetworks, verifies them independently with an off-the-shelf verifier, and composes the results to establish the property for the whole network. The framework includes an iterative refinement strategy that tightens assumptions to reduce overapproximation. Experiments on VAE and ResNet benchmarks show that CoVeNN can verify significantly larger networks than sotaf verifiers, solving 6–7 times more properties without running into GPU memory issues.", "questions": "- The decomposition strategy assumes linear, sequential splits. How would CoVeNN handle non-linear topologies like RNN?\n\n- The refinement loop is heuristic and may return unknown if bounds don’t converge. Is there any theoretical or empirical guarantee that refinement will succeed within the allowed rounds? If not, how can users avoid wasted compute?\n\n- The paper relies on heuristics for cuts, neuron selection, and scaling factors. How robust is CoVeNN to poor hyperparameter choices, and have you explored automated tuning?\n\n- The method depends on verifiers that assume piecewise-linear activations. How does CoVeNN generalise to networks with smooth or non-linear activations (e.g., GELU, tanh, sigmoid)? Does the soundness or refinement extend naturally to these cases?", "limitations": "Yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\n- Clear motivation: It’s a well-motivated practical problem, especially as DNNs continue to grow in depth and complexity.\n- Novelty: It introduces compositional techniques, specifically, assume-guarantee reasoning from formal verification, and adapts them for DNN verification. While the way of using assume-guarantee reasoning is standard as in formal verification, its application here in a concrete, verifier-independent manner appears for DNN, to the best of my knowledge, to be a first.\n- Strong empirical evidence: The experiments show that CoVeNN can verify significantly larger networks than the standalone underlying verifiers can.\n\n\nWeaknesses:\n- Limited adaptability to more complex architectures: The proposed decomposition assumes a mostly sequential, acyclic structure and may not naturally extend to models like transformers, RNNs, or GNNs, where the computation graph can be inherently cyclic or non-linear. For example, how would the decomposition handle genuine cyclic dependencies in RNNs, where the hidden state feeds back recursively?\n- No guarantees for refinement convergence: The iterative refinement loop is heuristic and may fail to converge. The paper does not provide strong theoretical or empirical guarantees explaining when or why convergence will succeed within the allowed rounds.", "was_revised": true, "final_justification": "The authors responses and clarifications, both to myself and to the other reviewers, have satisfactorily addressed the concerns and questions I had regarding the paper.  Therefore, I lean towards acceptance.", "rebuttal": "Thank you for your time and thoughtful comments. Please find our responses below.\n\n1. Handling non-linear topologies like RNN\n\nThe sequential composition we describe in the paper is one common case, but the framework supports more complex acyclic topologies by finding appropriate \"cuts\" in that graph. For RNNs, we believe CoVENN can handle them through unrolling, a common strategy in software verification. By fixing the number of recurrent steps and unrolling the RNN into an equivalent feed-forward network, we can apply CoVeNN's decomposition strategy. Existing work in RNN verification (e.g., Verifying Recurrent Neural Networks using Invariant Inference - Yuval Jacoby et. al.) applies unrolling before verification. Interestingly, unrolled RNNs create very natural decomposition points after each unrolled timestep, making them well-suited for our compositional approach.\n\nFor more general cyclic computation graphs, handling cycles would require incorporating more sophisticated circular assume-guarantee proof rules (e.g., Automated circular assume-guarantee reasoning - KA Elkader et. al.).\n\n2. Refinement loop may return unknown \n\nIndeed the refinement can return unknown, and we do not believe there is any guarantee  that refinement will succeed within the allowed rounds. Currently, wasted computation does occur in our approach: after reaching the number of allowed rounds, the process will stop and return unknown. \n\nHowever, there could be empirical early stopping strategies to avoid wasted computation. For example, in VAEs where the dimension of decomposed layers is generally small, CoVeNN may refine assumptions of the same dimensions multiple times across rounds. If the refinement yields no improvement on any dimension, we can stop immediately since the current settings (timeout for verifying each assumption, etc.) won't allow CoVeNN to improve further.  We will try this in future work.  \n\n3. Parameter choices and automated tuning\n\nWe included the detailed ablation study of parameters on the appendix E.3.2, L289. The algorithm indeed is affected by neuron selection (P) and less sensitive to scaling factor (F).   We haven’t yet explored automated tuning.\n\n4. Non-linear activations (e.g., GELU, tanh, sigmoid)? \n\nCoVeNN, and in general DNN verification tools, are not limited to piecewise-linear activations and can handle smooth or non-linear activations, e.g., tanh, sigmoid, etc. The key insight is CoVeNN represents intermediate assumptions using interval bounds at the cut point rather than discrete neuron status (on/off), making it activation-agnostic. CoVeNN captures over-approximated lower and upper bounds for each neuron at intermediate layers, and these interval bounds remain valid regardless of the activation function used. When refining these bounds, the refined intervals remain over-approximated, ensuring soundness."}, {"review_id": "RJbJmhZsPk", "reviewer": "Reviewer_dCtJ", "summary": "This paper proposes a novel approach to mitigate the high memory consumption involved in verifying large neural networks. The method decomposes a single verification problem into a sequence of subproblems, each of which can be handled by an existing verifier with lower memory requirements. Empirical results show that the proposed technique enables the verification of larger network architectures while reducing overall memory usage.", "questions": "1. Why is the decomposition method not applied to disproving properties? I would be happy to raise my score if the authors can provide a clear justification. It would also be helpful to include this clarification in the main paper.\n2. Why does the memory usage exceed 100% in Figure 3b?", "limitations": "The limitations section does not mention the method’s inability to disprove properties, as noted in the Quality section.", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 3, "originality": 4, "strengths_and_weaknesses": "### Quality\nThe approach appears sound to me. The authors present correctness theorems along with proof sketches in the main paper, although I did not review the full proof provided in the appendix. The empirical results, particularly those in Table 2, clearly demonstrate the proposed method’s superior ability to handle large-scale neuron networks compared to existing state-of-the-art techniques. \n\nHowever, my primary concern is the limitation of this approach in disproving properties. The proposed method can only verify that a property holds, but it cannot refute a property by providing a counterexample. As a result, the empirical evaluation only focuses on networks with valid properties. This is a notable weakness compared to most existing verifiers, such as $\\alpha\\beta$-CROWN and NeuralSAT, which can produce counterexamples when a property does not hold.\n\n### Clarity\nThe paper is generally easy to follow. However, too many algorithmic details are deferred to the appendix. For instance, the roles of the input parameters P and F in Algorithm 1 are not clearly specified, and the generateAssumption function (line 10) lacks sufficient explanation. \nTo improve clarity, the authors could consider including more of these important implementation details in the main text. Given the page limit, this could be achieved by reducing the space of the formal correctness section, which, in my view, does not contribute significant theoretical results.\n\n### Significance\nThe improvement in verifying large neural networks with valid properties is compelling; however, the inability to disprove properties makes the proposed method incomplete.\n\n### Originality\nThis divide-and-conquer-based approach to neural network verification appears novel and promising. With further development, it has the potential to effectively address the issue of high memory consumption in neural network verification.", "was_revised": true, "final_justification": "The authors provide a justification and an idea for addressing the incompleteness of their current method. I am satisfied with their response and have increased my score accordingly.", "rebuttal": "Thank you for your time and thoughtful comments. Please find our responses below. \n\n1. Disproving properties\n\nThis is a thoughtful question. The short answer is that decomposition might be able to disprove properties, however we haven’t explored this direction because verifiers rarely have issues with disproving properties (their employed adversarial attacks are highly effective at finding counterexamples), and existing benchmarks from VNN-COMP contain virtually no SAT (disproving) cases that cause scalability issues, giving us no opportunity to evaluate compositional disproving. \n\nThat said, we anticipate that a challenge in using compositional disproving is due to the nature of over-approximation that favors verification over falsification.  Counterexamples computed from overapproximation may not be valid and require additional checking and refinement. That said, by answering this question, we came up with an idea for compositional disproving by adapting preimage methods (e.g., PREMAP: A Unifying PREiMage Approximation Framework for Neural Networks - Xiyue Zhang et. al.). These backward analysis techniques find under-approximations of inputs reachable to predefined output spaces. Starting from a violated output space, we could compute intermediate spaces reachable to that output space through backward analysis until reaching the input precondition. If the found preimage space is a subset of the precondition, we can confirm the violation.\n\n2. Memory usage exceeds 100%\n\nWe use information reported by CUDA to compute this, which represents the total memory demand / available memory.  When the verifier attempts to allocate more memory than the system could provide, this exceeds 100% and causes OOM.\n\nIn particular, we extract 3 memory metrics: current memory usage (mem_cur), free memory (mem_free), and memory requested for the operation that caused the OOM (mem_req). The memory usage calculation is:\n\nmem_usage = (mem_cur + mem_req - mem_free) / mem_total"}, {"review_id": "4ZLph5CC1d", "reviewer": "Reviewer_GNvQ", "summary": "The paper proposes a compositional neural network verification approach for reducing the memory load of existing verification algorithms. Therefore, the computation graph of a neural network is split into parts that are incrementally verified using intermediate assumptions derived from heuristics; the verification of each part ensures that its output entails the assumption of the successor part. The intermediate assumptions can be iteratively refined. The evaluation demonstrates that the proposed approach can improve state-of-the-art verification algorithms when the available memory is limited.", "questions": "- Does the approach have other benefits than reduced memory load for large neural networks?\n- How are the computation graphs of the neural networks decomposed? Could you please elaborate with an example?\n- How large is the conservatism introduced by the intermediate assumptions? How are the intermediate assumptions represented, e.g., using intervals?\n- Why are the evaluations only done on non-standard benchmarks? There are many instances in the VNN-COMP that are not solved, e.g., a-b-CROWN only solves 74.5% of the CIFAR100 benchmark?\n- How does the approach affect computation time?", "limitations": "yes", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\n- The paper is well-written and the approach is well explained. \n- Exploring how large networks can be verified is an interesting research direction.\n- The claimed improvement in memory efficiency is demonstrated in the evaluation. \n\nWeaknesses:\n- The related work section is very brief and should be extended.\n- The paper does not go into the details on the heuristics for splitting the computation graph of the neural networks. \n- The proposed approach only benefits the verification of large neural networks with limited memory.\n- The evaluation is done on non-standard benchmarks.", "was_revised": true, "final_justification": "While the topic of handling relatively large networks under memory constraints is interesting, the applied techniques do not seem novel to me. Paired with missing description on how the models as decomposed (via which heuristics?), leads me leaning towards reject although I can also see it being accepted.", "rebuttal": "Thank you for your critical evaluation. Please find our responses below.\n\n1. Other benefits than reduced memory\n\nBeyond memory savings, CoVeNN doesn't give many other benefits. However, as mentioned by reviewer qN2F, the intermediate bounds computed during decomposition can be reused for solving multiple objectives of the same problem or save computation across different verification tasks.\n\n2. Networks decomposition and example\n\nCoVeNN decomposes networks by identifying strategic \"cuts\" in the computation graph that divide the network into sequential subnetworks (Sect.3.1).\n\nConsider a network in our evaluation ResNet-36 with 110 layers. CoVeNN would decompose it as follows:\n- Subnetwork N_1: Input layer + first CNN + first 6 ResNet blocks\n    - Input: Original image constraints (robustness)\n    - Output assumption γ_1: Interval bounds on 32x32x32 feature maps\n- Subnetwork N_2: Next 6 ResNet blocks \n    - Input assumption: γ_1 (refined)\n    - Output assumption γ_2: Interval bounds on 32x32x32 feature maps\n- Subnetwork N_3: Final 24 ResNet blocks + classification head\n    - Input assumption: γ_2 (refined)\n    - Output: Final classification property (e.g., argmax(output) = true_label)\n\n3. Intermediate assumptions conservatism and representation\n\nThe conservatism (abstraction) varies based on network architecture, property being checked, and the refinement process.  Currently we use polytopes to compute bounds, and CoVeNN goes through refinement processes to tighten bounds.  \n\nYes, CoVeNN represents intermediate assumptions at the cut point using hyperrectangular interval bounds. CoVeNN can use other representations but we use intervals in this work for compatibility with underlying verifiers, which typically work with interval preconditions.\n\n4. Applied to VNN-COMP instances that cannot be solved\n\nThe VNN-COMP instances that tools such as a-b-CROWN cannot solve are not due to scalability (e.g., memory limited) but rather due to imprecise abstraction employed by the verifier. CoVeNN and decomposition in general won't be able to help as such problems are better solved with better abstraction and smarter branching/decision heuristics.  \n\n\n5. How does the approach affect computation time?\n\nCoVeNN first runs a verifier to solve the problem and only invokes decomposition if the verifier fails. Thus if no decomposition is required then the overhead is 0 and decomposition only incurs overhead when the problem cannot be solved monolithically."}]

Author rebuttal:

Meta-review: (a) Summary of Scientific Claims and Findings

The paper presents CoVeNN, a framework that applies compositional "assume-guarantee" reasoning to make neural network verification (NNV) scalable. By decomposing large networks into smaller parts and verifying them independently, CoVeNN primarily addresses the memory limitations of existing verifiers. The authors claim this approach dramatically extends the scale of verifiable networks. Their findings show that CoVeNN solved nearly 7 times more problems on large VAE and ResNet models than state-of-the-art verifiers, which frequently failed due to out-of-memory errors.

(b) Strengths of the Paper

The paper's primary strengths were consistently praised by reviewers:

1. It introduces a novel and groundbreaking application of compositional reasoning to NNV, tackling the critical challenge of scalability.

2. It provides strong empirical evidence of scaling verification to networks far larger than what current tools can handle, a major practical advancement.

3. The framework is modular and can be used with any underlying verifier, allowing it to benefit from future improvements in NNV technology.


4. The complex approach is well-explained and illustrated, making it easy to follow.

(c) Weaknesses of the Paper

Initial reviews identified several limitations:

1. The method can verify properties but cannot find counterexamples to disprove them, a key feature of existing verifiers.

2. The decomposition strategy is primarily designed for acyclic networks, raising questions about its applicability to models with recurrent or cyclic structures.

3. The framework's performance depends on heuristics and hyperparameter tuning, and its iterative refinement process lacks convergence guarantees.

(d) Reasons for Acceptance

Despite its limitations, the paper earned a consensus for acceptance. Reviewers were highly impressed by the authors' rebuttal, which satisfactorily addressed their main concerns. The paper's core contribution—demonstrating a viable path to scale NNV to previously intractable models—was considered groundbreaking and significant enough to outweigh the current weaknesses. The authors also proposed credible plans to address the limitations in future work, reinforcing the reviewers' positive final assessments.


(e) Summary of Discussion and Changes

The rebuttal period was highly effective and pivotal to the paper's acceptance. Key issues were successfully resolved:

1. The authors acknowledged this limitation and proposed a concrete future research direction using backward analysis to find counterexamples, satisfying the reviewer's concern.

2. They clarified that the method could handle RNNs by "unrolling" them into feed-forward networks, a standard practice that makes them suitable for the compositional approach.

3. The use of custom-scaled benchmarks was justified by the need to create problems that are challenging enough to show the limitations of existing verifiers, which was the paper's goal.

The authors' thorough and convincing responses led to multiple reviewers increasing their scores and solidifying their recommendations for acceptance.
Decision: Accept (spotlight)