Out of the Shadows: Exploring a Latent Space for Neural Network Verification
Authors: Lukas Koller
Tobias Ladner
Matthias Althoff
Venue: ICLR 2026 Poster (2026)
Keywords: Neural Network Verification
Zonotope
Set-Based Computing
Latent Space
Formal Methods
Primary area: alignment, fairness, safety, privacy, and societal considerations
TL;DR: We propose a novel input refinement procedure to speed up GPU-based branch-and-bound verification of neural network.

Abstract: Neural networks are ubiquitous. However, they are often sensitive to small input changes.
Hence, to prevent unexpected behavior in safety-critical applications, their formal verification -- a notoriously hard problem -- is necessary.
Many state-of-the-art verification algorithms use reachability analysis or abstract interpretation to enclose the set of possible outputs of a neural network.
Often, the verification is inconclusive due to the conservatism of the enclosure.
To address this problem, we propose a novel specification-driven input refinement procedure, i.e., we iteratively enclose the preimage of a neural network for all unsafe outputs to reduce the set of possible inputs to only enclose the unsafe ones. 
For that, we transfer output specifications to the input space by exploiting a latent space, which is an artifact of the propagation of a projection-based set representation through a neural network.
A projection-based set representation, e.g., a zonotope, is a "shadow" of a higher-dimensional set -- a latent space -- that does not change during a set propagation through a neural network.
Hence, the input set and the output enclosure are "shadows" of the same latent space that we can use to transfer constraints.
We present an efficient verification tool for neural networks that uses our iterative refinement to significantly reduce the number of subproblems in a branch-and-bound procedure.
Using zonotopes as a set representation, unlike many other state-of-the-art approaches, our approach can be realized by only using matrix operations, which enables a significant speed-up through efficient GPU acceleration.
We demonstrate that our tool achieves competitive performance compared to the top-ranking tools of the international neural network verification competition.

Published as a conference paper at ICLR 2026
OUT OF THE SHADOWS: EXPLORING A LATENT SPACE FOR NEURAL NETWORK VERIFICATION
Lukas Koller' Tobias Ladner'
Matthias Althoff'
'Technical University of Munich
Llukaskkoleee tobias. ladner, althoff)@tum.dd de
ABSTRACT
Neural networks are ubiquitous. However, they are often sensitive to small in- put changes. Hence, to prevent unexpected behavior in safety-critical applica- tions, their formal verification state-of-the-an verification algorithms use reachability analysis or abstract inter- pretation to enclose the set of possible outputs of neural network. Often, the verification is inconclusive due to the conservatism of the enclosure. To address this problem, we propose novel specification-driven input refinement procedure, i.c., we iteratively enclose the preimage of a neural network for all unsafe outputs reduce the set of possible inputs only enclose the unsafe ones. For that, we transfer output specifications to the input space by exploiting a latent space, which is an artifact of the propagation of a projection- based set representation through a neural network. A projection-basse based set representation, e.g., a zonotope, is a "shadow" of higher-dimensional set - latent space that does not change dur- ing set propagation through neural network. Hence, the input set and the output enclosure are "shadows" of the same latent space that we can use to transfer con- straints. We present efficient verification tool for neural networks that uses our iterative refinement to significantly reduce the number of subproblems in a branch- and-bound procedure. Using zonotopes set representation, unlike many other state-of- sfute-of-the-ase the-hharrt art approaches, our approach can be realized by only using matrix op- erations, which enables significant speed-up through efficient GPU acceleration. We demonstrate that our tool achieves competitive performance compared to the top-ranking tools of the international neural network verification competition.
notoriously hard problem is necessary. Many
INTRODUCTION
Neural networks perform exceptionally well across many complex tasks, e.g., object detection (Zou ett al., 2023) or protein structure prediction (Jumper et al., 202T). However, neural networks can be sensitive towards small input changes, e.g., often adversarial attacks provoke misclassifica- tions (Goodfellow et al.] (2015). Thus, neural networks must be formally verified to avoid unexpected behavior in safety-critical applications, e.g., autonomous driving (Chib & Singh 2023) airborne collision avoidance (Irfan et al. 2020). where the inputs can be influenced by sensor noise or external disturbances.
The goal of formal verification of neural networks is to find mathematical proof that every possible output for given input set safe with respect given specification; in this work, we demand that the output avoids an unsafe set. The verification problem is undecidable in the general case (Ivanov al.
2019) and NP-complete for neural networks with ReLt-activation functions (Katz et al.) 2017 Appendix I). Many prominent verification algorithms use reachability analysis or abstract in- terpretation to enclose the intersection of an unsafe set with the output of the neural network (Gehr et al.; 2018; Singh et al. 2019a) Xu et al. [021 Bak] 2021 Kochdumper et al.) 2023): The input set is represented using a continuous set representation (such as intervals or zonotopes), which is conservatively propagated through the layers of neural network to enclose all possible outputs. If the intersection of the output enclosure with an unsafe set is empty, the safety of the given input algorithms do not scale well to
set is formally verified. Out of the box, most reachability-base large neural networks with high-dimensional input spaces because the conservatism of the set prop- agation increases due to over-approximating nonlinearities in the neural network. Most verification

---

Published as a conference paper at ICLR 2026
algorithms reduce the conservatism by integrating branch-and- bouudd procedure to recursively split the verification problem into smaller and simpler subproblems, c.g., by exploiting the piecewise lin- earity of ReLU-activation function to reduce approximation errors (Bunel al. 2018) or splitting the input set to reduce its size. However, in the worst case, the verification problem is split into exponentially many subproblems, all of which must be verified.
In this paper, we speed up the formal verification of neural networks by iteratively refining the input set only enclose the unsafe inputs. Thereby, we reduce the size of the input number of splits and, ultimately, the number of subproblems to be verified. For our iterative input refinement, we exploit a latent space transfer the unsafe set backwards through the network from the output space to the input space for the enclosure of all unsafe inputs, i.c., we can discard all inputs that are already proven to safe. The latent space is an artifact of using projection- set representations, which represent the projection ("shadow") of nigher-dimensional set, e.g., zonotope is the "shadow" of higher-dimensional hypereube. The set propagation through a neural network only changes the "shadow", while the nigher-dimensional set remains unchanged. Hence, all considered sets are different "shadows" of the same higher-dimennional set, representing a latent space. Thus, to transfer the unsafe set from the output space to the input space, thereby refining the input set. Moreover, if cannot verify the safety of the neural network, can utilize the latent space to generate candidates for counterexamples. Ultimately, we propose a verification algorithm that integrates our novel iterative input refinement into a branch-and- and--ound procedure for verifying and falsifying neural networks. Further, unlike many other statc-of-the-ar verification algorithms,, we implement our verification algorithm using only matrix operations to take full advantage of batch- wise computations and GPU acceleration to simultaneously verify entire batches of subproblems.
reduce the
exploit the dependencies between the considered sets through the latent space
To summarize, our main contributions are:
A novel iterative specification-drives input refinement procedure speed up branch-and- bound neural network verification and falsification that exploits dependencies between the input and output space through latent space.
An efficient algorithm for neural network verification that takes full advantage of GPU acceleration by only using matrix operations and batch-wise computations.
An extensive evaluation and comparison with state-of-the-art neural network verifica- tion tools on benchmarks from the neural network verification competition 2024 (VNN- COMP'24) (Brix et al. 2024). Additionally, we conduct extensive ablation studies to jus- tify the design choices of our verification algorithm.
2 PRELIMINARIES
2.1 NOTATION
Lowercase letters denote vectors and uppercase letters denote matrices. We denote the i-th entry of a vector x by Fig) and the entry in the i-th row and the j-th column of matrix A Raxm by A(a))- The i-th row is written as Ag.) and the j-th column as A(-))- The identity matrix is denoted by I E Raxn, We write the matrix (with appropriate size) that contains only zeros or ones as 0 and 1. Given two matrices A mmxx= and B E m2x,,, their (horizontal) concatenation is denoted by [A B] E (m1x(()tn)) The operation Diag(e) returns a diagonal matrix with the entries of vector V on its diagonal, and the operation |A| takes the elementwise absolute value of matrix A E "m We denote sets by uppercase calligraphic letters. Given two sets SI, S2 C R we write their Minkowski sum as S1 ① S2 {s1 + 82 81 E S1, 82 E S2). For n E N, [n] = (1, 2, 2.....n) ..) is the set of all natural numbers up to n. The nnddimensional interval I C R." with bounds 1, E TR"
is written as I [g, ø]. where E [m]: Z(() S Z(z) For a function f: IR" + RT, we abbreviate the image of C R² with f(S) = (f(s) I S).
2.2 FRED- NEURAL NETWORKS
A (feed-forward) neural network Φ: R - R" is a sequence of k E N layers. Each layer applies an affine map (linear layer) an element-wise nonlinear activation function (nonlinear layer).
2

---

Published as a conference paper at ICLR 2026
(a) (Constrained) Zonotope
(b) (Constrained) Zonotope
"Shadow"
0.5
0
-0.5
-0.5
0.5
-0.5
0.5
0.5
0.5
constr: Zonotope Xlss
Samples æ E X'
constr. Hypercube B, n (C,
Figure 1: (a) An illustration of constrained zonotope and sample with its generators, (b) the same constrained zonotope as the "shadow" of constrained hypercube.
Definition 1 (Neural Network, (Bishop
2006 Sec. 5.1)). For an imput x E R the output of
neural network (xx) T
ho = I,
h4 I (hx-1) for [k]].
y hgg
where
Wx hi- by ifk-th layer is linear, (x((ux-) otherwise,
(hk-1))
with weights We x bias by E IRR,, and (element-wise) nonlinear function dn.
2.3 SET-BASED COMPUTING
A zonotope is a convex set representation popular in reachability analysis due to its favorable com- putational complexity (Singh et al. 2019b, Kochdumper et al., 2023). Definition 2 (Zonotope, (Girard G E Raxq, zonotope is defined as
2005 Def. 1)), Given center e E R." and generator matrix
={c c Σ G B
2 == G)
B BEI-1,
Subsequently, we define the set-based operations for zonotopes required for our verification algo- rithm. The Minkowski sum of zonotope computed by (Altholi 2010 Prop. 2.1 & Sec. 2.4)
G) R and an interval [g,
_ is
Z + (x.
(c - 1/2 (x + æ), IG diag(1/2 m)))
(1)
The image of zonotope Z (c. G) C R under affine map f: R. - Rm + W x +
with W mm and E I is computed by Allhhfff 2010 Sec. 2e4.2.4)
f(2)
Z = (W c b, W G)z-
(2)
Using an affine map, we can write a zonotope 2 = (c, G)z C Rn with g generators, i.e. E R=xq, as the projection of a g-dimensional (unit)-hypercube B, [-1, Z = c c G G. Thus, intuitively, zonotope is the "shadow" of higher-dimensional hypercube.
convex polytope is the intersection of finite number of halfspaces (Althoff 2010 Def. 2.1): we {x R Ax S b} R", where A x and R".
denote polytope by (A, b)
All zonotopes are convex and symmttiy However, by constraining the hypercube, we can represent arbitrary convex polytopes (Scott et al. 2016 Thm. 1).

---

Published as a conference paper at ICLR 2026
Definition (Constrained Zonotope, (Scott et al. 2016 Def. 3)). Given a zonotope Z (c. G) C R" with E R and E R=*", the zonotope with constraints C 3 S d. for 3 E Bg with C Rbxg and d RP. is defined
Zlosa = B 1-111 c3 = G (B, (C,d)
Compared to (Scott 2016 Def. 3), we use inequality constraints instead of equality constraints for convenience. Both types of constraints are equivalent and can he translated by introducing slack variables. Moreover, the considered set-based operations, i.e., Minkowski sum (T) and affine map (2) identical for zonotopes and constrained zonotope (Scott al. 2016 Prop. 1). Fig. illustrates a constrained zonotope as "shadow" of a constrained hypercube.
2.4 FORMAL VERIFICATION OF NEURAL NETWORKS
The output set neural network can be enclosed by conservatively propagating zonotope through the layers of the neural network.
Proposition (Set Propagation, (Ladner & Althoff 2023 Sec. 2.4)). Given a neural network
i: _0 + - and an input set & C. K" enclosure y enclose @2, X) C IR of the image y = (Xx) C y can be computed as
Hop X,
Hy enclose(Lg, HA-1) for [n]].
y H
The operation enclose L, H6- encloses the image of the k-th layer for the input set Ha-11 i.e. (2 S enclose (L. H1-1) (Ladner & Althoff, 2023 Prop. 2.14). If the k-th layer is We Ha-1 $ by: otherwise, the ac- tivation function Φx is enclosed with a linear function and corresponding approximation errors: enclose(Ly.
linear, an affine map is applied (2) enclose(L,, 1
diag(m)) H4-1 ① [x], where ma(a) is the approximation slope and (x(t): fx(e) the approximation error of the i-th neuron, with i [mx] (Koller et al. 2025 Sec. IV).
Hx-1) Hx-1)
Please note that Prop. I can handle arbitrary elementwise activation functrons (c.g., sigmoid or hy- berbolic tangent) and not limited ReLU-activations
2.5 PROBLEM STATEMENT
Given neural network Φ; no + R", input set X C 1 and an unsafe set U C R" our goal is to derive an efficient and practical algorithm that can either formally verify the safety of the neural network, i.e.,
(X') nu = 0.
(3)
or find counterexample, i.e.,
X such that ((x) E E.
(4)
3 SPECIFICATION-DRIVES INPUT REFINEMENT
A zonotope is the "shadow" of higher-dime dibbes-aimnsi hypercube (Fig. [D). The propagation of zonotope through the layers neural network transforms the projection of the hypercube, but the hypercube itself remains unchanged. Thus, all enclosed sets, i.e., the input, hidden, and output sets, are different "shadows" of the same hypercube. Therefore, the hypercube represents a latent space. Let us demonstrate the "shadow" view by example:
Example 1. Fig. 2 illustrates the propagation of two- two-dimensional input set X through a linear layer and a ReI.U-activation function, i.e., x +> ReLU(( 1/2 [ x (b]). Intuttively, the linear layer rotates the hypercube, and the nonlinear layer tilts it to compute the output set as its "shadow."
For input set X (0,2 1/2 I2) z, the hidden set Hi and the y are computed using Prop. 1
-1
1
1
-1]
Hi 2 1/2
1
x
+
0
0
1/2
1
(5)
[[]]
[0]
0
1
2
-2
0
y = diag
Hi +
7/4
1/2
1/2
1/4
:
1
4

---

Published as a conference paper at ICLR 2026
(a) Input Space
(b) Hidden Space
(c) Output Space
0
2
Zonotope His
Unsafe Set 24
Hypercube B3
Unsafe Outputs y nu
Figure 2: Illustrating the zonotope propagation through linear layer and nonlinear layer as "shadows" of the same hypereube: (a) The input set in the input space; (b) The output of the linear layer, which rotates and offsets the imput set; (c) The output of the nonlinear layer tilts the hypercube to add the approximation errors. Using the hypercube, the unsafe set (M) is transferred from the output space to the input space. Additionally, the hypercube split along a hyperplane exploit the piecewise linearity of the ReLU-activation function.
to
The approximation slope and errors for enclosing the output of the ReL.U-activation function computed using (Koller et al.) (2025] Prop. 10). For each input x E X and its corresponding output =+(I)= E V, we use the definition of a zonotope (Def. 2 to obtain B E [_11,]] such that
1/v2
1/2
-2/2 B(DD +
[
1/v2 ((2))
= 1/1
+
1/1
1/4
1/4 B(3)
(6)
The input and the output y are represented using the same factors ((2)) with an additional factor Big for the approximation error. We can unsafe set U(1) 3/2 formluate straints in Fig. 2 on the factors 3(())) of the input:
2(1) 3/2
6
1/2 -122) +0 2/22 = [-1/2
1/2
B(1))
-1/2.
(7)
=d
Therefore, we can use the constraints on B, Lee. C3 S d, to refine the input set to X X S X, which encloses all unsafe inputs. Analogoushy, we can split the set along hy 0 =
1/2 1/2] B((2)) I 0, for h1 E Hi, to exploit the piecewise linearity of the Reatiiictitooon function ( in Fig. 2
As example I demonstrates, we can constrain the input set with an unsafe set in the output space by exploiting the dependencies between the considered sets through the latent space. Prop formalizes an input refinement based on our observations.
Proposition 2 (Enclosing Unsafe Inputs). Given are neural network क: RR - RR an input
set X (Ca, Gz) C Thn with G. E x , and unsafe set U = (A, b) g C R Let
y = (Cy, Gy) enclose(#, be an enclosure of the output set with G, E R X9x, We enclose
all unsafe inputs by constraining X to Xlosa i.e..
{o E X ((x)) U} C &loss S X.
where == A AGG(GG and = b Acy + |AGg 1.
Proof. See Appendix
5

---

Published as a conference paper at ICLR 2026
(a) Input Space
(b) Output Space
0
-2
3
constr. Zonotope A'oas
Unsafe Set U
Output Set ((x)
Unsafe Outputs nu
Figure 3: Illustaaiion of an iterative refinement of the input set (Prop. 2 After the fourth iteration, the intersection with the unsafe set is empty, and the neural network verified.
We iteratively apply Prop. to refine the input set minimize the intersection of the computed output set and the unsafe set. During each iteration, we transfer the unsafe set from the output space to the input space to remove the parts of the input set that provably safe. Please note that input refinement only encloses all unsafe inputs and does not, in general, preserve an enclosure of the full output set. In Fig. 3 iterate Prop. 2 until the intersection of the output and the unsafe set is empty, and thus the problem is verified.
4 SET-BASED FALSIFICATION, VERIFICATION, AND INPUT REFINEMENT
For the fast and practical verification of neural networks, we integrate our novel input refine- ment (Prop. into branch-and-bouud procedure (Alg. [D. where we utilize the enclosed output set for verification, falsification, and input refinement. In each iteration, we perform the following com- putations: (i) The output set of the current input set enclosed (Prop. [ (ii) The intersection with the unsafe set is checked. (iii) If the intersection is non-empty, the verification is inconclusive, and falsification attempted. (iv) Finally, if we cannot verify the input set nor find counterexample, we split and refine the input set (Prop. 2 The subsequent subsections describe the steps of Alg. in detail.
Set-Based Verification We compute the output set y (Cyy Gy) C R. of the current input set using Prop. I and check if the intersection with the unsafe set (A,b), b) R with A Rex", is empty (Scott et al. 2016 Prop. 2):
3i [p]: A Co AA. Gyl b(g) = ynu 0.
Set-Based Falsification If we cannot verify the current input within it. For that, we utilize the latent space (Sec. 3 to identify the input for boundary point of the intersection of the enclosed output set and the unsafe set. For each normal vector of the unsafe set specification A(..) E "R. Lemma l):
try to find counterexample
, for E [p]. we compute a boundary point (Althoff & Frehsel 2016
B, = sign(A (Au.) Gy).
3= + GGy B
Finally, we check if the corresponding input 5 = + G. B((a)))) E X' in the input set X (cz, Gaiz with G2 x
x0 is counterexample, i.e., whether 4(T) E U.
Input Refinement and Splitting We reduce the conservatism of the zonotope propagation by splitting the input set before applying our input refinement (Prop. 2 The splitting is realized by

---

Published as a conference paper at ICLR 2026
Algorithm 1: Set-based verification algorithm. We store input sets in queue and use the oper-
ations ini initQueue, isNonEmpty, enqueue, and dequeue from (Knuth) 1997 Sec. 2.2.1)
Input:
Neural network Φ input set X' (Cz; Gz) 2 and unsafe set U (A, Output: Verification result, i.e., VERIFIED or FALSIFIED(i) with counterexample à E X
function verify X, K,2)
Q - initQueue (), q.enqueue
1/ Initialize queue counter. Add the initial Input set.
while Q.isNoonEmpty( do
X; - (.dequeue()
// Get the next input set. // Soclose the output iProp.
V < enclose Φ X;)
if y nu 0 then
// 1, Verificstion
continue
11 Verified input set.
else
// 2. Folsification Hj t Cr + Ga (((au) for B, sign(A(i.) Gy) 1/ Generate adversarial) 1nput
Y: t F(x)
// Compute the adversorial output (Daf.
11
if UJ E EU then
return FALSIFIE(EE))
// Found unsaCe input.
14
else
11 3. Refinement Splittion
C, < Compute the constraints for the input set. Xlc..d...... &lc.,44 + Split the input set. ennquee (xl X.ccesa)
Prop.
16
11 Scott et al. 2018 Prop. 3)
// Add sets to the queue. // Increment the counter.
+ii11
19
end
20
end
21
end
22
return VERIFIED
1/ Queue is empty? verified ell input sets.
adding constraints to the hypercube (Scott et al. 2016 Prop. 3); e.g., we can split the input set or we can formulate constraints that exploit the piecewise linearity of the U-Lttvativttiin func- tion (M in Fig. 2). For each split, we heuristically select dimension or neuron by comparing gradients w.r.t. a zonotope norm of the output set (Appendix
5 EVALUATION
We have implemented our verification algorithm in MATLAB part of the CORA toolbox (Althoff) 2015). To make our evaluation as transparent and reproducible as possible, we compare our tool on
benchmarks from the neural network verification competition 2024 (VNN-COMP'24 (Brix et al.
2024 with the top-5 tools of the competition: a-3-CROWN (Wang et al. 2021), NeuralSAT (Duong
al.
2023). PyRat (Lemesle et al., 2024). Marabou (Wu et al. 20024) and nnenum (Bak 2021).
Tab. presents the results for 8 competitive and standardized benchmarks of the VNN- COMP'2 24 (Brix al., 2024]. Please see Appendix A for details. Across all benchmarks, verification algorithm achieves competitive performance, even matching the top performance in four benchmarks.
5.1 ABLATION STUDIES
run extensive ablation studies to justify the different design choices of our algorithm.
Input Refinement We evaluate the verification improvement and per-iteration overhead of our in- put refinement (Tab. 2. Therefore, (i) we compare the number of subproblems required for verifying or falsifying instances with (V) and without (X) our input refinement enabled: We observe that our refinement reduces the number of subproblems by 59.6% for acasxu and 65.3% for safenlp.
(ii) Further, while the per-iteration time is larger with our input refinement, the maximum verifica- tion time is reduced by 53.5% for exu and 37.7% for sa fen

---

Published as a conference paper at ICLR 2026
Table 1:
Main Results [%Solved t (#Verified / #Falsified)), where %Solved is the percentage of solved instances (verified or falsified), with counts shown in parentheses.
Tool
acsax0
collins
coma
dist
lizear
mete.
sa P
tilveriey -bench
-rtl-onn
-tiff
-i zenn
-room
99.5%
100.0%
81.1%
98.6%
100.0% 97.0%
89.2% (311 / 652)
100.0%
CORA (Ours)
(138 /47)
(30 32)
(18 128)
(63 / 8)
(59/ 1)
(90/7) 7)
(15/ 17)
Results from VNN-COMP'24
Brix et al.
2024)
100.0%
100.0%
87.8%
98.6%
100.0%
98.0%
100.0%
100.0%
8-BB-ROWN
(139 / 47)
(30 32)
(24/ 134)
(63
8)
(59 1) (91/7)
(421 (
(15 17)
98.9%
100.0%
87.2%
98.6%
100.0%
98.0%
90.5%
100.0%
NeuralSAT
(138 / 46)
(30)
(33/134)
(63 (8) (59/1) (91/7)
(327 /650)
(15 17)
98.9%
93.5%
83.3%
98.6%
100.0%
97.0%
79.9%
100.0%
PyRAT
(137 / 47)
(30 / 28)
(22
128)
(63 8) (59 1) (91/6)
(277 (86)
(15/17)
96.2%
100.0%
86.7%
95.8%
100.0%
53.0%
62.5%
93.8%
Marabou
(134 / 45)
(30 32)
(22 134)
(62 (72 (5 (46/7) (300 /300/375)
(13/17)
99.5%
100.0%
14.4%
98.3%
46.0%
89.2%
56.2%
nnenum
(139/46)
(30/
(20/6)
(-/-) (59/0) (44
(321 / 642)
(2/16)
Table 2: Input Refinement: without (X) with (V).
Input Refinement
acasku
eaCenlp
X
(Ours)
X
/ (Ours)
avg. #Sub-
1611.
651.5
4.00.88
1 529.2
problems& + (max)
(133438)
(36 134)
(293 304)
(114
&Slved
99.5%
99.5%
80.8
89.2%
(#Verified #Falsified)
(138 47)
(138 / 47)
(298 / 575)
(311 / 652)
max Time max Time per Iter. 4
32.5s
15.1s
19.9s
12.4s
118.6ms
302.8ms 8ms
54.3ms
89.4ms
GPU Acceleration and Batch Size We demonstrate the efficacy and speed up of the GPU accel- eration and batch size by comparing the results of the acasxu and sa fenlp benchmark computed on a CPU (Tab, 3ab: The GPU acceleration enables a significant speed up, which allows the verifica- tion of more instances within the allotted timeout, i.e., the GPU speeds up the verification by 82.8% on acasxu and 89.8% on safenlp.
Falsification Method We compare our set-based adversarial attack (Sec. against the fast- gradient-sign method (FGSM) (Goodfellow et al. 2015) on the safenlp benchmark. Tab. 3b shows the number of instances falsified within the first 50 iterations compare the falsification strength without influence from the runtime. Our set-based adversarial attack outperforms FGSM by falsifying 60.3% more instances. Further, the main results (Tab. [ show that in most benchmarks match the top falsification performance.
6 RELATED WORK
Neural Network Verification and Adversarial Attacks Most algorithms for neural network ver- ification either (i) formulate an optimization or constraint satisfaction problem and apply an of- f-the-shelf solver, c.g., satisfiability modulo theories (Katz al.) 2017, Duong et al. 2023 Wu
ctt al.) 2024) or (mixed-integer) linear programming (Singh et al. 2019b; Müller ct al. 2022 or
(ii) use abstract interpretation reachability analysis to enclose the intersection of the specification
with the output of the neural network (Gehr et al.] 2018 Wang et al., 2018 Singh et al. 2019a
Wang et al. 2021 Kochdumper al. 2023 Ladner & Althofi 2023 Lemesle al. (024)
The most common abstract domains or set representations are intervals (Gehr et al. 2018). zono- topes (Gehr al. 2018). or polytopes (Müller et al. 2022 Zhang al. 2018 Singh et al. 2019a)
8

---

Published as a conference paper at ICLR 2026
Table 3: Ablation studies.
(a) GPU vs. CPU [max. Verification Time J (%Sovved)).
Method
(b) Falsification [#Falsified 1 (%Solved)).
(Batch Size)
acasxu
satenip
CPU (1)
(95.7%)
40.1s
(83.1%)
14.7s
Falsification
(S 50 iter.
safenlp
7.3s
2.0s
FGSM
257 (23.8%)
GPU (128)
(99,5%)
(86.8%)
Ours
647 (59.9%)
6.9s
1.5s
GPU (1024)
(99.5%)
(89.2%)
that use linear relaxations of activation functions for the propagation. More complex set representa- tions can enclose the output set more tightly, e.g., polynomial zonotopes (Kochdumper al. 2023) hybrid zonotopes (Ortiz et al. 2023), star sets (Bak) 202T); however, due to higher computational cost, these approaches do not scale large neural networks. The results of multiple abstract domains can be combined to obtain a tighter enclosure (Lemesle et al.] 2024). A popular abstract domain, DeepPoly/CROWN (Singh al. 2019a Zhang al.) 2018). uses bounded polytopes, which represented as the intersection of linear bounds and intervals. Further, gradient-basee based optimization can be applied to bounding parameters to tighten the computed enclosure (Wang et al. 2021).
If formal verification is computationally infeasible, an alternative is to falsify neural networks using adversarial attacks. Often, gradient-based attacks are fast and effective at finding adversarial pertur- bations (Goodiellow et al., 2015 Kurakin et al., (017). Further, stronger adversarial examples can be computed with optimization- based approaches (Carlini & Wagner 2017). Our set-based falsifi- cation does not require the gradient of the neural network, while being faster to compute than an optimization problem.
Iterative Neural Network Refinement There are different iterative refinement approaches, e.g., refining bounds using umixed-integen linear programs (Wang al.] 2018 Singh et al.) 2019bb Yang et al. 2021). counterexample guided abstraction refinement (Wu et al. 2024), and refining the hyperparameters of output enclosure (Xu al. 202T Ladner & Althof! 2023). Our novel specification- driven input refinement iteratively encloses the set of inputs that cause an intersection with an unsafe set in the output space. Therefore, our refinement does not require tuning hyper- parameters or solving expensive (mixed-integer) linear programs. The refinement procedure uses dependencies between propagated zonotopes, which can be used simplify computations for reach- ability analysis or identify falsifying states (Kochdumper et al. 2020).
Further, our input refinement can used to enclose the preimage of a neural network. Linear bounding techniques can be used to enclose preimages by solving multiple linear programs to com- pute bounds with respect to constraints or dimensions separately (Kotha et al., 2003) Zhang et al.) 2024). Conversely, compute zonotope enclosing the preimage that optimize with an iterative procedure with respect to all constraints and dimensions simultancously.
Branch-and-Bound Algorithms and Splitting Heuristics For large neural networks, most ver- ification approaches are too conservative. Therefore, practice. most verification approaches use a branch-and-boun procedure that recursively splits the verification problem into smaller subprob- lems that are easier to solve (Brix al.) 2023 2024), e.g., by exploiting the piece- wise línear- ity of the ReL.U-activation function. There are various approaches and heuristics for splitting verification problem, e.g., largest radius, largest approximation error and its effect on the output constraints (Henriksen & Lomuscio, 2021). gradient or sensitivity-baset impact of a neuron on the output (Balunovic et al. 2019 Ladner & Althofi 2023), magnitude of the coefficient of linear relaxation (Durand et al. 20222, largest unstable neuron in the first undecidable layer (Yin et al. 2022), multi-neuron constrants (Ferrari et al. 2022), least unstable neuron (Duong et al. 2023).
heuristics to estimate the

---

Published as a conference paper at ICLR 2026
7 CONCLUSION
In this paper, we present a novel iterative specification-driven input refinement procedure to speed up the formal verification of neural networks. For the refinement, exploit latent space that is an artifact from the propagation of projection-based set representations, e.g., zonotopes, through the layers of neural network. Our procedure iteratively refines an enclosure of the unsafe inputs by using the latent space to constrain the input set with the unsafe set from the output space. We inte- grate our refinement procedure into branch-and- an extensive evaluation, we show significant reduction in the number of recursive splits required for verification. Moreover, we demonstrate that our algorithm achieves competitive performance compared to the top-5 tools from the most recent neural network verification competition. In sum- mary, the exploitation the proposed latent space presents a promising new direction for the formal verification of neural networks.
neural network verification algorithm. In
ACKNOWLEDGEMENTS
This work was partially supported by the project SPP-2422 (No. 500936349) and the project FAI (No. 286525601), both funded by the German Research Foundation (DFG).
REFERENCES
Matthias Althoff. Reachability analysis and its application to the safety assessment of autonomous cars. PhD thesis, Technische Universität München, 2010.
Matthias Althoff. An introduction to CORA 2015. In ARCH Workshop, pp. 120-151, 2015.
Matthias Althoff and Goran Frehse. Combining zonotopes and support functions for efficient reach- ability analysis of linear systems. In CDC, pp. 7439-7446, 2016.
Stanley Bak. nnenum: Verification relu neural networks with optimized abstraction refinement. In NASA formal methods symposhum, pp. 19-36, 2021.
Mislav Balunovic, Maximilian Baader, Gagandeep Singh, Timon Gehr, and Martin Vechev. Certi- fying geometric robustness of neural networks. In NeurlPS, volume 32, 2019.
Christopher Bishop. Pattern recognition and machine learning. Springer New York, NY, 2006.
Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (VNN-COMP). S7TT, 25 (3):329-339, 2023.
Christopher Brix, Stanley Bak, Taylor Johnson, and Haoze Wu. The fifth international verifica- tion of neural networks competition (VNN-COMP 2024): Summary and results. arXiv preprint 2rXhv:2412.19985 2024.
Rudy Bunel, llker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan Mudigonda. A unified view of piecewise linear neural network verification. In NewrlPS, volume 31, 2018.
Nicholas Carlini and David Wagner. Towards evaluating the robustness of neural networks. In IEEE SSP, pp. 39-57, 2017.
Pranav Singh Chib and Pravendra Singh. Recent advancements in end-to-end autonomous driving using deep learning: A survey. IEEE T-IV, 103: 2023.
Christophe Combastel. Zonotopes and Kalman observers: Gain optimality under distinct uncertainty paradigms and robust convergence. Automatica, 55:265-273, 2015.
Hai Duong, Vu Nguyen, and Matthew Dwyer. A dpll (t) framework for verifying deep neural networks. arXiv preprint arXiv:2307. 2023.
Serge Durand, Augustin Lemesle, Zakaria Chihani, Caterina Urban, and François Terrier. ReCIPH: Relational coefficients for input partitioning heuristic. In WFVMI. 2022.
10

---

Published as a conference paper at ICLR 2026
Claudio Ferrari, Mark Niklas Müller, Nikola Jovanovié, and Martin Vechev. Complete verification via multi-neuron relaxation guided branch-and- and-bound. In ICLR, 2022.
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Mar- tin Vechev. Ai2: Safety and robustmess certification of neural networks with abstract interpreta- tion. In IEEE SSP, pp. 3-18, 2018.
Antoine Girard. Reachability of uncertain linear systems using zonotopes. In IISCC, pp. 291-305, 2005.
Ian Goodfellow, Jonathon Shlens, and Christian Szegedy, Explaining and harnessing adversarial examples. In ICLR, 2015.
Patrick Henriksen and Alessio Lomuscio. DEEPSPLIT: An efficient splitting method for neural network verification via indirect effect analysis. IJCAI, pp. 2549-2545552 3549-2555, 2021.
Ahmed Irfan, Kyle D. Julian, Haoze Wu, Clark Barrett, Mykel Kochenderfer, Baoluo Meng, and James Lopez. Towards verification of neural networks for small unmanned aircraft collision avoidance. In DASC, pp. 1-10, 2020.
Radoslav Ivanov, James Weimer, Rajeev Alur, George Pappas, and Insup Lee. Verisig: verifying safety properties of hybrid systems with neural network controllers. In HSCC, pp. 169-178, 2019.
John Jumper, Richard Evans, Alexander Pritzel, Tim Green, Michael Figurnov, Olaf Ronneberger, Kathryn Tunyasuvunakool, Russ Bates, Augustin Židek, Anna Potapenko, Alex Bridgland, Clemens Meyer, Simon A. A. Kohl, Andrew Ballard, Andrew Cowie, Bernardino Romera- Paredes, Stanislav Nikolov, Rishub Jain, Jonas Adler, Trevor Back, Stig Petersen, David Reiman, Ellen Clancy. Michal Zielinski, Martin Steinegger, Michalina Pacholska. Tamas Berghammer, Se- bastian Bodenstein, David Silver, Oriol Vinyals, Andrew W. Senior, Koray Kavukcuoglu, Push- meet Kohli, and Demis Hassabis. Highly accurate protein structure prediction with alphafold. Nature, 596(7873):583-555) 2021.
Guy Katz, Clark Barrett, David L.. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In CAV, pp. 97-117, 2017.
Donald Knuth. The Art of Computer Programming, volume 1: Fundamental Algorithms. Addison- Wesley, 1997.
Niklas Kochdumper, Bastian Schürmann, and Matthias Althoff. Utilizing dependencies to obtain subsets of reachable sets. HSCC, 2020.
Niklas Kochdumper, Christian Schilling, Matthias Althoff, and Stanley Bak. Open- and closed-loop neural network verification using polynomial zonotopes. In NASA Formal Methods, pp. 16-36, 2023.
Lukas Koller, Tobias Ladner, and Matthias Althoff. Set-based training for neural network verifica- tion. TMLR, 2025.
Suhas Kotha, Christopher Brix, Zico Kolter, Krishnamurthy Dvijotham, and Huan Zhang. Provably bounding neural network preimages. In NeurlPS, 2023.
Alexey Kurakin, Ian Goodfellow, and Samy Bengio. Adversarial machine learning at scale. In ICLR, 2017.
Tobias Ladner and Matthias Althoff. Automatic abstraction refinement in neural network verification using sensitivity analysis. In HSCC, pp. 1-13, 2023.
Augustin Lemesle, Julien Lehmann, and Tristan Le Gall. Neural network verification with pyrat. arXiv preprint arXiv:2410.23300. 2024.
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. PRIMA: general and precise neural network certification via scalable convex hull approximations. PACMPI, 6(POPL). 2022.
11

---

Published as a conference paper at ICLR 2026
Joshua Ortiz, Alyssa Vellucci, Justin Koeln, and Justin Ruths. Hybrid zonotopes exactly represent relu neural networks. In CDC, pp. 5351-5357, 2023.
Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, 1998.
Joseph Scott, Davide Raimondo, Giuseppe Roberto Marseglia, and Richard Braatz. Constrained zonotopes: A new tool for set-based estimation and fault detection. Automaticu, 69: 19:126-136, 2016.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certi- fying neural networks. PACMPL, 3(POLL), 2019a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certifica- tion of neural networks. In ICLR, 2019b.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In NeurlPS, pp. 6369-6379, 2018
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. Beta- crown: Efficient bound propagation with per-neuron split constraints for neural network robust- ness verification. NeurIPS, 34:29909-299211 2021.
Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, et al. Marabou 2.0: a versatile formal analyzer of neural networks. In CAV, pp. 249-264, 2024.
Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. ICLR, 2021.
Pengfei Yang, Renjue Li. Jianlin Li, Cheng-Chat Huang, Jingyi Wang. Jun Sun, Bai Xue, and Lijun Zhang. Improving neural network verification through spurious region guided refinement. In TACAS, pp. 319-48888 2021.
Banghu Yin, Liqian Chen, Jiangchao Liu, and Wang. Efficient complete verification of neural networks via layerwised splitting and refinement. IEEE TCAD, 41(11):3898-390 2022.
Huan Zhang, Tsui-Wei Weng, Pin- Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. NeurIPS, 31, 2018.
Xiyue Zhang, Benjie Wang, and Marta Kwiatkowska. Provable preimage under- ander-approximation for neural networks. In TACAS, 2024.
Zhengxia Zou, Keyan Chen, Zhenwei Shi, Yuhong Guo, and Jieping Ye. Object detection in 20 years: A survey. Proc. IEEE, 111(3):257-27,, 2023.
A APPENDIX - EVALUATION DETAILS
For the evaluation, implement verification algorithm in MATLAB using the CORA tool- box (Althoff 2015).
To avoid an unfair comparison with the results of the VNN-COMP'24 (Brix et al. 2024). we run all our evaluations on a laptop with inferior hardware compared to the VNN. COMP'24, i.e., Intel Core 17-13700H and NVIDIA RTX 4070 Laptop GPU (8GB). The compe- tition utilizes servers equipped with an NVIDIA A10G GPU, featuring significantly more memory (24GB) (Brix et al. 2024 Sec. 2).
Hardware
12

---

Published as a conference paper at ICLR 2026
VNN-COMP
The selected benchmarks taken from the VNN-COMP'24 (Brix et al. 2024 acasxu a standard benchmark used by many prior works containing neural networks for airborne collision detection; collins-rul-che containing neural networks for condition-based mainte- nance; cora and metaroom containing neural networks for high-dimensional image classifica- tion; di st-shi ft containing neural networks for distribution shift detection; 1 lineart zenn containing neural networks for an autonomous aircraft taxing system; safenlp containing neural networks for sentence classification; tllveri fybench containing two-level lattice neural net- works.
Our selection of the top-5 tools is based on the ranking after the tool updates that resolved many penalties due to incorrectly formatted counterexamples (Brix et al. 2024 Tab. 35).
Ablation Studies To make meaningful comparison in our ablation studies, we compute the statistics in Tab. 2 3a 3 only for instances that all considered comparands have solved, because the additional instances solved would inflate the number of verified subproblems or the number of iterations, which would skew the statistics and prevent a meaningful comparison.
Refinement Termination We terminate our input refinement after fixed number of iterations. In each iteration of Alg. [ we apply 8 refinement iterations (Prop. 2 to the split input sets. For each refinement iteration, we apply our constraint zonotope bounding procedure (Prop. 3 for most iterations.
Numerical Tolerance All counterexamples are checked with respect to the numerical tolerance specified in the rules of the VNN-COMP (Brix et al., 2024, Sec. 2). In our experiments, did not observe any additional numerical instability caused by our input refinement.
B APPENDIX ENCLOSURE-GRADINN SPLITTING HEURISTIC
In each iteration of our verification algorithm (Alg. D we either split each input set along center of an input dimension or split the input set to an unstable ReLU-neuron along to exploit the piece-wise linearity of ReLU. Typical gradient- based splitting heuristics use the local gradient of the neural network to rank the importance of different input dimensions or neurons (Balunovic jet al. 2019 Ladner & Althofff 2023). The local gradient does not explicitly consider effects of splitting input dimensions or neurons guarantee a tighter enclosure. Therefore, we compute the gradient of the size of the output set with respect to the enclosure. We use the F-radius to measure the size of the output enclosure y (Cy, Gy)z enclose(* (f))), i.e., the F-radius is defined as the Frobenius norm of the generator
the conservatism of the enclosure, i.e., split does not
matrix (Combastel 2015 Def. 3): ||>|lr == EE Σj=1 G2 ((i.)) Intuitively, we use the gradient of the F-radius to measure the contribution an input dimension or an approximation error to the overall size of the output enclosure. For an input dimension i E [no]] we compute the score
s(i)
T()) Vrco [|)'||r
(10)
where the r |Gz 1 is the radius of the input set X' (cz, Gz)z C 1RT,, If the k-th layer is ReLU-activation layer, for l E [k]] we compute the score for the i-th neuron, for i E [nx]. by
s(L,, i) = (a(e) Vesco ||
(11)
where ex = 1/2 =x) is the radius of the approximation error. In each iteration, we split the input dimension or the neuron with the largest score.
In Tab. compare enclosure-gradien heuristic against a local-gradient heurtistic defined
as Ladner & Althoff 2023)
s()) r()) [V vo12
s s 1) Eu(s) /Verc
(12)
where y Th is the output of the neural network for the center of the input set, i.e., y (cz)). Our enclosure- enclosure-rradient heuristic outperforms the local-gradient heuristic on the considered benchmarks (acasxu and safenlp), demonstrating its effectiveness.
At the time of writing, VNN-COMP'2. 24 represented the most recent benchmark suite; the finalized hench- marks and results of VNN-COMP'25 released after the submission of this manuscript.
13

---

Published as a conference paper at ICLR 2026
Table 4: Splitting Hcuristics.
Heuristic Input Refinement Prop.
%Solved t (#Verified / #Falsified)
avg. #Sub-
avg. Time (max)
problems (max)
2ca.xu
98.4%
8580.5
1.8s
Local Gradient
(136 / 47)
(430403)
(85.2s)
99.5% (138 / 47)
620.3
0,8s
Enclosure Gradient (Ours)
(36 134)
(15.1s)
safenip
87.4%
6334.1
0.4s
Local Gradient
(297 647)
(177 123)
(19.2s)
89.2%
1478.1
0.3s
Enclosure Gradient (Ours)
(311 652)
(138 367)
(14.9s)
C APPENDIX ADDITIONAL RESULTS
In Tab. S we provide the results for the remaining benchmarks from Tab. 2 observations.
We briefly list our
Reduced Number of Subproblems Our input refinement reduces the number of subproblems across all benchmarks.
Verification Time Our input refinement speeds up verification for all benchmarks except acasxu, Anearizzen, and tllveri fybench; these benchmarks have low-dimensional input spaces (Brix al. 2024 Tab. 3), i.e., 5-dimensional for acasxu, 4-dimensional for linearizee zenn, and 2-dimensional for t veri Fybench. For acasxu and l linear zenn, naive input splitting already achieves fast verification times; for Eiverifybenchh the input re- finement only marginally reduces the number of subproblems, and thus the computational overhead increases the overall verification time.
Computational Overhead Quantifying the computational overhead of our input refinement is complicated due to batch-wise computations with varying batch sizes. Therefore, we report the max- imum per-iteration time to estimate the overhead. Generally, the per-iteration time is larger with our input refinement (V). However, for the high-dimensional benchmarks c.g., collinss follins-rul- cnn, cora, di sst-shi ft, and metaroom, the input refinement significantly reduces the splitting, thus, the batch sizes are significantly smaller and hence the maximum per-iteration time with input refinement is smaller; e.g., for collins rul cnn, the input refinement reduces the maximum number of subproblems from 97 (without refinement, X) to 2 (with refinement, v). Therefore, the maximum per-iteration time is reduced from 458.9ms (without refinement, 86.6m (with refinement, V)
D APPENDIX IMPLEMENTATION TRICKS
We efficiently implement our algorithm with only matrix operations to take full advantage of GPU acceleration. Furthermore, to make our algorithm practical, we reduce the memory footprint by storing only the bounds of the constrained zonotopes the queue. We use zonotopes for the set propagation (line However, compute the bounds of constrained zonotope before enqueue operation.
Computing the bounds of constrained zonotopes requires solving two linear programs for each di- mension, which limits GPU acceleration. Hence, we avoid solving linear programs by efficiently approximating the bounds of constrained zonotope by approximating the bounds of the constrained hypercube (Prop. B. The approximation is inspired by the Fourier-Mote elimination (Schrijver, 1998 Sec. 12.2).
14

---

Published as a conference paper at ICLR 2026
Table 5: Additional Results: without (X) vs, with (V) Input Refinement.
%Solved t (#Verified #Falsified) problems + (max)
avg. #Sub-
avg. Time
Input Refinement
max Time per Iter. +
+ (max)
aCE
99.5%
1611.2
0.7s
X
118.6ms
(138 47)
(133 438)
(32.58)
99.5% (138 / 47)
651.5
0,8s
(Ours)
302.8ms
(36 134)
(15.1s)
collins rul
100.0%
3.5
8.6s
x
2458.9ms
(30 32)
(97)
(241.7s)
100.0%
1.5
0.1s
/ (Ours)
86.6ms
(30 / 32)
(2)
(0.3s)
cora
40.0%
3.5
4.9s
X
383.3ms
(18 / 54)
(9)
(27.2s)
81.1%
1
0.1s
/ (Ours)
174.1ms
(18 / 128)
(1)
(0.2s)
dist-shift
98.6%
64.8
0.6s
x
281.4ms
(63 8)
(2420)
(13.6s)
98.6%
6.4
0.2s
((urs)
139.2ms
(63 8)
(229)
(4.9s)
"inearizen
100.0%
38.0
0.4s
x
50.6ms
1)
(210)
(1.2s)
100.0%
31,5
0.7s
/ (Ours)
83.2ms
(59 1)
(171)
(1.8s)
metaroom
93.0%
18.8
7.6s
X
751.2ms
(90/3) 3)
(42)
(149.5s)
97.0%
18.5
1.1s
/ (Ours)
476.1ms
(90 / 7)
(26)
(1.9s)
safenip
80.8%
4.00188
1.6s
x
54.3ms
(298 / 575)
(293 304)
(19.9s)
89.2%
529.2
0.3s
/ (Ours)
89.4ms
(311 / 652)
(1 (114 065)
(12.4s)
tllverifyaer.ch
100.0%
117.6
18.7s
x
3
(15 / 17)
(603)
(185.48)
100.0%
110.8
36.1s
v (Ours)
1148.9m
(15 / 17)
(595)
(368.6s)
To avoid clutter, we introduce further notation: For matrix A Rxxm denote the matrix with all non-positive entries set to zero with A E R2o, i.e., A+ = 1/2 (A + [A]); the matrix A E Rzo is defined analogously.
Proposition 3 (Bounds of Bounded Polytope). A constrained hypercube P. (C, d) H n _..50 c Ra with C Raxa and d E RP is enclosed by [g. i.e., P C [g.3]. For each dimension E [q). let Exe = In - ejee and for each (d() -t,, En Bo Ci.y En Bo)/C(a.)) The bounds P are computed as
(p), let Cos)
En = max (C(s.) 1 1 [p]: C(. < <0) U b.
B = min (Can)) | [p]: C(s) > 0} U (B
15

---

Published as a conference paper at ICLR 2026
Proof. We fix point 3 P and indices i [p] and [q] and show that 3 E B. From the definition of a polytope, it holds that: C(. 3 S d(c). By rearranging the terms, we obtain
Ca.)) d(s)
Ca. PUn S d(n
E
C(C,) Bas d(6) C(a)) 20 8.
hEld
We split cases on the sign of Ca.))
Case (Ct,,)) < 0). We obtain a lower bound for 8())
d()) - C(.,) 2100 8
S B1)
C(s))
Using the initial bounds, i.c., 2o0) S B1) S Bo(s) we can approximate the bounds of B(y);
B6) () d C(.)) 110 8
d() C(.,) Eun
d
C(. Ex B
2 min
min
C(,1))
REP
C(s))
BE B.
C(.))
d - minge 3o] C..)
2n) 3
d(s - -(t,t Enbt L0 - (i,)
E11b Bo
C(i))
C(i))
C(s)))
Case 2 (c.)) > 0). We obtain an upper bound for Р())
BG) 1 d C(.,) En
C(.)))
Using the initial bounds, i.e., 2000 S BB) S Boyy we can approximate the bounds of 8(z)
(6) (Ga))20) d(n - Ca.)) E1(r) 3
d()
CR.) En
d(1) - C.. En
max SEP
max
C(i,))
C(i))
BE A 5.,
C(s)
d(s - min minge BE [R, 100 C(i,) Eg0
d( (R.) En
L. (k.) Enet = C(a)
C(3
C(a,))
Each row i of the constraint matrix C generates an inequality for each dimension j of B. Thus, with _ [ Bo) we set 3 to maximum lower bound and Biy) minimum lower bound.
(5)
Note that Prop. 3 can be applied iteratively: For P = (C,d) n [0. with bounds [g. [8.
holds that P (C, d) n [3. thus, Prop. 3 can be applied again to obtain potentially smaller bounds. Fig. 4 illlstrrates the approximated bounds and exact bounds of a bounded polytope.
The bounds of a constrained zonotope 2 Blosa C R2 with 2 = (c, G)z can be approximated by applying an affine map to the bounds [ 3
C By of its constrained hypercube:
Blagd C [G B G 3
(13)
In Tab. 6. we evaluate the effects of our fast bounding constraint zonotope (Prop. 3 on the verifi- cation accuracy. We turned off the timeout because, with the exact bounds, we could not verify any instance within the allotted time. Both approaches can verify all instances, and as expected, com- puting the exact bounds is significantly slower; i.e., the average verification time is 823.3s vs. 1.0s for our fast bound approximation. Furthermore, the exact bounds only marginally reduce the num- ber of verified subproblems, i.e., on average 276.98 vs. 277.58 for the fast bound approximation, indicating that our approximated bounds sufficiently tight for verifying neural networks.
2 Computing the exact hounds of high-dimensional constrained zonotope is computationally expensive; thus, can only compare our approximation on the first 45 instances of the acasxu benchmark (prop1).
16

---

Published as a conference paper at ICLR 2026
0.5
-0.5
-1
0.5
0.5
Approx. Bounds [æ: ø
Initial Bounds [zg. Fol
Polytope P
Exact Bounds
Figure 4: Illustrating the approximated bounds (Prop. 3 and the exact bounds of a bounded poly- tope.
Table 6: Approximation of Constraint Zonotope Bounds.
%Sllved (#Verified #Falsified) problems 4 (max)
avg. #Sub-
avg. Time + (max)
Exact Bounds
max. Time per Iter. +
acasx:
100.0%
277.0
823.3s
171 559.7ms
(45 / 0)
(1045)
(3 0088.11
100.0%
277.6
1.0s
X (Prop.
110.2ms
(45 / 0)
(1 051)
(1.9s)
E APPENDIX COMPUTATIONAL COMPLEXITY
The following proposition provides the time complexity of an iteration of Alg.
Proposition Let E be the number of layers, p N be the number of output constraints, N be the number of generators of the output enclosure, and ε E M be the number of splits each iteration. An iteration of Alg. (lines 4 27) takes (n + Epq2) computation time with respect to i, P, and &.
Proof. Computing the enclosure of the output set (line 6 takes time O(k Koller et al. 2025
Prop. 16). Checking if the intersection of the enclosure with the unsafe is empty (line takes time Op q). Generating candidate counterexample (line 10) takes time (( +n, g): check- ing the counterexample (line 11 takes time O(x q² + pm,). Splitting the input into new sets and refining the each new input set (lines 15 takes time O (p + pg²)) p²?).
The dequeue and enqueue operations take constant time (Knuth 1997
Sec. 2.2.1).
In total, an iteration of Alg. takes time O(Eq² + Epq?).
F APPENDIX - PROOFS
Proposition 2. Given are a neural network ④: 1 - R"= an input set (cr. Gz)z C Ro with G. E IR x90, and unsafe set U (A,b) CR., Let y (cys Gy) z enclose 1 X) be an enclosure of the output set with Gy E R X4s, We enclose all unsafe inputs by constraining X to &lcsa i.e.
{or X (()) E C Xlosa C X,
17

---

Published as a conference paper at ICLR 2026
where C. == (oo))))) and d = Acy |AG vo- 1.
Proof. We fix unsafe input I fa E X ((x) u). Let y ((x) be its corresponding output. We use the definition of the unsafe set and the definition of zonotope, i.e., there are factors 3 E Bgg
c cy + Gy
(14)
For an unsafe output, have the following inequality:
yeu u Alcy + B) Sb
3)
AG,B5b- Acy
Please note that the first yo factors of the output are the factors of the input x, i.e., x = Cx + Gg B((oo))- Our goal is to constrain the factors B((oo])- Therefore, we rearrange the terms
A AG 3 s
Acy
- A G ((1oo) + A G ((-1 (llal\lool)) S Acy
A lool P((oo)) b (Acy AC P(lla]
C ((())))) S b- (A + A G (awl)(o))))) (((an)Moo)))
We bound the right-hand side get obtain constraints C' (((oo)) I d on the factors of a::
C. ((oo)) S cA A AG yC (ooo))))) s Acy + ((. d.
Thus, we conclude that the input x: is contained in the constrained input set X: Masa
The following corollary proves the soundness of our refinement for neural network verification and falsification.
Corollary 1. Given neural network Φ: R Rh input set X C TR= and unsafe == (A, b) n C R"s, the refinement of the input set (Prop. 2 can be used for verification and falsification
D(Xlc5a) nu= = -0 = x(X) nu= 0, Br E Moga: ((x) Eu = Br X: $(x) u.
Proof.
With Prop.
we obtain
X' \ Alosa S fo E ((x) $ u),
and therefore, we have
(( Mlcsa) =
-33x E X' X Elossa ((x) e U).
(15)
Thus,
{b ((2 nu =
0^ F(x (loss)) nu= (8(8)osa)
nu=
x c(u)
n(
Br Aloss:: ((x) Eu
13
Rr E Aloga: (xx) E EU
3r X' Xloss: Φ(x) Eu
Rr E (Nlosa U \ X cca):: ((x) Ed
Rr E X: ((x) U.
G DISCLOSURE USAGE OF LARGE LANGUAGE MODELS (LLMs)
We used a large language model (LLM) as general-purposs. tool to refine the writing and enhance clarity of expression. All research ideas, methodology, analysis, and conclusions are solely the work of the authors.
18


Reviews:
[{"review_id": "SgsCNgGnUo", "reviewer": "Reviewer_Lqdf", "summary": "The paper proposes a latent-space framework for abstract-domain propagation in neural network verification. The main idea is that instead of treating each layer's abstract element separately, the authors view them as projections of a higher-dimensional hypercube. This allows the method to \"pull back\" unsafe output constraints into the latent space and iteratively refine the input set based on those constraints. The approach integrates with a branch-and-bound (BnB) verifier and is designed to run efficiently on GPUs. Experimental results on VNN-COMP'24 benchmarks show competitive performance with fewer subproblems and good results.\n\nThe paper proposes a creative latent-space formulation for zonotope-based verification that conceptually unifies input and output abstractions and enables input refinement. While the idea is novel and shows promise for improving scalability, clarification of the soundness of the refinement and further exploration of the empirical impact is needed. Overall, the contribution is original and technically interesting.", "questions": "Discuss and clarify weaknesses above.\n\nAdditionally, the empirical results presented are mostly on smaller neural networks from VNN-COMP. Please clarify and discuss the capability to handle larger networks and other tasks, such as image classification. Can the approach work on adversarial robustness of MNIST, CIFAR, etc.? This would perhaps better highlight the capabilities of the approach to scale, as claimed in the contributions (and that the reviewer agrees is an interesting and potentially effective idea to exploit the latent space as an abstraction).", "limitations": "", "rating": 6, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The paper introduces a clear and creative latent-space interpretation of zonotope propagation. Viewing all layer abstractions as projections of a shared higher-dimensional B-space provides an interesting way to reason about dependencies between input, hidden, and output abstractions.\n\nProposition 2 provides a sound theoretical basis for transferring output-space constraints back to input space, and the overall refinement process integrates cleanly within a branch-and-bound verification loop. Well written pseudocode.\n\nThe experimental evaluation covers multiple VNN-COMP'24 benchmarks and includes evaluation that isolate the effects of the proposed refinements, GPU batching, and splitting strategies. The results show tangible improvements in efficiency (fewer subproblems, faster verification) while maintaining comparable verification coverage.\n\nFigures such as Figure 3 and the toy example make the geometric intuition accessible and help connect the abstract mathematics to practical verification behavior. Great figures overall.", "weaknesses": "While Proposition 2 and Corollary 1 justify the logical use of the refinement in verification, they don't prove that the latent-space refinement preserves enclosure of the reachable set. In particular, the paper does not formally establish that the refined zonotope Y_refined still over-approximates all reachable outputs of the corresponding refined input region X_refined.\n\nAlthough the method is described as applicable to \"projection-based\" abstractions, the implementation and evaluation are restricted to zonotopes. Consider either extending the analysis to another domain (e.g., star sets) or narrowing the claim.\n\nThe paper's main conceptual innovation, the latent-space input refinement, is only briefly evaluated. Table 2(a) reports only a few benchmarks, where acasxu shows reduced subproblems but no timing improvement, and timing metrics are absent from Table 1. Expanding the evaluation to include additional benchmarks in Table 2(a) and timing data in Table 1 (even in the appendix) would clarify whether the reported efficiency gains primarily stem from the refinement itself or from implementation factors, and would enable readers to better judge the consistency and generality of the refinement's impact.\n\nMinor Comments/Typos Found\n\n\"contrain\" - > \"constrain\"\nMissing % for some of the results of the tables.\n\"activiation\" - > \"activation\"\nConsistency in notation for vectors (bold vs. plain).\nTable 1: define \"Solved\" in the caption and clarify what counts as verified/falsified.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "vLRIufqu3c", "reviewer": "Reviewer_jJ3V", "summary": "This paper presents a novel verification algorithm for neural networks that integrates an iterative, specification-driven input refinement into a branch-and-bound procedure. The core idea is to use the dependency information preserved by zonotope propagation to \"transfer\" output constraints back to the input space, thereby refining the input set to focus only on potentially unsafe inputs. The implementation is designed for full GPU acceleration via matrix operations. The evaluation on VNN-COMP'24 benchmarks demonstrates competitive, state-of-the-art performance, with extensive ablation studies validating the design choices.\nHowever, the paper's central conceptual framing of a \"novel latent space\" is overstated, as it repackages the standard mathematical interpretation of zonotopes without providing a meaningful new insight for the verification task. Furthermore, the analysis lacks a thorough discussion of the computational overhead introduced by the iterative refinement procedure itself.\n\n**Recommendation:**  \nDespite the conceptual overreach regarding the \"latent space,\" the paper presents a solid, practical, and effective verification algorithm with strong empirical results. The core technical contribution of the iterative input refinement is novel and valuable. Given the competitive performance and efficient implementation, I am inclined towards **acceptance**, provided the authors significantly revise the framing to more accurately reflect the nature of their contribution and address the points above.", "questions": "*   Could the authors clarify what is gained by the \"latent space\" interpretation beyond providing an intuitive name for the shared factor space? Does it lead to algorithmic insights that are not apparent from a standard zonotope dependency analysis?\n*   The paper should temper its claims regarding the novelty of the latent space view and reframe the contribution to more accurately highlight the effective iterative refinement procedure and its efficient GPU implementation as the primary advances.\n*   Could the authors provide more analysis of the computational overhead of the refinement procedure and its impact on overall verification performance?\n*   The algorithm description would benefit from including more critical details in the main text, particularly for the adversarial input computation and constraint generation steps.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 4, "presentation": 2, "contribution": 3, "strengths": "1.  **Novel and Sound Method:** The iterative input refinement procedure (Proposition 2) is a novel and technically sound contribution. By iteratively constraining the input set based on the unsafe output specification, the method effectively reduces the number of subproblems in the branch-and-bound tree, leading to faster verification.\n2.  **Efficient Implementation:** The decision to implement the algorithm using only matrix operations to leverage full GPU acceleration is a significant practical strength. The results show a substantial speed-up compared to CPU execution, making the approach scalable.\n3.  **Convincing Evaluation:** The experimental evaluation is comprehensive and transparent. The tool achieves competitive performance against the top-5 tools from VNN-COMP'24. The ablation studies effectively demonstrate the individual contributions of the input refinement, GPU acceleration, and the proposed enclosure-gradient splitting heuristic.\n4.  **Practical Impact:** The method leads to tangible improvements in verification performance, including a reduced number of subproblems, faster solve times, and a high success rate across diverse benchmarks.", "weaknesses": "1.  **Overstated Framing and Novelty of \"Latent Space\":** The paper's central conceptual framing—a \"novel latent space\" for verification—is overstated. The observation that a zonotope is a projection of a hypercube is a standard, well-known interpretation of the zonotope definition. Maintaining a single, constant hypercube by padding generator matrices with zeros is an algebraic convenience rather than a profound theoretical insight. The paper fails to provide a meaningful interpretation of this \"latent space\" for the verification task itself. Consequently, the \"latent space\" narrative feels more like a post-hoc metaphor than a foundational concept that the algorithm genuinely depends upon in a deep way. The core algorithmic contribution (the refinement procedure) could be clearly explained without this conceptual overhead.\n2.  **Incomplete Algorithm Description:** The presentation of the core algorithm (Algorithm 1) relies heavily on appendices for critical components, including the adversarial input computation (Section 4.2) and constraint computation (Proposition 2 and Appendix B). This makes it difficult to understand the complete method from the main text alone.\n3.  **Limited Analysis of Refinement Overhead:** While the paper demonstrates that refinement reduces the number of subproblems, it doesn't adequately analyze the computational cost of the refinement procedure itself. The trade-off between reduced branching and increased per-iteration complexity deserves more discussion.\n\n### Minor Issues\n- Typo: P3 L149: $\\beta\\in [-1,1]^{q}$\n- Typo: P5 L262: constrain\n- I had problems understanding the statement of Proposition 2 because of the way it is formulated. Clarify that \"$\\mathcal{X}|_{C\\leq d}$ encloses the intersection of the input set with the preimage of the unsafe set\" is the main statement.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "sFP9gYkUsJ", "reviewer": "Reviewer_hneQ", "summary": "This paper proposes a novel refinement method for zonotope-based verification of the robustness properties of neural networks.\n\nSpecifically, it describes a latent space, meaning a hypercube, with the property that the input zonotope, as well as the intermediate and output zonotopes while and after propagating through the network, are all \"shadows\" of this hypercube, that is, they are projections. This method enables the creation of a relatively tight enclosure of the set of inputs.\n\nThe performance of the proposed procedure is demonstrated experimentally on SOTA benchmarks by incorporating the proposed refinement into a branch-and-bound algorithm. The experiments show that it is often competitive\nwith existing high-performing ones verifiers. Additionally, the number of subproblems that\nmust be solved is, in some cases, significantly fewer than without the proposed refinement.", "questions": "- I am curious about the reasonable next steps for the approach to refinement you have proposed here. More specifically, I am attempting to understand whether this \"novel view\" you propose paves the way for follow-up works and, if so, in what manner?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "Improving the performance of FNN verifiers, particularly those based on zonotopes, is a topic of significant relevance and a suitable contribution for ICLR.\n\nFurthermore, the paper is excellently written and thoroughly polished,\nmaking it a pleasure to read. This is particularly evident in the balance\nbetween formal rigour and the intuitive explanations provided by the authors.", "weaknesses": "I identify one notable weakness:\n- The experimentally demonstrated improvements, while present, are not dramatic. I perceive the incremental enhancement offered by this refinement as a valuable contribution. Nonetheless, as I am not a specialist in this precise domain, I wonder if the enhancement might be too modest or if further extensive experiments are required to substantiate the minor, yet existent, improvements due to this refinement approach.\n\nMinor issues include:\n- The explanation of \"shadows\" as a concept of refinement is appreciated. However, while it is clear that the latent hypercube remains the same across steps but is rotated (see, for instance, Figure 2), the connection between this idea and Proposition 2 is not entirely clear. A slightly clearer exposition could be beneficial.\n- Although it is not central to the paper, the introduction's claim that \"verification of FNN is in general undecidable\" and \"NP-complete for ReLU FNN\" feels superficial. There is not a single \"verification problem\" for FNNs. Various notions exist, such as robustness and reachability, each contingent on parameters like input and output set specifications and FNN architecture types. Consequently, this has spawned extensive literature analysing the complexity of these problems in detail (see, e.g., [1],[2],[3] and others). Furthermore, the undecidability assertion appears misplaced. While referenced in another paper, so not a statement of the authors, it arises simply from the existence of undecidable sets of reals and is not an inherent property of \"FNN verification\" problems.\n- Proposition 2: The definition of $d:=...$ is unclear to me. This may be due to a typo.\n\n--- \n[1] Marco Sälzer, Martin Lange:\nReachability in Simple Neural Networks. Fundam. Informaticae 189(3-4): 241-259 (2022)\n\n[2] Adrian Wurm:\nRobustness Verification in Neural Networks. CPAIOR (2) 2024: 263-278 \n\n[3] Moritz Stargalla, Christoph Hertrich, Daniel Reichman:\nThe Computational Complexity of Counting Linear Regions in ReLU Neural Networks. CoRR abs/2505.16716 (2025)", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "GNbTWm6FHo", "reviewer": "Reviewer_JVYp", "summary": "This paper introduces a novel latent-space formulation for neural network verification based on projection-based set representations, such as zonotopes. The key idea is to interpret the sets propagated through a network as “shadows” of a shared higher-dimensional latent set, which enables transferring output constraints back to the input domain for iterative specification-driven input refinement. The proposed method integrates this refinement into a branch-and-bound verification framework, implemented purely with matrix operations for efficient GPU acceleration. Experimental results on VNN-COMP’24 benchmarks show competitive performance and substantial reductions in subproblems compared with state-of-the-art tools.", "questions": "1.How does the proposed latent-space refinement behave when using non-piecewise-linear activations (e.g., tanh, sigmoid)? Can the method generalize without losing soundness guarantees?\n2.The refinement procedure iteratively constrains inputs based on unsafe output sets. How is termination ensured in practice—by a fixed iteration limit or a convergence threshold?\n3.Since the algorithm uses only matrix operations, could the authors discuss numerical stability issues (e.g., accumulation of floating-point errors) in deep networks?\n4.Double-Blind Compliance: The manuscript notes that the proposed verifier “would place it among the top-ranking tools of the last VNN-COMP’24.” Could the authors clarify whether they personally participated in VNN-COMP’24 or reused their own competition submissions? If so, this phrasing might unintentionally compromise anonymity. A general comparative statement without potential self-identification could be safer under ICLR’s double-blind policy. \n5.It would be valuable to understand the trade-off between refinement accuracy and computational overhead—does aggressive refinement ever hurt verification completeness?", "limitations": "", "rating": 8, "confidence": 2, "soundness": 4, "presentation": 3, "contribution": 4, "strengths": "1.Conceptual originality -The latent-space interpretation of set propagation provides a fresh geometric perspective on verification problems.\n2.Technical soundness-The integration of constrained zonotopes and iterative refinement is mathematically consistent and grounded in established reachability theory.\n3.Practical scalability-The matrix-only implementation with GPU acceleration is elegant and demonstrates a real performance gain.\n4.Comprehensive evaluation -The comparison with multiple VNN-COMP tools and detailed ablations add credibility to the empirical claims.\n5.Potential for future extensions-The framework could generalize to other activation functions and verification domains (e.g., control systems).", "weaknesses": "Clarification of Competition Reference： The paper states that the proposed tool would rank among the top of VNN-COMP’24, which, while illustrative, might risk breaking double-blind policy if the authors were participants or submitted related work. A clearer phrasing could avoid potential self-identification. \n \nLimited Discussion on Generalization： While the latent-space formulation elegantly improves efficiency, its scalability to larger architectures beyond benchmarks (e.g., transformers or diffusion models) is not discussed, leaving some uncertainty about general applicability. \n \nEvaluation Scope： Experiments are strong on VNN-COMP tasks, yet cross-domain or real-world safety-critical benchmarks (e.g., perception-driven models) could further demonstrate practical robustness. Overall, these are minor concerns rather than major flaws.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)