Set-Based Training for Neural Network Verification
Authors: Lukas Koller
Tobias Ladner
Matthias Althoff
Venue: Accepted by TMLR ()

Abstract: Neural networks are vulnerable to adversarial attacks, i.e., small input perturbations can significantly affect the outputs of a neural network. Therefore, to ensure safety of neural networks in safety-critical environments, the robustness of a neural network must be formally verified against input perturbations, e.g., from noisy sensors. To improve the robustness of neural networks and thus simplify the formal verification, we present a novel set-based training procedure in which we compute the set of possible outputs given the set of possible inputs and compute for the first time a gradient set, i.e., each possible output has a different gradient. Therefore, we can directly reduce the size of the output enclosure by choosing gradients toward its center. Small output enclosures increase the robustness of a neural network and, at the same time, simplify its formal verification. The latter benefit is due to the fact that a larger size of propagated sets increases the conservatism of most verification methods. Our extensive evaluation demonstrates that set-based training produces robust neural networks with competitive performance, which can be verified using fast (polynomial-time) verification algorithms due to the reduced output set.

Published in Transactions on Machine Learning Research (08/2025)
Set- Training for Neural Network Verification
Lukas Koller Technical University of Munich
mokas.koller@tumn
Tobias Ladner
tobias. www.er@run.ddee.e...
Technical University of Munich
Matthias Althoff
althoff@tum.d de
Professorship for Cyber-Physicd, Systems Technical University of Munich
Reviewed OpenReview: https: opte:e:///penevvieeuu net/ forum? ieapnmmmdddaeen id=mOlzHrAkkA
Abstract
Neural networks are vulnerable to adversarial attacks, i.e., small input perturbations can significantly affect the outputs of neural network. Therefore, to ensure safety of neural networks in safety-critical environments, the robustness of a neural network must be formally verified against input perturbations, e.g,, from noisy sensors. To improve the robustness of neural networks and thus simplify the formal verification, we present a novel set- set-based training procedure in which we compute the set of possible outputs given the set of possible inputs and compute for the first time gradient set, i.., each possible output has a different gradient. Therefore, we directly reduce the size of the output enclosure by choosing gradients toward its center. Small output enclosures increase the robustness of neural network and, at the same time, simplify its formal verification. The latter benefit is due to the fact that a larger size of propagated sets increases the conservatism of most verification mothods. Our extensive evaluation demonstrates that sct-based training produces robust neural networks with competitive performance, which can be verified using fast (polynomial- time) verification algorithms due to the reduced output set.
1 Introduction
Neural networks demonstrate impressive performance for complex tasks, such as speech recognition (Hinton et al. 2012) object detection (Wang et al. 2023 However, many neural networks sensitive to input perturbations (Szegedy et al.] 2014): Small, carefully chosen input perturbations ions can lead to unexpected outputs. This behavior is problematic for the adoption of neural networks in safety-critical environments, where the imput often contains noisy sensor data or subject to external disturbances, e.g., autonomous ve- hicle control (Ye et al. 2022) or airborne collision avoidance (Trfan et al. 2020). Thus, the formal verification of noural networks gained interest recent years (Brix et al., 2023 2024). Given a set of inputs, the goal of formal verification of neural networks is find a mathematical proof that the neural network returns the correct output for every input from the set. We focus training and verifying robust neural networks. For the robustness verification, the goal is to verify that within bounded input perturbations, which are typically modeled as balls of radius E Rso, there is no adversarial input that is classified incorrectly.
In this work, we address the challenge of training and verifying the robustness a neural network with novel sct-based training procedure. Adversarially trained neural networks Madry et al., [0188 Zhang et al. 2019) achieve great empirical robustness (against adversarial attacks). However, they remain hard to formally verify due to large approximation errors, which increase the size of enclosures of their output

---

Published in Transactions on Machine Learning Research (08/202))
Single Gradient
IBP
(b) DifFAi
(c) SABR
Target
Target
Target
(d) Gradient Set (ours)
Accuracy
Robustness
Gradient Set
Target
Target
Target
000 Output Set
Gradient
Interval Enclosure
Zonooope Enclosure
Comparing gradient set with the gradient of other robust training approaches for the same neural network in the output space. The blue area shows the exact output set of the neural network. Other training approaches ((a) IBP (Gowal et al., 2019). (b) DifTAi (Mirman et al. 2018) and (c) SABR (uüllr et al. 2023 propagate intervals to compute a single gradient. On the contrary, our set-based training (d) computes a gradient set based on the position (for accuracy) and size (for robustness) the output set.
Figure 1:
sets. Thus, we propose a novel set-based training that can explicitly enforce small output sets to simplify subsequent formal verification. During training, we enclose the output of the neural network and compute gradient set, ie., each possible output has different gradient. We can directly enforee smaller output enclosures by choosing gradients that point toward the center of the enclosure. gradient set, we use set-based loss function, which considers the position (for accuracy) and the size of the output enclosure (for robustness). Previous works are limited to a single gradient for training, thereby discarding much set-based information. Fig. compares our gradient set with the gradient of three robust training approaches: Interval bound propagation (TBP) (Gowal al. 2019), DiffAi (Mirman et al. 2018) and SABR (Mäller al. 2023). IBP computes bounds of the output and uses the gradient of the worst- case output; DiffAi
To compute the
zonotope enclosure compute tighter bounds compared to IBP; SABR the gradient of the worst case of smaller input region to reduce regularization by large approximation errors. Subsequently, we provide an overview of related work.
Formal Verification of Neural Networks The formal verification of neural networks is computationally challenging, i.e. the problem is NP-hard with only rectified linear unit (ReLU) activation functions (Katz) et al.] 2017); thus, approaches cither (i) formulate an optimization problem, which is solved with an off- off-tho-sholf solver, c.g.
verifying small neural networks can take long time. Most formal verification
(mixed-integer) linear programminn (Singh el al. 2011bb Zhang el al.] 2022 Müller el al. 2022) or satisfia- bility modulo theories (Katz et al. 2017 Wu et al. 2024), or (ii) use reachability analysis with efficient set representations, c.g., zonotopes (Girard 2005), and set- based computations to enclose the output set of a
neural network (in polynomial time) |Gehr al. 2018 Singh et al., 2019a] Wang et al., 2021 Kochdumper
et al. 2023
Ladner & Althoff
2023 Lemesle et. al. 2024). If the enclosure of the output is sufficiently
2

---

Published in Transactions on Machine Learning Research (08/2025)
tight, it can be used to formally verify neural network. The challenge for most reachability-based ap- proaches is the enclosure of nonlinearities in a neural network, which limits their scalability because each nonlinearity adds an approximation error that accumulates for large neural networks. Therefore, in practice, often branch-and- 2022 are used to recursively split the verification problem into smaller and simpler subproblems, e.g-; by exploiting the piccewise lincarity of the ReLU activation function. Due to the recursive process, branch-and- bound algorithms have exponential runtime in the worst case. We want to train robust neural networks that can be quickly verified without splitting the verification problem.
procedures (Bunel et al. 2020; Wang et al. 2021 Durand et al., 2022 Ferrari et al.,
On the contrary, neural networks can be falsified by adversarial attacks, i..,, small input perturbations that lead to an incorrect output. Often, adversarial attacks are fast to compute and effective at provoking incorrect outputs (Goodfellow et al. 2015). The fast gradient sign method (FGSM) and projected gradient descent. (PGD) are the most prominent approaches. The FGSM is a single-step gradient- adversarial attack that efficiently generates adversarial attacks (Goodfellow et al. 2015). PGD uses multiple itcrations of FGSM to compute stronger adversarial attacks (Kurakin et. al. 2017). However, neural networks can be robust for one type of attack but can remain vulnerable to another type of attack (Madry et al. 2018 ; thus, it is necessary to formally verify the robustness of neural networks.
Training Robust Neural Networks The training objective of a robust neural network is typically formulated as a min-max optimization problem (Madry et al. 2018): minimize the worst-case loss within a set of possible inputs. Computing the worst-case loss within a set is computationally difficult (Weng et al, 2018). Nonetheless, robust neural networks can be effectively trained by approximating the worst-casc loss with adversarial attacks, e.g., computed using PGD (Madry et al.) 2018
The well-established tradeoff-loss Zhang et al. 2019) combines regular loss for accuracy with boundary loss for robustness, which is approximated using adversarial attacks. The boundary loss pushes the decision boundary of a classifier away from the training samples and thereby improves the robustness of the trained neural network. However, neural networks trained with adversarial attacks remain hard to formally verify.
Therefore, some approaches combine the training and formal verification of neural networks. In these works, the approximation of a worst-case loss is replaced by an upper bound, guaranteeing that no perturbation will lead to an incorrect output. Different methods for computing an upper bound of the worst-case loss have been proposed: Interval bound propagation (IBP) (Goaal et al., 2019), lincar relaxation (Zhang et al. 2020), (mixxed-nnlegrr) linear programming (Wong & Kolter 2018), or abstract interprelation (Mirman el al. 2018). IBP computes conservative output bounds and uses the worst case within the bounds for training and verification (Gowal et al.) 2019) (Fig. [b). However, large approximation crrors can create an over- regularization and lead to poor performance (Müller el al. 2023
Thus, by propagating smaller input sets, state-of-the-art robustness results are achieved (Müller et al., 2023) (Fig. [p). However, branch-and-bound algorithm with worst-case exponential-time complexity is used for their formal verification. Instead, aim to train robust neural networks that can be quickly verified using polynomial-time verification algorithms. Therefore, we enclose the output set of a neural network using zonotopes, which is significantly tighter than using IBP. More closely related to our work is an approach using zonotopic enclosures during training {Mirman et al. 2018); however, much baseb information is discarded by only using the enclosure to bound the worst-case loss. All related approaches for training robust neural networks consider a single gradicnt. Conversely, our approach considers a gradient set (Fig, [D)), thereby simultaneously increasing the robustness of the neural network and simplifying the formal verification.
Other approaches combine IBP adversarial attacks computed in a latent space (Mao et al. 2023 Similarly, zonotopes can be partially propagated through a neural network to compute adversarial allacks in latent space (Balunović & Vechev 2020); however, the partial propagation results in layer-wise training of the neural network, which has significant computational overhead. Furthermore, the training of robust neural networks can be improved by using a specialized initialization for the parameters of a neural network (Shi et al. 2021
3

---

Published in Transactions on Machine Learning Research (08/2025)
Contributions Our main contributions are:
novel set-based training procedure for robust neural networks that, for the first time, uses a gradient set for training that generalizes the well-established tradeoff-loss (Zhang et al. 2019). The gradient set enables direct control of the size of the output enclosure to improve the robustness of the neural network and simplify formal verification.
A fast, batch-wisc, and diffcrentiable set-based forward propagation and backpropagation that is efficiently computed on a GPU. The set propagation uses analytical solutions for the image enclosure of typical nonlinear activation funetions.
An extensive empirical evaluation in which we demonstrate the competitive performance of our set-based training and compare with state-of-the-art robust training approaches. Moreover, we include large-scale ablation studies to justify our design choices.
Organization
We introduce the required preliminaries Sec. 2 In Sec. B we present our set-based
training procedure, which benefits from a fast, batch-wise, and differentiable set propagation derived in Sec. D We provide an empirical evaluation, including ablation studies in Sec. 5 Finally, we conclude our findings
in Sec. f
2
Preliminaries
2.1 Notation
Lowercase letters denote vectors and uppercase letters denole matrices. The i-th entry of a vector æ is denoted by I(z). For a matrix RTxm, A(i,)) denotes the entry in the i-th row and the j-th column, A(i,) denotes the i-th row, and A(-)) the j-th column. The identity matrix is written as In E Rg*x., We use 0 and 1 represent the vector or matrix (with appropriate size) that contains only zeros or ones. Given two matrices A E Rmxn and B E RRxx2, their (horizontal) concatenation is denoted by [A B] E (n if R1 n2, their Hadamard product is the element wise multiplication (A@B) A(.j) B(.,) The operation Diag(z) E Raxx returns a diagonal matrix with the entries of the vector x E R on its diagonal. We denote sets with uppercase calligraphic letters. For set S C R", we denote its projection to the i-th dimension by S(a). Given two sets S C R and S2 R" we denote the Cartesian product by Si S2 [ $2 $1 E S1, $2 E S2), and if n m, write the Minkowski sum S1 @ S2 {51 + $2 $1 S1. $2 E S2). For N, [n] {1,2, .2...,,,, n denotes the set of all natural numbers up to An n-dimensional interval I C R" with bounds l,u E I is denoted by I = [1, u]. where Vi E [m]: (()) I u(()- For function f: R + Rm we abbreviate its evaluation for a set S C IR" with S(S) = {f(s) 8 E S). The derivative of a scalar function R is denoted as f'(x) = 4/dx f(x) Moreover, the gradient of a function f: R² + R w.r.t. a vector x E R is its clement-wise derivative: (V)((z))() = 0farc f(x), for [n]. Analogously, we define the gradient of a function f: paxm w.r.t. a matrix A e Raxm; (Vaf(A)) = o/a f(A), for E [n] and j [m].
f: F +
2.2 Ferd-Forward Neural Networks
A foed-forward neural network bo R R consists of sequence of K E N layers. For the k-th layer, R4-1 N denotes the number of input neurons and n& E N denotes the number of output neurons. A layer can either be linear layer, which applics an affine map, or nonlinear (activation) layer, which applics a nonlinear activation function elernentwwise.
Definition 1 (Neural Network, (Bishop) 2006, Sec. 5.1)). For an input x E R the output y fo(x) R
of neural network & is computed by
ho
he (hx-1) for k E [x],
where
Wh 11-11-1 by if k-th layer is linear, otherwise,
hu = (1)
= Di (he-))))
4

---

Published in Transactions on Machine Learning Research (08/2025)
with weights Wa R bias by R and nonlineor activation function ox which is applied element- wise.
We denote the parameters of the neural network with 0, which include all weight matrices and bias vectors from its linear layers.
Training of Neural Networks We consider supervised training settings of a classification task, where a neural network is trained on a dataset = {(11,4)) (1)..... (Zn: (n),, containing inputs 32 E R with associated largets I, E {0.1)% 1)",. A larget 4, E {0, 10,1)%
one-hot encoding of the larget label 4 [md]. i.., 44)) 1 + 4 for all j [nx]. A loss function L 1R= R + R measures how well a neural network prodicts the targets. A typical loss function for classification tasks is the cross-cntropy error:
LCe(t, () =- Σ t0) In(p(s)):
(1)
where In denotes the natural logarithm and P(t) = (xx(vn)((ex((() 1) are the predicted class probabil- ities. The training goal of a neural network is to find parameters that minimize the total loss of the dataset D Bishop 2006
Sec. 5.2):
min Σ L(t,, Ro(x:))
(2)
(BLA)ED
We revisit the training of neural network to later augment it with sets. A popular algorithm to train neural network is gradient descent (Bishop 2006 Sec. 5.2.4): the parameters are randomly initialized (Glorot & Bengio 2010) and iteratively optimized using the gradient of the loss function. We denote the gradient of the loss function L w.r.t. the output of the k-th layer hg as:
9k = Vny Lt,
(3)
where y = (x(x) for input E R",, The weight matrix W' and bias vector by of the k-th layer are updated as [Bishop 2006, Sec. 5.3)
WA + We 7 Vw, ((, = W - 19 1
by - by Vn, L(l,)) = bb 1]
(4)
where 77 E Ryn is the step size of gradient descent, i.e., the learning rate. The gradients Jk are efficiently computed with backpropagation (Bishop) 2006] Sec. 5.3): by utilizing the chain rule, the gradient gN of the last layer is propagated backward through all neural network layers.
Proposition (Backpropagation, (Bishop 2006 Sec. 5.3)). Let y E uh an oulput of neural network with target E " The gradients IIe are computed in reverse order as
Wx 9k
if k-th layer is linear, Diag (hg gle otherwise,
9x vyL(t.y).
9k-1
for 1: = K, K 1 1.
From now on, we refer to this (standard) neural network training point-based training.
2.3 Set-Based Computation
Our approach extends beint-based training to sets, which represent by zonotopes. A zonotope is convex set representation describing the Minkowski sum of a finite mumber of line segments.
Definition 2 (Zonotope, (Girard 2005 Def. 1)). Given center E R= and generator matriz G E Raxx
zonolope Z C R is defined as
9 2 = c Σ G 30)
3 8E1-1,11 = G)
5

---

Published in Transactions on Machine Learning Research (08/2025)
Output Set y
Input I E X
Output y E )
Unsafe Outpuls N
Neural Network
Input Set A
Outer-approx.
Output Set y
Figure 2: Verifying the local robustness of neural network.
Subsequentl, we define several operations for zonolopes used in our training approach. Please note that for the complexity analysis, we only consider the number of binary operations and neglect the computational effort of unary operations. Moreover, we consider the textbook method and do not assume any special numerical tricks that have been developed for large matrices.
Proposition 2 (Interval Enclosure, (Althoff 2010 Prop. 2.2)). zonotope = (c. G) with c E R" and G TRxx is enclosed by the interval [7, u 2, where
u -=
and | compules the element-wise absolule volue. Compuling interval enclosure is in O(n
Proposition (Minkowski Sum, (Althoff 2010 Prop. 2.1 and Sec. 2.4)). The Minkowski sum of zonotope
Z (c, G) and interval I
[1 R with c, e,l, E Rº and G E 1828 is computed
Z I (c (u |G 1/2 Diag(u - 11))
and has time complezity O(n).
Proposition 4 (Affine Map, (Althofi 2010 Sec. 2.4)). The result of an affine map f: R" + +", 2 W r+b with W E mxxx and b E I applied to a zonotope = (c, G)z with c E Rn and E Raxq
((2) ([(=) 2) = W Z @ b (W We+b,WG)zz
and has time complerity (mm
During set-based training, we want to reduce the size of the output sets. However, determining the volume of zonotope computationally demanding (Elekes 1986). Nevertheless, we can effectively approximate the size of zonotope by its F-radius [Combastel 2015): The F-radius of zonotope is the Frobenius norm of its generator matrix.
Proposition 5 (F-Radius, (Combastel 2015 the F-radius is
Def. 3)). For zonotope 2 (c, G)z R with G Rax
q
2 | = 1/n
Pasy
(1j))
Please note that in contrast to (Combastel set-based training, compute a gradient set, i.c., the gradient of function w.r.t. zonotope, which is also vonotope, where the center is the derivative w.r.l. the center and the generator malrix is the derivative w.r.t. the generator matrix.
2015 Def. 3), include normalization factor of 1/n. For
Definition& 3 (Zonotope Gradient). The gradient of a function f(-) w...t. zonotope Z = (c, G) C R is defined as
Vzf(Z)= (v)))

---

Published in Transactions on Machine Learning Research (08/2025)
2.4 Formal Verification of Neural Networks
In this work, consider the robustness of neural networks for classification tasks: Fach dimension of output y E R corresponds to class, and the dimension with the maximum value determines the predicted class. An input I is correctly classified by neural network if the predicted class matches the target label I E [mx]:
arg max M(k) = I. kefnal
We call neural network (locally) robust for given set of inputs if the neural network correctly classifies every input within the set. Following previous works (Madry et al.) 2018 Gowal el al. 2019 Zhang et al.
2019
Müller et al. 2023), we use the -bal of radius E Ry0 around an input I E 12 as an input set:
Te = (x,, e Enoiz = { E R || - xl100 <]}.
(6)
For classification task with target label I E [nx], the unsafe set contains every incorrect classification, i.c., there is dimension k E [nx] for which the output v(a) is larger than the output of the larget dimension Vay (Ladner & Althoff 2023 Prop. B.2):
U = { E R
3k E [na]: B(A) v(0) = {8 Rd | (Ln, e ( 1),
(7)
where et R is the i-th standard basis vector. For input set X Te(x) R we formally verify the robustness of neural network to by using set-based computations to efficiently compute (in polynomial time) an enclosure y C " of its output set ) == &x(X') S y (Fig. 2 If y does not contain unsafe outputs, we have formally verified the neural network for the input set X, as also yr does not intersect with U:
ynu = = y" -
(8)
To compute an enclosure V, evaluate the layers (Def. over sets. The output set of linear layer is computed with an affine map (Ladner & Althoff 2023 Sec. 2.4), whereas the output set of a nonlinear layer is enclosed as it cannot be computed exactly for zonotopes, because they are not closed under nonlinear maps. The required steps are summarized in Fig. 3 The activation function is applied element-wise; hence, the input dimensions are considered independently. We first project the input set onto a dimension and compute bounds (Steps 1 & 2). The activation function is approximated using a linear function, and to ensure the soundness, bound on the approximation errors is computed (Steps 3 & 4). Finally, the approximation is evaluated over the input set, and the approximation errors are added (Steps 5 & 6).
We define the following set-based forward propagation.
Proposition 6 (Set-Based Forward Prop., [Ladner & Althoff 2023 Sec. 2.4)). For an input set X C R"" an enclosure y C Te of the output set. y" Tx(X)) of a neural network can be computed as
Wv H + be enclose (0k, Ha-1)
if k-th layer is linear, for k E [n], y Hr.
Ho X,
H4
otherwise,
The operation enclose( (42, Hk-1) encloses the image of a nonlinear layer [adner & Althoff 2023 Prop. 2.14). We denote the enclosure of the output set of a neural network 29 by y = enclose 48. X)).
Using the enclosure of the put set (Prop. 6), we can formally verify the robustness of neural network.
Proposition (Neural Network Verification, [Ladner & Althoff 2023 Sec. 2.4)). Given a neural net- work Φ: _o n and an input x _o with target label E [nx], we enclose the output set enclose ( ne (x)). We can formally verify the robustness of the neural network by
max (In, - yEY
- 1)v50 - nun 6
7

---

Published in Transactions on Machine Learning Research (08/2025)
Steps 1 &
Steps 3 & 4
Steps 5 & 6
Output
1
Input
Input
Input
Polynomial
Image Enclosure
Figure 3: Main steps of an image enclosure Ladner & Althol] 2023
Prop. 2.14).
2.5 Problem Statement
We want. to leverage set-based training to create robust neural networks.
Definition 4 (Set-Based Training). Given set-based loss function C R x 2 + R, set-based training trains a neural network using a gradient set Vy R (Def. 3 which defines a different gradient g V)((t,)) for each point y E y.
Set-based training can directly enforce smaller output sets by choosing gradients that point toward the center of an output set (Fig. 4 Thereby, we can simultaneously improve the robustness of the neural network and simplify the formal verification. We want to set-based training to train the parameters 0 of robust neural network 4g:
min Σ
C(te, enclose ne (2:))).
(Z..))ED
By reducing the size of the output set using set-based training, we can verify neural networks with fast (polynomial time) algorithms.
3 Set-Based Training of Neural Networks
We present a novel set-based algorithm to train robust neural networks with gradient set (Def. In each
training iteration, we (i) enclose the output set of the neural network by zonotopes (Sec. 4.1 (ii) compute a gradient set derived from a sct-based loss function using features of the output enclosure (Sec. 3.1
(iii) baoppraaagate the gradient set (Sec. 4.2), and (iv) aggregate the gradient set to update the parameters of the neural network (Sec. 4.3).
3.1 Set-Based Loss Function and Gradient Set
We derive the gradient set used for training by computing the gradient of a set-based loss function, which maps an output set to a loss value (Def. 4 In this work, we define the set-based loss function L R"= 2 + R. that it combines (i) standard loss of the center of the enclosure (for accuracy) with (ii) the
F-radius (Prop. 5 of the enclosure approximate its size (for robustness) (Fig. [p))
Definition 5 (Set-Based Loss). We define set-based loss function as
C(t,)) ( +
T/Dl
Accuracy Loss Robustness Loas
where L: T Th is loss function, E R>0 is the perturbation radius, and y (cxs Gx) is an oulput set.
8

---

Published in Transactions on Machine Learning Research (08/202))
Zonotope Gradient Set
10
5
-5
10
Zonotope
Gradient Sample
Figure 4: Gradients of the F-radius of zonotope.
The set- based loss function balances the standard loss of the center and the F-radius of the output set using hyperparameter [0, 1), controlling the tradeoff between accuracy and robustness. To make tuning the hyperparameter т easier, the F-radius in Def. 5 is normalized using the input perturbation radius E Ry0. The normalization is derived by taking the ratio of the F-radi of output enclosure y and input set X' = (T(),,
i.e., [ 1/4 |
Our set-based loss generalizes the well-ostablished tradcoff-loss (Zhang et al. 2019 Eq. 5), which combines standard training loss with boundary loss; for (b(x) and weighting factor X:
LTRADES(L, standard training loss
L(ly))
max (ET. boundary loss
L/ t
(9)
The F-radius in our set-based loss and the boundary loss in equation 9 have the same goal of training the robustness of the neural network. However, the F-radius captures the size of an output set in all directions, whereas the boundary loss only considers the distance to the furthest output. Morcover, through the sound set-based computations (Prop. 6 the set-based loss accurately over-approximates the size of the output set. In contrast, the boundary loss only approximated (Zhang et al., 2019) using adversarial attacks.
We derive the gradient set for training by computing the gradient of the sct-based loss function (Def. which requires the gradient of the F-radius.
Proposition 8 (Gradient of F-Radius). Given output set y (cn, Gx)z R"", the gradient of the F-radius is
Gn V>ID/1 = (0. nw ||
Proof. See Appendix D
The negative gradients of the F-radius of zonolope point toward the center of the zonotope (Fig. 4h hence, minimizing the F-radius of zonotope reduces the size of the zonotope. With Prop. we compute the gradient set used for training:
Proposition 9 (Set-Based Loss Gradient). Given an output set y = (Ces Gx) C R==, the gradient of the bat-based loss function is
VyL(t,)) -(10))(()) (1- Ve, L(t 7 E nu ||11| Gx Gx))
1
Proof- See Appendix D

---

Published in Transactions on Machine Learning Research (08/2025)
Fig. visualizes the gradient set for samples from the output set. For effective set-based training using the gradient set, we require efficient and differentiable set propagation, which we address next.
4 Fast, Batch-wise, and Differentiable Set-Propagation
We require efficient, batch-wisc, and differentiable set propagation to implement set-based training. In this section, we first. define a forward propagation with the required properties (Sec. before we derive the corresponding set-based backpropagation (Sec. 4.2) and weight updates (Sec. 4.3 Finally, we investigate the time complexity of our set-based training (Sec. 4.4
4.1 Set- eat-Based Forward Propagation
The set propagation through linear layers is computed with an affine map, which can be efficiently imple- mented batch-wise using matrix multiplications on a GPU. Further, we want to efficiently compute batch-wise image enclosures of nonlincar layers. Sampling- based methods (Ladner Althoff 2023 Kochdumper et al., 2023) are impractical for this task because they use polynomial regression and thus are not ellicient enough for backpropagation. In contrast, (Singh et al., 2018) derives fast analytical solutions for the approximation errors of a specific linear approximation of s-shaped activation functions; however, this approach causes large approximation errors. During training, large approximation errors induce an over-regularization, leading to poor performance (Müller et al. 2023). To address this issue, we derive analytical solutions for the approx- imation errors of linear approximations for three typical activation functions: rectified linear unit (ReLU), hyperbolic langent, and logistic sigmoid. Secondly, we provide a linear approximation whose approximation errors are smaller or equal to Singh's enclosure (Singh et al. 2018 Thm. 3.2) while being equally fast to compute.
For the remainder of this section, let Φ: R R be a monotonically increasing function, which is approximated by a linear function p: IR - R, ++ mæ z + within an interval [1, u] R. The approximation errors of p are given by the largest lower distance and upper distance between & and p (Fig. 5).
Definition 6 (Approximation Error of Linear Approximation). The approzimation ervor of a linear approz- imation for & within the interval [L. u] are defined as
E = min (xx) - p(x), xE(L.u]
غ = max 6(x) - p(x). xE!(u)
We enclose the output of the activation function & as,
a(l, ul) S p(z) @ lc.
Fig. 5 illustrates a linear approximation p of the hyperbolic tangent along with its approximation errors.
Efficient Computation of Approximation Errors We efficiently find the approximation errors e and of a linear approximation by only checking specific points of the interval [1 u]. i.e., extreme points of the activation function Φ
Proposition 10 (Approxination Errors for ReLU, Hyperbolic Tangent, and Logistic Sigmoid). The ap- prozimation error of for o (ReLU, tanh, of are computed as
min ((x) -p(x),
max
((x) - p(x),
zEPon((.u)
x =EP xEPon(L.u)
where
= [0,
Pranh = { tanh u,
P. = (+2 tanhi
(VI " 4m). hmm,,,,, ,l,u].
Proof. See Appendix D
10

---

Published in Transactions on Machine Learning Research (08/2025)
Output
Input
Input
tanh
P
Our Enclosure
Singh's Enclosure
Figure 5: Image enclosure of hyperbolic tangent: (left) Our linear approximation and approximation errors;
(right) Comparison of our image enclosure and Singh's enclosure (Singh et al. 2018 Thm. 3.2).
We note that our computation of the approximation errors works for any (monotonically increasing) linear approximation. Moreover, observe that the offset d of the linear approximation p does not affect the image enclosure; hence, w.l.o.g. we set d= 0.
Definition 7 (Linear Approximation of an Activation Function). Within the interval [L. u], we approzimate an activation function & by a linear function p(x) m, where
m o(u) 6l))
We note that the slope of our approximation identical to the slope used for the triangle relaxation by DeepPoly (Singh et al. 2019ab; however, instead of formulating linear constraints, we require the explicit computation (Prop. 10 of the approximation errors for the zonotope propagation. Our image enclosure no longer a polynomial regression requires sampling to compute the approximation errors (Kochdunper et a.. 2023 Sec. 3.2). Moreover, only matrix operations required, i.e., matrix multiplication, matrix addition, min, and max. Therefore, it can be efficiently computed batch-wise, taking full advantage of GPU acceleration.
Our Enclosure vs. Singh's Enclosure We motivate the choice for our image enclose by comparing it with Singh's enclosure (Singh et al.) 2018 Thm. 3.2). For s-shaped activation functions, e.g., hyperbolic tangent and logistic sigmoid, we prove that the approximation error of our linear approximation (Def. 7 is always smaller equal to the approximation crror of Singh's 's enclosure (Singh et al., 2018 Thm. 3.2) w.r.t. the area in the inpul-output plane (see Fig. measuring the integrated approximation error over [1, u]:
(sea [1) (u (e-
(10)
Proposition 11. Let & be an s-shaped function, and let [T, u] be an interval. Moreover, let [e be the approzimation errors of our enclosure (Def. 1 and 7., and let es be the approrimation ervor of Singh enclosure (Singh al., 2018 Thm. 3.2). It holds that
area ([s, 1,, u|) I area([-es, es). u,))
Proof.
See Appendix D
Fig. shows an instance where the output set computed with our image enclosure significantly smaller and does not intersect the unsafe region. In contrast, the output computed with Singh's enclosure intersects the unsafe region.
11

---

Published in Transactions on Machine Learning Research (08/2025)
-20
3/99)
-40
-60
40
20
0
1(8)
Unsafe Sct
Output Samples
Our Enclosure
Singh's Enclosure
Figure 6: Comparison of the output set of a neural network computed with our image enclosures and Singh's 's
enclosure (Singh et al. 2018 Thm. 3.2).
4.2 Set-Based Backpropagation
We now derive the corresponding set-based backpropagation. Analogous to the standard backpropaga- tion (Prop. [. the set-based backpropagation computes for every layer the neural network the gradient set w.r.t. the output set H4 (ck, Gkizi
=== (ch, (c4
VH,
(11)
The set-based backpropagation of linear layers is straightforward it applies an affine map (Prop. I However, the backpropagation of nonlincar layers is more involved: while the image enclosure only uses linear approximations, these depend on the input set. Thus, intuitively, we have to apply the product rule.
Please note that, we use the plus symbol (+) between zonotopes to denote their element-wise addi- tion: (e1, G1)z z + (c2.G2), G2)z = (c1 c2, G1 + G2)z, whereas the Minkowski sum is denoted as (c1, G1) (c2, G2)z (c1 02 (., G2l)z.
Proposition 12 (Backpropagation through Image Enclosure). Assume the k-th layer nonlinear layer with activation function dx. Given imput set H (Ck-1, (Ck-1,GR-1)2 with Gk-1 RR and a gradient
set Gb (ch, Gh) z the gradient set G (ch-1,, Gh-1) is computed for each dimension i [mg]]
9R-16 = -m(ss) Pu()) + (chcos Ck-1()) + Gi(c.De Gh-1(s)) FHe-sco
(4200) + (k(iptt) VHu-10 + (CEE)) - Ch(iptt)) (M(-)
The operation G6-1 backpropEnclosse Gk) computes the gradient set of an image enclosure.
Proof. See Appendix D
Using the backpropagation of an image enclosure, we can (analogous to Prop. 1 backpropagate the gradient sets through all layers of neural network.
Proposition 13 (Set-Based Backpropagation). The gradient sets G& are computed in reverse order as
WT Gx
if k-th layer is linear, backprop@hccosse@@.... 9k)) otherwise,
-x = VyL(t),
96-1
for k
Proof. See Appendix D
12

---

Published in Transactions on Machine Learning Research (08/2025)
4.3 Set- eat-Based Update of Weights and Biases
We now describe how to use the gradient set 9k and the set of inpuls Ha-1 to update the weights and biases of a linear layer: Intuitively, we compute the outer product between the gradient set Gh and input sct H4-1- To avoid clutter, we define the outer product between two zonotopes 21 = (c1, G1)z C R and 2 = (c2, G2)z C R as 21 O Z = cj cj + G1 G1 E R x"2.
Proposition 14 (Gradient Set of Weights and Biases). The gradients of the sel-based loss w.r.d. a weight matrix and bias vector are
Vw, ((1,)) VH. ((1)3) H
((1.))) (
Proof. See Appendix D
The weight matrices and bias vectors are updated analogous to standard training using the gradients of the set-based loss function:
W& W 77 Vw, ((t.))
by t by 1 Vo, (t,
(12)
4.4 Computational Complexity Finally, we derive the time complexity of set-based training. Alg. implements our image enclosure.
Algorithm 1: Image Enclosure of Nonlinear Layer. function enclose(dit, HE-1) Find bounds [4-1, 4x-1l of H for i 1 to ni do Find linear approx. ma(1) x of dx
// Prop-
4
// Def
Find approx. errors Ex(t); Ck(s)
// Prop.
Hy < Diag(m,) H4-1 1/2 (Ex + ex)
// Prop- 4
H4 + Hs @ lee. Ex] return Hk
// Prop.
We provide the time complexity of Alg. [ w.r.t. the number of input dimensions and generators. Proposition 15 (Time Complexity of Alg. 1. For an imput set H4-1= = Z with c E R and E R Alg. has time complerily On q) w.r.l. the number of inpul dimensions n and the number of generalors q.
Proof. See Appendix
Using Prop. 15 we can compute the time complexity of a set-based forward propagation.
Proposition (Time Complexity of Prop. G). The zonotopes during a forward propogation (Prop. have most q S no EkeW ni generators. Let Tmmaz = maxxe]<] n& be the marimum number of neurons in layer. The set-based forward propagtion (Prop. 6 has time complerity On 9k) w.r.t. To and the number of layers k.
Proof. See Appendix
Alg. implements an iteration of set-based training. First, we enclose the output set of the neural network (lines Gb. Then, we compute the gradient set (line(s which is backpropagated through the neural network
(lines 9 15 Finally, the parameters of the neural network are updated (lines 12 13
Proposition 17 (Time Complexity Alg, 2 Alg.
has time complexity O(n 2 qR) w.r.t. Rmaaz g and
the number of layers ss
13

---

Published in Transactions on Machine Learning Research (08/2025)
Algorithm 2: Sct-based Training Iteration. Hyperparameters: C Rs0, E [0, and Rzo-
Data: Input & E IR Target & E R
Result: Neural Network with Updated Parameters Ho f- (x, Inoiz
// construct input set // set-based forward prop. (Prop.
for f- to do
if k-th layer is linear then
Hr* s Wx Ha-1 bk
else
Hy + enclose( 11
y t Hx
// obtain output set // compute gradient set (Prop.
9N +- ())((t))
for k + ni to do k-th layer is linear then G f- W Is
// set-based backprop. (Prop.
13
10
11
12
W - W₁- (Gk @ H(-1)
// Prop. 14 and equation 12
13
by - by 7) (9x o (1
// Prop. and equation
12
14
else
15
- + backpropEnclosse(0. 9k)
// Prop. 12
Proof. See Appendix D
The time complexity of baseb training is polynomial, and compared to point-based training, only has additional factor O(no + Ekejw) R&). The increased time complexity is expected because set-based train- ing propagates entire generator matrices through the neural network. Moreover, for some linear relaxation methods, similar time complexities are reported (Zhang et al. 2018
5
Evaluation
We use the MATLAB toolbox CORA (Althofi 2015 to implement set-based training. Following previous
works Gowal et al. 2019). we train 6-layer convolutional neural network on MNIST (LeC'un et al. 2010
SVHN Netzer et al. 2011). CIFAR-10 (Krizhessky 2009), and TINYIMAGENET (e & Yang 2015 The training details can be found in Appendix We first present the main results and then justify our design
choices with extensive ablation studies.
5.1 Main Results
We compare our set-based training against adversarial tradeoff training, Lee. TRADES (Zhang et al. 2019), as well as two state-of-the-art interval-based training approaches, i.e,, IBP (Gowal et al. 2019 and SABR (Müller et al. 2023 For each training scheme, we report the clean accuracy (percentage correctly classified test samples) ) the falsified accuracy (percentage of test samples for which PGD finds an adversarial example) (Gowal al. 2019 and, unlike previous works, the fast-verified accuracy (percentage of verified test samples using zonotopes). Most related works report verified accuracies computed with slow (exponen- tial time) verification algorithms using branch-and- aouudd (Balunovié & Vechev 2020 Müller et al. 2023 Mao et al. 2023) or mixed-integer programming (Gowal et al.) 2019); the verification can take to 34h for MNIST networks (Müller el al. 2023) App. C). Our goal is the fast. (polynomial time) verification of neural networks. Thus, we report verified accuracy, which uses a single zonotope propagation (Prop. 6 with polynomial time complexity (Prop. 16p for the verification of each test input without a branch-and- procedure. The verification of 6-layer convolutional neural network trained on MNIST with 100 test inputs takes approximately 30min.
14

---

Published in Transactions on Machine Learning Research (08/2025)
Table 1: Comparison with state of the art (mean & std. dev. of the best runs across seeds).
Dataset
60o
Method
clean Acc.
falsified Acc.
fast-verified Acc. (max)
TRADES
99.40 0.04
98.40 = 0.06
0.00
(0.00)
IBP
97.76 0.26
96.32 = 0.39
95.58 0.41
(96.05)
MNIST
0.1
SABR
97.94 0.44
95.84 + 1.28
92.80 +-5.7
(95.86)
Set (ours)
98.76 0.29
97.52 = 0.26
0.88
(96.40)
TRADES
82.96 + 0.35
67.35 + 0.01
0
(0.00)
IBP
46.54
42.13 = 2.56
36.83 + 1.74
(38.80)
CIFAR-10
3/235
SABR
54.20 1::00+0: 0.90
48.04 + 0.49
39.96 0.30
(40.30)
Set (ours)
2.283
55.17 = 1.56
37.79
(39.36)
TRADES
91.30 0.28
78.34 0.28
0.00
(0.00)
IBP
72.33 + 4.26
61.27 + 3.46
46.93 + 3.09
(50.18)
SVNH
0.01
SABR
81.79 4.36
63.26 = 14.32
12.62
(17.81)
Set (ours)
82.66
72.35 = 2.68
29.39
(41.35)
TRADES
28.14
19.80 = 0.43
0.00
(0.00)
IBP
9.62
8.76 - 0.95
2.89
(4.07)
TINYIMAGENET
1/235
SABR
1.37
12.49 = 1.25
3.68 0.87
(4.68)
Set (ours)
16.70 + 2.79
14.80 2.54
0.02
(0.05)
Standard Training
Set-Based Training (ours)
Class
Class 2
Perturbation Set
Figure 7: Comparing the decision bounds of point-based (left) and set-based (right) training. The dashed line is the decision boundary of basnt-based training.
Tab. shows results. Across all datasets, TRADES shows the best performance for clean and falsified accuracy; however, the verification is notoriously hard. Both interval-based approaches, IBP and SABR, have lower clean and falsified accuracy than TRADES but are significantly easier to verify. SABR achieves slightly better performance due to less regularization by propagating smaller intervals. For SVHN, SABR has lower verified accuracy than IBP, indicating that stronger verification algorithms are required. Our set- based training strikes a balance between TRADES and interval- based approaches, with significantly higher verified accuracy compared to TRADES and higher clean and falsified accuracy compared to IBP and SABR.
15

---

Published in Transactions on Machine Learning Research (08/2025)
Table Performance on MNIST for different weighting factors the set-based loss (Def.
Method
clean Acc.
falsified Acc.
fast-verified Acc. (max)
Set (r = 0.0)
98.87 0.01
96.48 + 0.18
89.40 0.58
(90.04)
Set (T = 0.01)
98.74 0.07
96.77
93.45 0.47
(93.73)
Set (r = -0.1)
97.57+000 0.09
95.60+0.11
94.03 + 0.04
(94.06)
Set (r = 0.2)
0.017
9..0
93.70 = 0.12
(93.82)
Set (T 0.3)
96.59
93.46 1.20
88.91 + 4.36
(93.95)
Table 3: Performance on MNIST of different input sets.
Method
clean Acc.
fast-verified Acc. (max)
Set (fee) Set (FGSM)
97.58 + 0.03
93.83 0.06
(93.89) (94.06)
97.57 = 0.09
94.03 0.04
5.2 Understanding Robustness
To better understand the robustness of neural networks, compare the learned decision boundaries of standard (point-basod) and set- training for simple binary classification task (Fig. 7 Both training methods learn the training data perfectly, but set-based training pushes the decision boundaries away from the samples, making the set-based-trained model more robust. For some samples, the decision boundary of the point-based trained neural network crossos their perturbation sets, which is not the case for the tra-beeed-trained neural network.
5.3 Ablation Studies
We conduct ablation studies to justify our design choices. Please refer to Appendix A for details.
Weighting of Robustness Loss It has been shown that there is a fundamental tradeoff between accuracy and robustness (Zhang et al. 2019). The weighting factor T in our set-based loss (Def. 5 can trade off accuracy with robustness. Tab. shows the accuracies for different values of 7: For smaller values of т, the clean accuracy is larger, and the verified accuracy is larger for larger values. Thus, this hyperparameter can used to tune the tradeoff between accuracy and robustness.
Input Set Compared to other robust training approaches (Gowal et al. 2019 Müller et al. 2023 Mao
et al. 2023), our set-based training is not limited to multi-dimensional intervals as input sets. In Tab. we compare using the ball as an input set with a smaller input zonotope where the generators are computed using adversarial attacks (see Appendix A for details). The smaller input set leads to better performance; thereby, we confirm the obscrvations from previous works (Müller al. 2023) that smaller input sets reduce the regularization by creating smaller approximation errors and thus resulting in better performance.
Set- Set-Propagation Method We compare the propagation of zonotopes with our image enclosure to other set propagation methods during our set-based training (Tab. 4 IBP, zonotopes with Singh's 's enclosure, and zonotopes with our enclosure (Prop. 6 The results support our choice of enclosure as it consistently obtains higher accuracies than the other enclosures. This is due to the smaller accumulated approximation errors (Prop. II Thus, we observe that our enclosure produces the best results, justifying the use of zonotopes for our image enclosure.
Size of the Output Sets and Robustness In Tab. we compare the size of the output sets (of the first 1000 test samples) and the Lipschitz constant of the best performing neural networks trained on MNIST. The Lipschitz constant of a neural network is another metric for robustness, because bounds the sensitivity of the neural wotwork for input changes (Fazlyab et al. 2019). Moreover, compare the interval norm (Althoff
16

---

Published in Transactions on Machine Learning Research (08/2025)
Table 4: Performance on MNIST of different set propagation methods.
Method
clean Acc.
falsified Acc.
fast-verified Acc. (max)
Set (Zonotope+ours)
98.60 0.21
97.13 + 0.13
96.13
(96.25)
Set (Zonotope+-Singh)
98.36 0.13
96.60 0.59
94.4
(96.04)
Set (IBP)
97.77 0.19
96.11 0.20
95.35
(95.62)
Table 5: Comparing the sizes of the output sets and Lipschitz for different training methods.
Method
Size (Interval Norm)
Lipschitz Constant
TRADES
276.36 120.40
9.72 10
IBP
4.77 + 1.96
2.78 10
SABR
5.26 2.39
4.20 10
Set (ours)
1.85 + 1.27
3.49 10
Sec. 3.1) of the output set, because computing the volume of zonotope is computationally hard. 2023
The Lipschiz constant of the TRADES-trained network is the smallest, which explains the great empirical robustness (falsified Acc. in Tab. [; however, the output sels are too large for verification (fast-verified Acc. in Tab. D Our set-based-trained neural network produces the smallest output sets and a smaller Lipschitz constant compared to IBP and SABR.
6 Conclusion
This paper introduces the first set-based training procedure for neural networks that uses gradient sets: During training, we enclose the output of the neural network using set propagation and derive gradient set, which contains a different gradient for each possible output. By choosing gradients that point to the center of the output set, improve robustness and simplify the formal verification. The set-based training is made batch-wise, and differentiable propagation of zonolopes, which utilizes analytical solutions for approximation errors. Our experimental results demonstrate that our set-based approach effectively trains robust neural networks, which have competitive performance and admit fast verification (in polynomial time). Thereby, we demonstrate that gradient sets can be effectively used to train robust neural networks. Hence, set- based training represents promising new direction for robust neural network training and significant. step toward fast verification of neural networks and, thus, the widespread adoption of formal verification of neural networks.
simultaneously directly reduce the size of the output set. Thereby, possible by a fast,
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). We also want to thank our colleague Mark Wetzlinger from our research group for his revisions of the manuscript.
References
Matthias Althoff. Reachability analysis and its opplication 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. Checking and establishing reachset conformance in CORA 2023. In ARCH Workshop, pp. 9 33, 2023.
17

---

Published in Transactions on Machine Learning Research (08/2025)
Mislav Bahunovíć and Martin Vechev. Adversarial training and provable defenses: Bridging the gap. In
TCLR, 2020.
Christopher M. Bishop. Pattern recognition and machine learning. Springer New York, NY, 2006.
Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (VNN-COMP). STTT, 25(3):329 339, 2023.
Christopher Brix, Stanley Bak, Taylor Johnson, and Haoze Wu. The fifth international verification of neural networks competition (VNN-COMP 2024): Summary and results. arXiv preprinl 112 19985, 2024.
Rudy Bunel, Tlker Turkaslan, Philip H. S. Torr, M. Pawan Kumar, Jingyue Lu, and Pushmeet Kohli. Branch and bound for piecewise linear neural network verification. J. Mach. Learn. Res., 21(1):1 39, 2020.
Christophe Combastel. Zonotopes and Kalman observers: Gain optimality under distinct uncertainty paradigms and robust convergence. Automatica, 55:265-273, 2015.
Serge Durand, Augustin Lemesle, Zakaria Chihani, Caterina Urban, and François Terrier. ReCIPH: Rela- tional coefficients for input partitioning heuristic. In WFVMI, 2022.
György Flekes. A geometric inequality and the complexity of computing volume. Discrete Comput. Geom.. 1(4):289 292, 1986.
Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George Pappas. Efficient and accurate estimation of Lipschitz constants for deep neural networks. In NearIPS, 2019.
Claudio Ferrari, Mark Niklas Müller, Nikola Jovanović, and Martin Vechev. Complete verification via multi- neuron relaxation guided branch-and-bounn bound. In ICLR, 2022.
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. AI2: Safety and robustness certification of neural networks with abstract interpretation. In IEEE SSP, pp. 3 18, 2018.
Antoine Girard. Reachability of uncertain linear systems using zonotopes. In HSCC, pp. 291 305, 2005.
Xavier Glorot and Yoshua Bengio. Understanding the difficulty of training deep feedforward neural networks. In AISTATS, pp. 249-256, 2010.
Ian Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. ICLR, 2015.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovie, Timothy Arthur Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In ICCV, pp. 4841-4850, 2019.
Geoffrey Hinton, Li Deng, Dong Yu, George E. Dahl, AbdeIrahman Mohamed, Navdeep Jaitly, Andrew Senior, Vincent Vanhoucke, Patrick Nguyen, Tara N. Sainath, and Brian Kingsbury. Deep neural networks for acoustic modeling in speech recognition: The shared views of four research groups. IEEE Signal Process. Mag., (6))):82 97, 2012.
Ahmed Trfan, Kyle D. Julian, Haoze Wu, Clark Barrett, Mykel J. Kochenderfer, Baoluo Meng, and James Lopez. Towards verification of neural networks for small unmanned aircraft collision avoidance. In DASC, pp. 1-10, 2020.
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.
Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. In ICLR, 2015.
18

---

Published in Transactions on Machine Learning Research (08/2025)
Niklas Kochdumper, Christian Schilling, Matthias Althoff, and Stanley Bak. Open- and closed-loop neural network verification using polynomial konotopes. In NFM, pp. 16-36, 2023.
Alex Krizhevsky. Learning multiple layers of features from tiny images. Technical report, Computer Science Department, University of Toronto, 2009.
Alexcy Kurakin, Ian Goodfellow, and Samy Bengio. Adversarial machine learning 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.
Ya Le and Xuan Yang. Tiny ImageNet visual recognition challenge. CS 231N, 7(7):3 2015.
Yann LeCun, Corinna Cortes, and CJ Burges. MNIST handwritten digit database. ATT Labs [Online]. Available: http://yann.. lecun.
wwwwwe.ww./eeeeeeeeeeee....eeeee com/eoddeeeee (exdb/mniss 2, 2010.
Augustin Lemesle, Julien Lehmann, and Tristan Le Gall. Neural network verification with PyRAT. arXiv preprint arXtt:2410.2390,, 2024.
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In ICLR, 2018.
Yuhao Mao, Mark Müller, Mare Fischer, and Martin Vechev. Connecting certified and adversarial training. In NeurIPS, pp. 73422-73440, 2023.
Matthew Mirman, Timon Gchr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In ICML, pp. 3578 3586, 2018.
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, 2022.
Mark Niklas Müller, Franziska Eckert, Mare Fischer, and Martin Vechev. Certified training: Small boxes are all you need. In ICLR, 2023.
Yuval Netzer, Tao Wang, Adam Coates, Alessandro Bissacco, Bo Wu, and Andrew Y. Ng. Reading digits in natural images with unsupervised feature learning. In NIPS, 2011.
Zhouxing Shi, Yihan Wang, Huan Zhang, Jinfeng Yi, and Cho-Jui Hsieh. Fast certified robust training with short warmup. In NeurIPS, pp. 18335-18349, 2021.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In NeurIPS, 2018.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. PACMPL, 3:1-30, 2019a
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification of neural networks. In ICLR, 2019b.
Christian Szegedy, Wojeiech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. In ICLR, 2014.
Chien-Yao Wang, Alexey Bochkovskiy, and Hong- Yuan Mark Liao. YOLOv7: Trainable bag-of-freebies sets new state-of-the-art for real-time object detectors. In CVPR, pp. 7464-7475, 2023.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsich, and Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. NewrIPS, $4:29909-2990 2021.
19

---

Published in Transactions on Machine Learning Research (08/2025)
Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsich, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for ReLU networks. In ICML, pp. 2018.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In ICML, pp. 5286 5295, 2018.
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: versatile formal analyzer of neural networks. In CAV, pp. 249-264, 2024.
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsich. Automatic perturbation analysis for scalable certified robustness and beyond. In NewrIPS, volume 33, pp. 1129 1141, 2020.
Cunliang Ye, Yongfu Wang, Yunlong Wang, and Ming Tie. Steering angle prediction YOLOv5- end-to- end adaptive neural network control for autonomous vehicles. Proc. Inst. Mech. Eng., 236(9):1991-2))) 1911-2011, 2022.
Hongvang Zhang, Yaodong Yu, Jiantao Jiao, Eric Xing, Laurent El Ghaoui, and Michael Jordan. The- orctically principled trade-off between robustness and accuracy. In ICML, volume 97, pp. 7472-7482, 2019.
Huan Zhang, Tsui- Wei Weng, Pin- Yu Chen, Cho-Jui Hsieh, and Luea Daniel. Efficient neural network robustness certification with general activation functions. In NewrIPS, pp. 4944-4953, 2018
Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane S. Boning, and Cho-Jui Hsich. Towards stable and efficient training of verifiably robust neural networks. In ICLR, 2020.
Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsich, and J Zico Kolter. General cutting planes for
neural network verification. NewrIPS, pp. 1656 1670, 2022.
A Evaluation Details
Hardware Our experiments were run on a server with 2xAMD EPYC 7763 (64 cores/128 threads), 2TB RAM, and NVIDIA A100 40GB GPU.
Training Hyperparameters The training hyperparameters are listed in Tab. 6 and the neural network
architectures in Tab. 7 We use the same notation as (Gowal et al. 2019): Coxv w x h + denotes a convolutional layer with & filters of size w x h and stide 8, and Fcn denotes a fully connected layer with n neurons. The weights and biases are initialized as in (Shi et al. 2021). We use Adam optimizer (Kingmaa & Ba 2015) with the recommended hyperparameterss. For all training methods, we tried to use hyperparameters as close as possible the reported hyperparameters in their respective paper: for (Gowal al. 2019 we use 1/2, for (Zhang et al., 2019 use 1/2 6, for (Mäller al. 2023) we use X = 0.1 for CIFAR-10 10.
and À = 0.4 for MNIST and SVHN. For any PGD during training (used by methods (Madry et al. 2018
Zhang et al. 2019 Müller et al. 2023 we used the settings from (Mäller et al. 2023): 8 iiterations with an initial step size 0.5, which is decayed twice by 0.1 at iterations 4 and 7. All PGD allacks for lesting are computed with 40 iterations of step size 0.01. Moreover, all reported accuracies are averaged over the best of 5 runs. We clip gradients with a fz-norm of greater than 10. All reported perturbation radii are w.r.t. normalized inputs between and 1. To reduce computational resources, we performed the ablation studies with a smaller layer convolutional neural network trained on MNIST.
20

---

Published in Transactions on Machine Learning Research (08/2025)
Table 6: Training hyperparameters.
# #Epochs
Dataset
7
Batch Size
(warmmup / ramp-up)
Decay
MNIST
5 10-4
0.1
0.1
256
70 (1/20)
50, 60
CIFAR-10
5 5-10-1
2/255
0.005
128
160 (40/ (40/120) 120)
120, 140
SVHN
5.10-1
0.01
0.01
128
70 (20 /50/
50, 60
TINYIMAGENET
5- 10-
1/255
0.1
64
70 (20/50)
50, 60
Table 7: Neural network architectures. Each linear layer convolutional layer (except the last layer) is followed by batch normalization and nonlinear activation layer (ReLU).
CNN3
CNN6
CONV +2
CONV 32 3
CONV 10 4+1
CoNv 32 4 x 4+2
FC 100
CoNv 64 1
CoNv 64 x 4+2
Fc 512
FC512
Datasets MNIST contains 60 000 grayscale images of size 28 28. Each image depicts handwritten digit from 0 to 9. SVHN is real-world dataset that contains 73 257 colored images of digits of house numbers that are cropped to size 32 x 32. The CIFAR-10 10 dataset contains 60 000 colored images of size 32 x 32. The TINYIMAGENET data set contains 100 colored images of size 64 x 64 labeled with 200 classes. We use the canonical split of training and test data for each dataset and the entire test data for evaluation; because test labels are not available for TINYIMAGENET, we follow (Müller et al., 2023) and use the validation set for testing. Following (Xu et al., 2020 augment the CIFAR-10 and TINYIMAGENe: dataset with random crop and flips. The perturbation applied before the normalization to ensure comparability with the literature.
Improvements for Scalability The complexity of our set-based training depends on the number of generators of the output set used during training (Prop. 17). We use two methods reduce the number of generators: (i) We propagate the approximation errors intervals through the neural network and compute the Minkowski sum at the end. (ii) We use input sets with fewer number of generators. Our set-based training any zonotopic input set and is not limited to -n-in sets. Building on previous work (Müller et al, 2023), we use adversarial attacks to construct smaller input sets that focus on critical regions of the input; thereby, the regularization through large approximation errors is reduced. Previous works only use a single adversarial attack to construct a smaller input set (Mülee et al.) 2023). We extend this idea and use several adversarial attacks to construct zonotopic input sets: We shift the center of the input set the average attack and use scaled directions of the attacks as gencrators for the input set. Given an input o, for [A] (e.g,, using FGSM). The input set is
E RR"o, we compute adversarial atlacks z; constructed
X'
1/x
Σ
82
5x]
Fairness We note that compared to the litcrature, we use smaller neural networks and compare the mcans across several training runs; most. literature only reports their best-observed scores, which is problematic regarding reprodueibility and fairness because it unclear how many training seeds were used. Therefore, create fair comparison, we have reimplemented related approaches (Madry et al. 2018) Gowal et al. 2019 Zhang et al. 2019 Müller et al. 2023). The implementations have been validated by reproducing their reported results.
21

---

Published in Transactions on Machine Learning Research (08/2025)
Table 8: Comparing the maximum perturbation radius.
Method
(max)
TRADES
0.0715
(0.1094)
IBP
0.1856
(0.2441)
SABR
0.1792
(0.2422)
Set (ours)
0.1782 + 0.0494 (0.2676)
Table 9: Performance on CIFAR10 for different weighting factors in the set-based loss (Def.
Method
clean Acc.
falsified Acc.
fast-verified Acc. (max)
Set (T 0.0)
61.42 + 1.12
0.660
31.98 = 0.61
(32.53)
Set (r 0.005)
59.95 + 1.13
50.89 + 0.64
38.50 + 0.32
(38.87)
Set (T 0.01)
59.29 0.99
50.37 + 0.76
3..59
(39.92)
Set (T 0.05)
0.79
18.80+0.46
0.11
(41.24)
Set (T 0.1)
47.90 5..9
(41.87)
Sct (T 0.2)
1.18
45.05 0.83
40.08
(40.49)
Set (T 0.3)
1.77
41.29 1.51
36.13
(38.23)
B Additional Experiments
Maximum Porturbation Radius In Tab. 8 we compare the maximal perturbation radius for which wo can verify the robustness. We used binary search (10 iterations) to compute the maximum perturbation radius for the first 1000 test samples of the MNIST dataset. The perturbation radii of IBP, SABR, and Set are comparable and significantly higher compared TRADES.
Weighting of Robustness Loss the CIFAR10 dataset.
Tab.
shows the accuracies for different values of of CNN3 trained
Pet-Propagation Method Tab. gation methods.
T0 shows the results of CNN6 trained on MNIST for different set propa-
Training Times The training times compared in Tab. 11 The computational overhead of set-based training is slightly higher than TRADES, IBP, and SABR. However, the TRADES-trained neural networks have great empirical performance (clean and falsified accuracy Tab. T but cannot be verified using polyno- mial time verification approaches (fast-verified accuracy Tab. 1 IBP and SABR have significantly lower empirical performance compared to TRADES. Our set-based trained neural networks have higher empirical performance compared to IBP and SABR and have great verified robustness (fast-verified accuracy Tab, I. Moreover, with our set-based training, we can use weighting parameter in the set-based loss to explic- itly tune the tradeoff between empirical performance and verified robustness. Therefore, set-based training strikes balance between training time, empirical performance, and verified robustness.
C Reproducibility of Fig. 7
Fig. compares the decision boundaries of point- and a set-based training neural network for a binary classification task. The network architecture is nn-med: layers with 100 neurons each. The training
22

---

Published in Transactions on Machine Learning Research (08/2025)
Table 10: Performance of CNN6 on MNIST different propagation methods.
Method
clean Acc.
falsified Acc.
fast-verified Acc. (max)
Set (Zonotope+ours)
98.66 0.02
97.71 0.08
97.08 0.08
(97.15)
Sct (Zonotope+-Singh)
98.13 0.88
97.61 0.19
96.88 0.19
(97.08)
Set (IBP)
98.08 0.08
96.60 = 0.21
95.96 0.21
(96.11)
Table 11: Training time with CNN6 MNIST (min. of runs) |sec Epoch].
Method Training Time [sec / Epoch]())
Point
6.1
TRADES
49.6
IBP
19.9
SABR
52.0
Set (ours)
61.2
data are 20 random input samples rı E [0, 1]2 with corresponding targets t; E {0,
{[[ 0.0622
[[]): ([ 0.6534
[9])
0.4759
[b]) ([ 0.8812
[ [b]) ([ 0.5047
(1)
0.6995
[.9409
0.7163
0.10020
(.46685
([ ((0.3278)
00.1470
[1]]. 0.3439
([
[t]) 0.9098
[Q]) ([)))((()))) ([0.5596 [00.8588
[B]) ([
[.00545
[0]
[.3225
0..1395
0.5422
(...669)
0.0825
([ [0.889
[0]) ([0.283)
[.9992
[t]):
0.6781
[1]) ([ [0044411
([0.3940))
[f]). ([0 [0.4575
0.44771
0.2857
0..0033
0.3302
0...487
0.1222
[b]).
0.6506
[1])
0.5207
[b]) (( 0.3271
[8))
0.68588 ([0.6853
[00)
0.4699
0.1129
0.0616
We train both neural networks for 200 epochs with mini-batch size of 10 using the Adam optimizer with learning rate of r = 0.01. For set-based training, we use c 0.05 with T = 0.1.
D Proofs
Proposition
Given an output set y = (cx, GRdz C TR=,, the gradient of the F-radius is
Vy|Di/| (0, The || Gx Gx)
1
Proof. The center does not affect the F-radius, hence V., ||]|= = 0. The F-radius is the sum of all squared entries the generator matrix. Hence,
Gx
VG, 1DIFF = Th
Vo. VO.VIT IT (Gx GG. Th ||
(13)
Thus,
Def.
(ee ||'l, Va, 1)))))
13
0, nr
Gx
1
(0, Go))z)
||'||
nx ||
Proposition
(Set-Based Loss Gradient). Given an output set (cas Gx) C Th the gradient of the set-based loss function is
VyL(t,)) = (1--) V(, 7 e nw ||11F
1(1)))aa))))
1
Gx
23

---

Published in Transactions on Machine Learning Research (08/202))
E
Output
2 ds
I
Input
Our Enclosure
Singh's 's Enclosure
Figure Illustration for Prop.
Proof. This follows from Def. 5 and Prop.
V),((,)) Def. 5
7) VyL(I, ex)
T V>DDiil
Def. 8
(1 (1-7) ((1,e,,, 0) - 1>/10//1
Prop.
(1 (1-71h L(t Ltt, + en 12
(0. Gn)
(1-- Ve, C(t, T
enx |ill Gn Gm))
Proposition
10
The approrimation error of p for & E (ReLU, tanh, of are computed as
min <0x) -p(x), zEPon(L.v)
max ZEPon(L.))
6(x) - p(x),
where
= (0, (0,
Pranh { tanh (V1 tanh-
1,
Pa = {+2 tanh tanh (V1-4 4m) ul,
Proof. Case (i). o = ReLU. ReLU(x) p(x) is linear for 1, and [0, u]. Thus, the approximation errors are found the bounds x (1, u} or where e
x =0
Case (ti). o tanh. The derivative of the hyperbolic tangent is tanh' (x) = 1 - tanh(z)2 To compute the extreme points of tanh(x) - p(z), we demand that its derivative is O and simplify the terms:
0 d/zz(tanh(z)) p(x))
0= 1 tanh(x)))
+ tanh (V1-m) m).
Case (iii). Φ = o. To compute the extreme points of a(x) - p(x), we demand that its derivative and simplify the terms:
0 = d/arlo(()) - p(x))
0 = ////////////// (tanh + + p(x))
= -= +2 tanh (V1 mm) O
Proposition
Let & be an s-shaped function, and let [t, u] be interval. Moreover, let le, e] be the approzimation errors of our enclosure (Def. 6 and 7 and let es be the approzimation error of Singh 's enclosure (Singh et al. 2018 Thm. 3.2). holds that
11
area((s,e) e), (1, w]) s area([-es, es), 1,,)).
24

---

Published in Transactions on Machine Learning Research (08/2025)
Proof. We first observe that the approximation errors and of p be computed at points Σ, [1, such that x S x (Fig. 8
e (zz) - p((),
z= -
(14)
Singh's enclosure (Singh et al. 2018 Thm. 3.2) uses the linear approximation ps(x) = mg x + ds, with slope mig offset ds, and approximation error eg:
mg mi)( (l) (u)), ds = 1/2 (d(u) + o(1) my (u 1)),
es 1/2(((u) x(1) ms (u 1)). (15)
Using Def. we obtain the following inequality:
m ((u) - (1)
1 ms.
Hence, we have
m [T - 2n) 2 ms (T z)
(16)
Morcover, from
we have for all x E [1, u]:
((x) +() 2 ms (x [) - )(z) 2 x(1) + ms (I 1--1 1),
(17)
o(u) - 6(x) 2 ms (u x) = (()) S ((u) mg (u T).
Ultimately, we have
14
(<>) 2 - p(z) - (Φ(x)) p(x))
Def. (xx) (mx) - (δ(x) (m z2)
(18)
6 2 ((x) ms (i x)
Φ(u) ms (u 3) (0(1) ms (r 1)) mm (x x))
2 eg.
Hence, we obtain the bound ē - 2 eg. Thus,
10
10
area ( E]. 1, ul)
(u 1) (ī
(u 1) 2es
area es], (1,
Proposition 12 (Backpropagation through Image Enclosure). Assume the k-th layer is nonlinear layer
with activation function ob. Given an input set H4-1 = (ck-1, Gk-1)z with Gk-1 E 12s-1Xp and a gradient set Gp = (ck, Gi) 2 the gradient set Gz-1 -ch-1; (C is computed for each dimension i E [mg] as
Gk GR-1(() -ma(s) Gu(iy (chess CK-1(1) + Ghee. Gk-(ie)) Vuu- MR(i)
(c40)) + GR((Dtt) VHa-i (M(1 + 2 (Che)) - Gh(int)) VHe-
+
The operation Gk-1 = backpropEnncoose (ok. Gk) computes the gradient set of an image enclosure.
Proof. The image enclosure adds nę generators, hence the input set H4-1 has ny generators less than gradient set Gk, i.e. Gk-1 E R and G² R==xq with g = p + ni.
We unfold I1 and rewrite the gradient set Gk-1 using the chain rule for partial derivatives. Let H4 (cx, Ga)z with Gş E R be the output set of the k-th layer and let G (c2, Gx)z be the gradient set w.r.t. Hy:
nu ac(t,))
nk 9
aC(t,)) aGk(H
Gk-1
VHE [(t,))
VHe_, (k(()
VHe-, GR(so)
dep(s)
(19)
VHa-1 Ck(i) +
((t)
1=1 1=1
25

---

Published in Transactions on Machine Learning Research (08/2025)
We split 19 into three summands:
1R- Σ
((1) VHu-i Ck(f3s
1=1
-
Ga(ts)) GH(Li
i=1 1=1
Gk-14-
Σ
Gk(l,) Vitzi GR(ss)
am
jupt1
Hence,
Gk-1 = Gk-1,e Gk-1, + gk 1,g
(20)
Furthermore, the input set H is enclosed by the interval [1=-1, uk-1), 1], where 44-1 Ck-1 |Ga 1 and Ug-1 + GG (Prop.
Firstly, we derive the gradient VHN-i Ck() needed for I for which we need the gradients of center Ck(s) = m)()) (k-1(s) + 1/2 (Ex()) + (x())) w.r.t. the input set Hx-1 for each dimension [ng]. The image enclosure is applied for each dimension individually; therefore, we can consider each dimension separately because for any dimensions i,j [m where *
VH Ck(s) 2)
VH Gk(L,) Z)
(21)
Let E [nx] be a fixed dimension and [p] fixed index of generator. We require the gradient of the slope mz) and the offset (,,(()) The gradient of the slope mi(s) is:
0mp()
Def. (()) 05 (1)-1(1)) Uk-1(() - -x11(())
0ck-1(0)
dmz())
o' (())) + Ø (1(22-168) - 2 m
sign(Gx-1(.)))
(Gk-1().))
Uk-1(1) (=1(())
Let T3 and Zy be the points of the approximation errors En and ex:
arg max (x: (x:)
Fg arg min (x(x) (x()
xEP
aEP
To prevent repetitions in this proof, let denote the center, or an arbitrary generator of the input set Hg-1
{ck-1, GR- Gk- ((-2) ... GR- GR-1
For (z E {(Tx, ex), (Ig, }.),, we apply the chain rule and the product-rule to derive the gradients of the approximation error e())
dem (((((()) mx(a) 2(0)
Oz 8m4)()
(01(((()) - - Age)
z(a)-
0g(
Ogi
Og(a)
Using the gradient of the slope mx(s); we derive the gradient of the center Cx(S);
a (a))) Ck- 106) + 1 (((()) + + m)()) + Ock-1(0)
Ock(s)
@mp())
Fex())
Ck-1(1)
0ck-1(6)
Ock-1())
Ock-1(0)
Oca-1(0) 1()-(())
a ((mA()) Ck-1()) + (b(0) + EM()))
dcx())
0ma(s
deR(1)
dEN(i)
Ck-1(6) +
+ 8Gk-1(15)
0Gt-1(i.))
@Gk-1(i5)
0G
2 @G
26

---

Published in Transactions on Machine Learning Research (08/2025)
Hence, we have
(
dck(t)
Ock(s)
Ht 166) Ck(i)
dck-1(s) 165) -
(22)
= =mb()) + Ck-1(t) VHa-iro mk(() + 1 (Han-10 Ck(() + VH (H Ex(0)
Secondly, we derive the gradient Vi GR(ag) needed for G8-1x. Let j' E [na] be different generator index: j' * j: the gradient of Gn(sS) is
@Gk(1.)
((mx()) Gk-1(b.))
@mz(()
GR-1((a))
0cz-1(6)
Ocx-1())
Ocg-((1) 1(1)
0Gk(1.)
(m)(())
Gk-1(6.)) mk(i) + 0Gk-1(15))
@mp())
Gk-1(id))
(Gk-1(15)
aGk-1(id)
dGR(S.)
((m(i))
Gk-1((.))) 0mz()) Gk-1((i))
0Gk-1(6d")
(Gk-1(1o")
0Gk-1(id")
Hence, we have
0cx-1(0) aGR- ) = Gk-I((i)) VH ma(e) + mx()) (0, (6.)))
@GG((s)) aGk(i.)
VHy 1053 GR((d))
(23)
where ((i E {0,1] is a matrix containing only zeros except for position (i,j) which contains a one.
Thirdly, we derive Gx-1.g- Please recall, the diagonal entries of GR(sp+(ne)) contain the approximation errors, while the non-diagonal entries are 0; hence, the gradient of any non-diagonal entry j' [4]: j' pAj # p+i is O: VHe-1co GR(ad") (0, 2- Hence,
simplify Gk-1.g¹
GR-1,0()= = Σ GRoan VHu-u GR(Ln = Gkistt)) 2 (HHLLLO ER(() (H1-2
1
(24)
3=p+1
We add Gk-1e and 1 followed by reordering the terms:
Gx-1,0(0) 9k-1,p()) Ce(s)
VHe- Ck(() + Σ Gh(i,)) VHE-sCo GR(ld)
22
deee)
mx(1)) - ck-1(() VHa- + (VHL-1o)ER0) Ex() + (0)-1190((8)
p
Gloco,3) VHa-10
1=1
23
CR(s)
mik(s) + ck-1(3) VHe- Mk(s) + 2
1 (Hu-noy ER(1) + VHL-1090M33)
(25)
Ga (Go-1(i)) V + mx(e) (0. 1(()))))
=ma() IK(o) + (C--1(0) dhe)
Ch0) + Gk-1(t)) Go(A)o)) VHe-io mz(4)
1 + cke0 2 (He-no0, Ek(A) + VHa-n(
27

---

Published in Transactions on Machine Learning Research (08/2025)
Finally, we obtain
20
GR ((4)
Gh- Gk-1,ct0) + 9x-1,p(0) + 9 1k-1,1())
mu(s) GN(i) (G--1()) + ((((,)))) (1-1(())) VHe-nc mM10) + (233) VHe (cb()) + 9k-1,(00)
24
mk(i) GK(S) + (CE-161) da) + Gk((,e))) Gk-1(1.)) VHe-sco
1 c4())
(VHte 1631 Ek(1) + Vn, un ex()) + G'((sott)) 1
(Vn, 10 Ex(1) Vuyy 100 Ck(3))
2
= =mx()) GK(E) + (ck-1(0) 40( + ((())))) Gk-1(1)) Vie-sio MA(())
+ 1 (e()) + (h(pp)))) Vun ue) (n()) (ca(s) - -Cu(sott) Vua 160 Ck())
Proposition 13 (Set-Based Backpropagation).
The gradient sets Gr are computed in reverse order as
W 9z
if k-th layer is linear, otherwise,
9N = V)((t,)),
Gx-1
backprop@hncooso@le....
for k = K. 18 - 1, 1,
Proof. If k n. we compute the gradient of the set-based loss according to Prop. === (c2, Gk)z and H2 (ck, Gk)z.
We assume & < Let
We split cases the type of the k-th layer and simplify the terms.
Case (t). The k-th layer is linear. For dimension E [nx], we have
-( (WiT (WALn.):)) 0)2
VnL-, VHE-, (Wa(i.) ck-1 + bx(t)) = VHt- Gk(ld) VHE- (Wa(i.) Gk-1(-51) (0, WA(s.) o, 7)2
(26)
Thus,
Gk-1
19
GolD) VH Ck(s)
Gk()d) FHa-IGR(s
1=1
i=1
12
9
Goe (W.. ()
Ch 00, WT k(c))) c7)
==
nk
((.) 6e(0)
Σ 2=1
W Gh(e.))
(WT dr Wi. Gk)zz
Wi. Ge.
Case (ti). The k-th layer is nonlinear. Prop.
12
proves the correctness.
Proposition 14
Gradient Set w.r.t. Weights and Bias). The gradients of the set-based loss w.r.t. weight matrix and bias vector are
Vw. Vw. ((,))) VH. C(1,)) H
0 Vo, VH. = (1, (1,0)
28

---

Published in Transactions on Machine Learning Research (08/2025)
Proof. We rewrite the gradient by applying the chain rule for partial derivatives:
(w,C(t,)))
Σ
Se0 Vwe Ck(1 +
GRRss Vw, Gk(I)))))
1=1
Vbg ((t,))
660 Vb, Ck(i) +
Ch(s,)) Vog GR(E5)
where G5 E R Morcover, we have for dimension E [nx] and generator index j E [g]:
Vw, Ck(1) = Vwi C--1 + bu(s)) = e Ck-11
Vw, Gua,) = Vw, (WA(L.) Gk- Gk-1(-5)) = e, GK-1(-))
Vo, Ck(1) Vb, (WA(L.) Ck-1 bu(t)) Gi,
Vo, GR(BR)) Vo, (Wa(L.) Gk-1(-J)) 0,
where e, {0, 13mh is the i-th standard basis vector. Thus,
Vw. = de ch + G2 Gk-1 9k ① Hz-11
Vo, C(t,)) = de = - (1,0)
Proposition 15. For an input set Ha-1 2 with E Thn and G E Raxq, Alg. has time complerity O(n" 9) w.r.t. the number of imput dimensions n and the number of generators q-
Proof. Finding the interval bounds of H (line 2 takes time ((n (Prop. 2 Computing the linear
approximation (line and the approximation errors (linc 5) for each ncuron takes constant time; honce,
the loop takes time On)). The linear map of Hx-1 (line G takes time O(n² q) (Prop. 4h. Adding the
approximation errors (line takes time (()). Thus, total we have O(n + O()) O(n q) + O(n) = O(n²g) g).
The zonotopes during a forward propogation (Prop. have most q S no Ekeial nig generators. Let Tmaz == maxke]e] nu be the marimum number of neurons in a layer. The set-based forward propagtion (Prop. 6) has time complerity O(n k) w.r.t. Rmmaz q and the number of layers
Proposition 16
Proof. The initial e-perturbance set has no generators (line 1 and every nonlinear layer adds n& gener- ators for the approximation errors (Alg. D. Moreover, there are al most k. nonlinear layers. Thus, in total, there are at most (no + EkEldl n4) generators.
Time Complexity: The k-th step of the set-based forward propagation takes time O( q): The linear map (line 4 well as the image enclosure (line 6) takes time O(n n& 9) (n 9) (Prop. and 15
Thus, the set-based forward propagation (lines 6 takes time On q).
Proposition 17 Alg- 2 has time complenity O On w.r.t. Mmnax q and the namber of layers
Proof. The set-based forward propagation (lines 26 takes time O( 7) (Prop. 16 The gradient of the set-based loss has (nw + n, entries, and the computation of each entry takes constant time; hence, computing the gradient takes time On,, + n2 4). The k-th step of the set-based backpropagation takes at most. O(n--1 fig q) = On q) time: a linear layer computes a linear map (line 11 which takes time O 71. q) (Prop. 4p. and the set-based backpropagation of an image enclosure (line 15 takes time O m) (Prop. (2). Hence, the set-based backpropagation (lines g 15 takes time x (n q). Updat- ing a weight matrix takes time O 17k + R 71 q) O 9) (line 12) and updating bias vector takes time ((p))= = O(mmax) (line 13 There
at most linear layers; hence, updating the weight matrix and bias vector of all linear layers takes time K (O 9) + O()max)) k ( g). Thus, in total, an iteration of beteb training takes time 3 n. O On max y k) O g k)).
29


Reviews:
[{"review_id": "DIllmtR1xw", "reviewer": "Reviewer_4XbV", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "The paper is well-presented and quite easy to follow, considering the quite technical nature of the content. The authors have done an above-average job in this respect.\n\nIn my view, the main contribution of this paper is a novel approach for bounding the approximation errors of the linearised activation function, resulting in better zonotope propagation through non-linear layers. The benefits of this approach over the well-known method of Singh et al. (2018) are demonstrated quite convincingly at an intuitive level, although the benefits seem to be limited in the experimental setup considered by the authors.\n\nWhile the set-based training is also interesting, I think there is a lack of meaningful justification for the proposed loss, beyond how it enables one to do set-based training. It would be nice to see it tied to the usual justifications used for motivating a particular loss function (e.g., cross entropy corresponds to maximum likelihood estimation under categorical likelihood, hinge loss upper bounds zero-one loss, etc). From what I can tell the typical approach of taking the maximum loss inside the zonotope will also cause the F-radius of the zonotope to decrease, and it also provides an upper bound to the adversarial loss. Is there is a reason why integrating over the whole zonotope would be more useful in practice? Since it computes an average instead of a maximum, could it result in less robust models?\n\nThere are a few other places where I think the experiments could be improved. In particular:\n* I would have liked to see how the method scales compared to other approaches as the networks are made deeper---is there a point where the errors introduced by the enclosures compound to the point where this approach is no longer viable? If so, is that point substantially later than when the bound of Singh et al. (2018) is used?\n* Ablations are performed on MNIST, a dataset where linear models can already achieve quite high accuracy. In this case, I suspect the overapproximation discussed in Sec 4.1 is not a big problem. Is there a more noticeably difference in performance when more difficult datasets are used for ablations?\n* It is generally good practice to investigate how sensitive adversarial defences are to the exact choice of $\\epsilon$.\n* Adversarial training is very effective in practice, but lacks guarantees; if adversarial training is used to train the network, can the proposed approach provide meaningful guarantees?", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "No", "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": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper proposes a set-based training approach for promoting verifiable adversarial robustness in neural networks. A novel technique for propagating zonotopes through neural networks is provided, enabled by the introduction of a novel loss function. An experimental comparison with other formal methods approaches is provided, and some ablations are also conducted.", "claims_and_evidence_yn": "No", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "A better experimental validation of the benefits w.r.t. Singh et al. (2018) is necessary. The purported mechanism by which the proposed method improves on existing approaches is by finding smaller enclosures, but this is not sufficiently demonstrated. The other suggestions for additional experiments should be considered optional.\n\nSome more discussion on the relative merits of the proposed loss versus existing losses would be appreciated.", "broader_impact_concerns": "No broader impact concerns.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "ZqodCAR824", "reviewer": "Reviewer_URdj", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "First, at the beginning of this submission, the authors tell us that this work is motivated by the adoption of neural networks in safety-critical environments, citing examples like autonomous vehicle control and airborne collision avoidance. The evaluation and methodology focus primarily on image classification tasks (MNIST, CIFAR-10, SVHN, TinyImageNet), which do not fully represent the complexity of safety-critical applications. Thus, the conducted experiments cannot support the claim in the introduction. \n\nSecond,  the work is driven by the need to ensure neural network robustness against small input perturbations, particularly in safety-critical environments where noisy sensor data or adversarial attacks are concerns. However, the approach addresses robustness against limited perturbations categories, which is a specific and simplified model of adversarial attacks. If I understand it correctly, such a consideration may not adequately satisfy the requirement in the real world. \n\nThen, the proposed training procedure is computationally intensive compared to other robust training methods. Table VII in the paper shows that the proposed method has a training time of 61.2 seconds per epoch on the MNIST dataset with the CNN6 architecture, significantly higher than baselines like IBP (19.9 seconds), TRADES (49.6 seconds), and point-based training (6.1 seconds). The authors need to clarify whether such a higher computational cost undermines or affects the use of such a framework. \n\nIf I understand it correctly, this work relies on dataset-specific hyperparameters for balancing accuracy and robustness. Such reliance on dataset-specific hyperparameters for balancing accuracy and robustness may complicate practical adoption and generalization to new tasks.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "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": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper presents a novel set-based training approach to enhance the robustness of neural networks and facilitate their formal verification, particularly for safety-critical applications. By leveraging zonotopes to represent input and output sets, the authors introduce a gradient set that directly minimizes output enclosures, improving robustness against adversarial perturbations. A set-based loss function balances accuracy and robustness, supported by efficient, differentiable set propagation algorithms. The method is evaluated on datasets such as MNIST, CIFAR-10, SVHN, and TinyImageNet, demonstrating competitive performance and enabling polynomial-time verification.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "Please address my concerns", "broader_impact_concerns": "No need for this paper to add the broader impact statement.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "Wj0bke8vqe", "reviewer": "Reviewer_5Fqf", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n\nThe paper is well-written. Achieving robustness is notoriously hard, specially when one aims to achieve a robust classifier verified formally. I like the set-based approach, however more clarity is needed to showcase the benefit.\n\nWeakness: \n\nPlease see below.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "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": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The central focus of the paper is the robustness of neural networks: a network is robust if small, carefully chosen input perturbations cannot lead to unexpected output. The paper propose a novel set-based training procedure to achieve robustness with formal verification, where they compute the set of possible outputs given the set of possible inputs and consider a novel gradient set for the entire input. The gradient set controls the size of the output enclosure to improve robustness and simplifies formal verification.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "- The work is more related to Mirman et al. 2018 proposing zonotope enclosure, yet the illustrative Figure 1 does not include any comparison with this baseline. \n\n- The key contribution is utilizing set-based computation instead of single instance-based computation, yet the introduction does not go into details on it. How set-based training increases robustness or simplifies formal verification need to be explained intuitively in the introduction.\n\n- Why is different epsilon chosen for different datasets?\n\n- The experimental result shows a trade-off where the presented method is neither highly accurate nor efficient in verification. Is there a fundamental limitation here that no method can be better in both dimensions?\n\n- The paper mentions polynomial verification of the set-based approach, but I do not find any formal proof in the main paper.", "broader_impact_concerns": "NA", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Decision: Accept (poster)