Support is All You Need for Certified VAE Training
Authors: Changming Xu
Debangshu Banerjee
Deepak Vasisht
Gagandeep Singh
Venue: ICLR 2025 Poster (2025)
Keywords: Certified Training
Trustworthy Machine Learning
Variational Autoencoder
Wireless
Primary area: alignment, fairness, safety, privacy, and societal considerations
TL;DR: Certified Training of VAEs by support set bounding of the latent layer.

Abstract: Variational Autoencoders (VAEs) have become increasingly popular and deployed in safety-critical applications. In such applications, we want to give certified probabilistic guarantees on performance under adversarial attacks. We propose a novel method, CIVET, for certified training of VAEs. CIVET depends on the key insight that we can bound worst-case VAE error by bounding the error on carefully chosen support sets at the latent layer. We show this point mathematically and present a novel training algorithm utilizing this insight. We show in an extensive evaluation across different datasets (in both the wireless and vision application areas), architectures, and perturbation magnitudes that our method outperforms SOTA methods achieving good standard performance with strong robustness guarantees.

Published as a conference paper at ICLR 2025
SUPPORT IS ALL YOU NEED FOR CERTIFIED VAE TRAINING
Changming Xu, Debangshu Banerjee, Deepak Vasisht & Gagandeep Singh Department of Computer Science University of Illinois Krbana-Champall
Champaign, IL 61820, USA {cx23, db21, deepakv, sgndsj@illinois..em
ABSTRACT
Variational Autoencoders (VABs) have become increasingly popular and deployed in safety-criticat applications. In such applications, we want to give certified prob- abilistic guarantees on performance under adversarial attacks. We propose novel method, CIVET, for certified training of VAEs. CIVET depends on the key insight that we can bound worst-case VAE error by bounding the error on carefully cho- sen support sets at the latent layer. We show this point mathematically and present a novel training algorithm utilizing this insight. We show in an extensive evalu- ation across different datasets (in both the wireless and vision application areas), architectures, and perturbation magnitudes that our method outperforms SOTA methods achieving good standard performance with strong robustness guarantees.
INTRODUCTION
Deep neural networks (DNNs) achieve state-of-the-art performance in a wide range of fields, includ- ing wireless communications Cho al. (2023); Yang al. (2018), autonomous driving [Bojarski] et al. (2016); Shafaei et al.) (2018), and medical diagnosis Amato et al. (2013); Kononenko (2001). Despite their success, DNNs are vulnerable adversarial perturbations added the input, mak- ing their use in safety-critical systems, such as autonomous driving and wireless communication, risky and potentially tife-thheeaening. To address this issue, numerous robust learning Mirman al. (2018); Mao et al. (2023); Wong & Kolter (2018) and verification approaches [Singh et al. (2019); Xu et al. (2021): ; Wang et al. (2018); Ehlers (211)) have been developed for deterministic DNNs. However, robust learning approaches for stochastic DNNs, including popular generative deep neu- ral networks, are scarce. With the recent surge in the use of stochastic networks like variational autoencoders (VAEs) in security-critee
systems, such wireless networks Liu et al. (202I), it is increasingly vital to develop training methods for stochastic DNNs which are accurate and have provable guarantees of robustness.
VAE is a generative deep neural network architecture. VAEs are used in various domains such computer vision Duan al. (2023). language processing Qian Cheung (2019), wireless Liu et al. (202T). and representation learning van den Oord et al. 2017). However, as with other neural network architectures, existing research has shown that VAE's performance can be unreliable when exposed to adversarial attacks Kos et al.] (2018); Mhondim-Ribente works on training VAEs with formal guarantees impose strict architectural constraints like fixed latent layer variance Barrett et (2022). We lift these restrictions and propose a general framework for training VAFS with certified robustness.
et al. (2018). The few existing
Key Challenges. Unlike deterministic DNN classifiers commonly used in certifiably robust training methods Gowal et al.) (2018); Yang et al. (2023); Mueller et al. (2022), VAE's outputs are stochastic. This requires training methods that can compute the worst-case loss over potentially infinite set of output distributions. Even for a single output distribution, calculating the worst-case error is challenging, its probability density function may not have tractable closed form. Additionally, to apply these methods to practical networks, the worst-case error computation must be both fast and compatible with gradient descent based optimization methods, which are typically used in DNN

---

Published as a conference paper at ICLR 2025
training. Therefore, the worst-case must be expressed as differentiable program involving network parameters to enable efficient parameter refinement.
This work. We propose Certified Interval Variational Autoencoder Training (CIVET), which ef- ficiently bounds the worst-case performance VAEs over an input region while ensuring that the error bound remains differentiable and useful for optimizing network parameters. To the best of our knowledge, CIVET is the first certified training algorithm for VAEs that imposes no Lipschitz or fixed variance constraints on the architecture. Our method is based on key insight: by carefully selecting a subset (support set) of the latent space and bounding the worst-case error of the deter- ministic decoder within this set, we can effectively bound the worst-case enror across all reachable output distributions. Here, the support set selection is driven by the distributions computed at the latent layer by the encoder.
Main Contributions. We list our main contributions below:
We mathematically show that for VAEs, the worst-case error over all reachable output distributions from an input region can be bounded in two steps: (a) identifying an appropriate subset S of the latent space (the support set), and (b) bounding the worst-case error of the decoder over S. This reduction simplifies the problem of bounding the worst-case error for stochastic VAFs to more tractable problem of bounding the error for deterministic decoder networks. However, both steps- support set selection and decoder error bounding must be differentiable to enable efficient learning. By restricting the support sets to specific geometric shapes, such as multidimensional boxes, we ensure that both the support selection and bounding steps differentiable. Here, the support selection step relies on the encoder parameters, while the error bounding step involves the decoder parameters. CIVET efficiently combines these two steps, enabling the simultaneous optimization of the encoder and decoder parameters to minimize the worst-case error w.r.t. the input region.
We perform extensive experiments across the wireless and vision domains on popular datasets with different DNN architectures, showing that our method significantly improves robust worst- case errors while causing only a small degradation in standard -on-adversarial setting:"
BACKGROUND
This section provides the necessary notations, definitions, and background on deterministic and stochastic DNN certification, and certified robust training methods for deterministic DNNs.
Throughout the rest of the paper, use small case letters (x, y) for constants, bold small case letters (x, y) for vectors, capital letters X, Y for functions and random variables, and calligraphed capital letters X, y for sets including sets of probability distributions.
Notation.
2.1 VARIATIONAL AUTOENCODERS
Given a set of inputs, X C dR, generated via an unknown process with latent variables, Z C R4 we want learn latent variable model with joint density po z) - pe px (x|z)p(z) which describes this process. Learning the parameterization, 8, is often intractable via maximum likelihood; instead, we can use variational inference to address this intractability by learning a conditional likelihood model po., po, (x:[z) and an approximated posterior distribution po, (=|z:) Kingma et al. 2019).. A Varia- tional Autoencoder (VAE) is a combination of these two models where 0g represents the parameters of an encoder network, No dd + P(R4), and 0₂ represents the parameters of a decoder network, Nd; : )( + P( (l)dd Here P(R")) denotes the set of probability distributions defined over IR". Generally, for VAEs, given single input z E Rd, the decoder's 's output (d is deterministic.
VAEs Wireless. The effectiveness of VAEs has resulted in their use in several security-critice systems, including wireless applications Liu al. (2021) ) Cho et al. (2023): Yang et al. (0088) 8). Liu ct al. (202T) present FIRE, an end-to-end machine learning approach that utilizes VAES for precise channel estimation, critical operation for wireless communications such cellular and Wi-Fi networks. In a real-world testhed environment, FIRE achieves an SNR (Signal to Noise Ratio) improvement of over 10 dB in Multiple Input Multiple Output (MIMO) transmissions compared to SOTA non-machine learning methods. However, despite their strong performance in wireless systems, Liu al. (203) exposes the vulnerabilities of VAEs to practical adversarial attacks.
"Code provided http://gghhh..ommmiiiffccaaalll
2

---

Published as a conference paper at ICLR 2025
2.2 NEURAL NETWORK CERTIFICATION
Given a deterministic DNN N: I - Rd.,, DNN certification Singh et al. (019 proves that the network outputs y = (a) corresponding to all possible inputs x specified by imput specification & : R - {True, False), satisfy output specification & Rd + { rue, False]. Formally, we show that v' E R .(lloo(()) x)) + <x(())) holds. Safety properties like local DNN robustness linear inequality (or conjunction of linear inequalities) over DNN output y E RR e.g. (y) = (c" y 2 0) where e E IR However, this formulation assumes N is deterministic and does not work when the network's output is stochastic like VAEs.
encode the output specification (1/)
Certification for Stochastic Networks. (Berrada et al. 2021) generalizes DNN certification for stochastic networks including VAEs w.r.t. the input region Φ Rd At a high level, in this case, we want to prove that the worst-case eπrог is bounded over all possible output distributions with high probability say (1 (1-88 8) E (0.5. 1]. For a set of inputs (possibly infinite) oe S R let y denote the set of distributions computed by a stochastic DNN N Ih + P(Rd on Φt. Then y {YIY= = =Nx)), x E TR/4) where Y a random variable representing the output distribution ((x) at single input æ. Given an error threshold 60 E IR, target probability threshold (1 5) E (0.5. 1], and a error function M de + [0, oc) the output specification v : P(RRd + (True, False] is
defined as Pmin ()', ca) (1 5) with Pmin Eo) miny Ey PYM S Eg).
2.3 CERTIFIED TRAINING FOR DETERMINISTIC DNNS
Certified training allows to learn network parameters that make the DNN provably robust against adversarial perturbations. During training for any input Do Th from the training set, certified training methods first bound the worst-case loss Lw (Ne((N))) = ma ((N)(z)) w.r.t. a
local input region de (zx) around Zo. The method then refines the network parameters 9 based on the worst-case loss (NN instead of the point-wise loss ((N)(zo)) used in standard training. The local input region (2ra) typically contains all possible inputs 2 satisfying || Follox S 6 for some perturbation budget Rt. However, even for ReLU networks and Lxp norm bounded local input regions, exactly computing L.. (Ng is NP-Hard Katz et al. (2017b). Hence, SOTA certified training methods for scalability replace the worst-case loss [No (xo)) with an efficiently computable upper bound (No
- Lus (No (No (2o)) provably reduces the worst-case loss during optimization. Moreover, training meth- ods ensure that Lub (No()))) computation can be expressed as a differentiable program allowing refine network parameters 0 with gradient descent based algorithms. For example, one popu- lar certified training method Mirman et al. 2018) uses interval bound propagation (IBP) or Box propagation to compute (Ne(o))) IBP first over-approximmtes the input region, di (xo), with multidimensional box where each dimension E [dm]] is an interval with bounds [4, u.j. Then IBP training propagates the input box through each layer of the network using interval arithmetic Mirman et al. (2018) to find the bounding interval [Cno(N (No()))) L.s (N)()))) of the worst-case error En (2o))
Note that minimizing the upper bound
Although significant progress has been made in certifiable robust training for deterministic networks, to the best of our knowledge, there is currently no general framework for certifiably robust training of VAEs that does not impose architectural constraints. The key challenge is to bound the worst- case training loss over a potentially infinite set of output probability distributions while ensuring that the bounding method is both scalable and differentiable (suitable for gradient-based parameter learning). Next, we discuss our approach for training certifiably robust VAEs.
3 CERTIFIABLY ROBUST TRAINING FOR VAES
In this section, we describe the key steps of CIVET with the formal problem formulation in Sec. 3.1 the reduction of worst-case error computation for stochastic VAES to worst-case error bounding for deterministic decoders in Sec. 3.2 and efficient support selection and bounding algorithm in Sec. 3.3 Fig | illustrates the workings of CIVET highlighting its key steps. In Appendix C we provide concrete example of the steps outlined in this section.
3

---

Published as a conference paper at ICLR 2025
N(a,
VAE Staudard Pass
X
CTVE Training
H4, a
Hib
Bub
o(x)
No
LLub Mubl
N( 9b)
Muu Cub
Z5
Ohbs Jub)
Nd
S
C(Ss)
8
SELECTSUPP(HID) Mubi Oub.
Figure 1: (CIVET Overview) The blue dashed box (i.)) shows a standard pass over a VAE, where the encoder (No) generates parameterization of distribution which is sampled in the latent layer and passed the deterministic decoder (Nd). The green dotted box ( (II shows CIVET training over the same VAE. Here an input region is passed through Ne using deterministic DNN bounding algorithm like IBP which gives range of distribution parameterizations. CIVET then computes support with given probability threshold (1 8) which then be passed through N using deterministic DNN bounding algorithm to obtain an overapproximation of the loss.
3.1 PROBLEM FORMULATION
We define the worst-case loss of a VAE with an encoder network Ne and decoder network Nd w.r.t. input region (x(x)) around training data point æo E gda, Let, Z denote the set of distributions at the latent layer computed by N on (z i.c Z 26 = (x)) (1 ZJ. Note that each Y and are random variables corresponding to a specific probability distribution over R4 and R respectively. Then given target probability threshold (1 5) and error function M, the worst case error L (Ne, Ndd ,0) = maxyey T(Y) where T(Y) defined as follows
and y be the set of output distributions y {Y Y (Z),
T(Y) = min w. P(M(Y) I w) (1 (1-5)
WER
At high level, for any given output distribution Y. T(Y) determines the tightest possible error threshold, ensuring that for any sample T(Y) with a probability of least (1 - 8). (N', .o)) maximizes the error threshold T(Y) over all possible output distributions. Assuming sampled from input distribution X the expected worst case loss is Ex-x (N', .á x). Now, with fixed architectures of No and Ná learning the parameters 8e, Oa corresponding to the smallest expected worst case loss be reduced to the fol- lowing optimization problem: (0", 07) = arg ming, 00, Em-x x. ,Z, (0z, 02 x). While this optimiza- tion problem precisely defines the optimal parameters (6' 07). solving it exactly is computationally prohibitive for networks of practical size. Even determining T(Y) for single continuous random variable Y can be costly, making worst-case loss computation for a single local input region (x(2)) practically intractable. Therefore, similar certifiably robust training methods for deterministic networks, we focus on computing mathematically sound upper bound Lub (0e, 0d, T.)
Y. the corresponding error M is no more than
However, unlike deterministic DNNs that existing works handle, VAEs require bounding methods capable of handling a potentially infinite set of probability distributions. To tackle this, we first show possible compute non-trivial upper bound (us 04, 20) by: a) finding an appropriate subset S S R4 (referred as the support set in the rest of the paper) based on the set of reachable distributions the latent layer, and bounding the worst case error of the decoder N'd over i.e. bounding maxzes M (2) (Section 3.2) Additionally, in Section 3.3 we show that both finding and bounding S can be efficiently expressed as a differentiable program involving the encoder and decoder parameters 0g. 0g. This enables learning the parameters with gradient descent.
3.2 BOUNDING WORST-CASE LOSS
First, we formally define support sets for the set of distributions at the latent layer. Definition (Support Sets), For set of distributions over Rd and a probability threshold (1-5), subxet S C RRd: is a support for Z provided (minzez P(Z 8)) > (1 5).
4

---

Published as a conference paper at ICLR 2025
For fixed (1 8), we show that for any support set S the error upper bound Tuc(S) max+es M (N serves as valid upper bound of the worst-case error Lw (fe, 8g. 2o) I (S) S, computing Tub (S)(S) is same as bounding the error of a deterministic (N4) network on input region (S). This shows that with ap- propriate & we reduce the worst-case error bounding for VAEs to the worst-case error bounding of deterministic networks as handled in existing works Katz et al. (017b).
(Thm I. Since decoder's output (²) is deterministic for all
Theorem 1. For VAF with encoder N decoder No, local inpul region 6i (3r),, error error function M and probability threshold (1 - 5). if z = {Z| Z = (²(x), x E or(20)} then for any support set S ffor Z the worst case error Lw (N Ná, 20) S (S) where Tub max M (N))
Proof Sketch. Let, te (v) = -M(y) < ()) be an indicator where lo = (S) The key observa- tions are that a) the indicator 4,, (Nd(z)) (z))
for all = E S and b) given S S R4 is a support hence for any Z E 2. .s fz (z)dz 2 (1 - 6) where fz is the probability density function of Z.
Now, with Eq. 1 it is enough show (Y) S to) 2 (1 6) for any Y = (Z) where Z E Z. Since S C TR.. P(M(Y) S 4n) 2 Is Jr. (2) x fz(2
)dz and from observations (a) and (b) we get Js (N) x fz(z)dz 2 (1 5). The detailed proof is in Appendix A
Ideally from the set of all possible supports S. we should pick the support S* that minimizes Tws (S) over all S E S. Although S* provides the tightest upper bound (N',, xo) from S, finding and subsequently bounding the optimal S can be expensive. In contrast, picking an arbitrary sup- port S from S can make the upper bound (N"; N , a0) too loose hurting parameter (0., 0a) refinement. For example, the entire latent space R2 is always a valid support but it fails to provide a non-trivial upper bound C.,, Nod ). To strike balance between computational efficiency and tightness of the computed bounds we first restrict S to a subset of supports S C S where com- puting (S) is cheap and then find the optimal support S* from this restricted set (Section 3.3).
Before moving into the support selection algorithm, we want to emphasize a couple of key points. First, Theorem can be extended to subsets of any hidden decoder layer. This means that supports can be chosen from any hidden decoder layer, not just the latent layer. However, we focus on the latent layer because the distributions Z E 2 typically have well-defined closed forms for their probability density functions, such as Gaussian distributions, which simplifies the support selection process. Second, similar to stochastic DNN verifiers Berrada et al. (202I); Wicker et al. (2020), we assume that for a given (1 8), there exists at least one bounded support S. Without this, T (S) for an arbitrary unbounded S may not be bounded.
3.3 SUPPORT SET COMPUTATION AND BOUNDING
As mentioned above, it is computationally expensive to minimize over all possible supports S. By picking a restricted set of supports S' we balance computational efficiency and tightness. In S', we only consider multi- [di]
Mib
Hub
Nip.o)
dimensional boxes where for any dimension we include all values within the range [4, uz]. Hence, finding a support set from S' only requires computing the bounds 4i, uz for each dimension. Moreover, IBP techniques commonly used in deterministic certified training can bound the worst-case error of the decoder over any support set from S'. So only picking a support set is sufficient to reduce the problem into an instance of deterministic certified training.
[Ma
t E [An, Gab
Alan, ond)
M(Huh, Gub)
A Alpm oub
S₂ [M
C, Mab + Ç)
Given a set of distributions Z Z with probability density functions fz (z) and a fixed (1 - 6). let S = [t, u.). Our bounding problem can now be expressed as finding 1, u s.t. ZZ E Z. Lú fz(2)dz 2 (1 5).
Figure 2: Support Set Visualization. Given a set of distributions (N(,, Hutt), a E [oms mnl) we define sym- metric support set S3 [mm - C, Pub + c)
For the scope of this paper, we assume that Z is derived from the latent layer of a VAE where N is deterministic network that outputs μu, for each latent dimension parameterizing gaussian distribution (the most common setting for VAEs). Thus, given (2)) and N we can use existing deterministic network bounding techniques (i.e. Mirman al. (2088) to overapproximate reachable
5

---

Published as a conference paper at ICLR 2025
intervals [ur. Mubli low. Tubll Let's first consider the 1d case. We now have 2 = (M(u, p Pabb a E [or owol]. Therefore, our bounding problem can be expressed as finding I, s.t.
Vu E [uas, Publ, [orus ousl Pn,a (u) 2n (1) 2 (1-0) o)
(2)
Here, Pu.o is the normal cumulative distribution function (CDF) with mean i and variance o² and for case of notation let & := 1 There are many ways to pick [L, ul satisfying Equation 2 Since this set of normal distributions is symmetric around its midpoint 1/2(/40 + (ubb), we choose symmetric support, i.e. [t, u| Jau - Mub Muu + {] with O. Note that the interval [2. u) always
includes the interval [u4s, Mub] as required by the condition (1 - 6) > 0.5 (see Sec. 2.2). Figure
gives pictorial representation of our support selection. In Theorem given - 6) we give support set satisfying Equation
Lemma 1. Given bounds pib, plud, Olh, Jub E IR probability threshold (1 11-00 8), and ( E Rt. Let C(u,o,u, 1) 4 ( (p) Then Vu [ptb [pib-Publ Publ, E (ow. Tubl.
C(H, + 4. () 2 C(pabr Bubs Pub + C, Pib - ()
Furthermore,
C(uub Jbb. Hub + Mib - 5) = C(pab. Jub. Pub + Mib ()
Proof Sketch. The proof relies on two key facts: a) for a fixed mean E [pAN [ubl and bounds C(u, u, > C(u, Tub. u, b) for any standard deviation
1 S Pib. Hub [otb, aubl C(u, or Huu + M.b C) is maximized at each side as increases (or, decreases). Formal proof is provided in Appendix A
Jub
Bact and is strictly decreasing
Lemma I limplies that when support set is symmetric around [pm Mubl then the distributions the endpoints N M(pw. Jub ), (Hu,, oub) minimize C.
Theorem 2. Given = {N(,, o) μ E [mie: Hasl. E [o,., owll probability threshold (1 - 5), then 1. u] [m aws Φb (Po), Hub + T (po)] satisfies Equation 2 Where
Po
min pE((1-8)1]
Φ (p)(p) x- x- (1 8))
Pub
Ouh
Proof Sketch. Using Lemma [ we can prove that this formulation satisfies Equation 2 N (Huut Jub) does. We can then plug this distribution into C to show that & Puss (u) T ppus.o.s (1) 2 (1 5). Formal proof can be found Appendix A
Although --1 has closed form solution Vedder 1993) given 1466 Mla. Uub can compute Po using binary search since t is strictly monotonic. For higher dimensional latent spaces, the distribution for each dimension in the latent layer is independent for individual inputs. Based this, given a probability threshold (1 8) over di dimensions, we can compute the probability threshold
for each dimension as (1 1/14 Therefore, given (1 8). each dimension E [d] of the selected
support S is interval S j44 o - (p6), pu one (r-((6)) where ph is independently
computed in each dimension as defined in Theorem 2 This shows the S3 is function of the
encoder's output (1ib, Hub, oub) and subsequently depends the encoder parameters O..
3.4 CIVET LOSS
Theorem 2 gives us a way to find a support set, Ss given Pib: Hub: Tub for specific (1 8). However, we may not know the target probability training time. We would like to cover the target probability without selecting an overly large (1 - ò) which may result in loose bound. Inspired by numerical integration Gibb (1915). CIVET computes the loss over multiple support sets weighting them based on their covered probability. We provide additional analysis on this selection in Appendix|] D

---

Published as a conference paper at ICLR 2025
Given single 6, we can obtain overapproximation of (S)) by passing Sx through the deter- ministic (N network using existing worst-case network bounding techniques Mirman et al. (0018) We call this loss (d x, Sq). For CIVET we combine multiple support sets to compute our loss so we let Ss, be the support for 2 with probability threshold (1 6:) for each i. For the remainder of the paper, assume that lists of 5 are sorted in reverse order, formally, 6g < 53 if i j. For the largest 6, 5j, corresponding to the smallest So we assign weight (1 - 61). For the remainder of the 8,'s s, we weigh them based on the additional probability they cover compared the previous 6, in other words, Vi E .2.....n...s
gets weight 6;-1 - 8g. This leads to CIVET loss.
Definition 2. (CIVET Loss) Given deterministic decoder network Nd, input Pib Pub. uub E and a set of ós (ō,....,ān) We define,
R&,
LCIVET = =(1 Looc ar ) +
Σ (0 - 6,) 6,)n Ss:)
3.5 CIVET ALGORITHM
Algorithm shows CIVET's training algorithm based on the LCIVET from the Section 3.4 We specify IBP as the deterministic bounding method; however, CIVET is general for any differentiable deterministic bounding method. For each Epoch, we iterate over inputs æ in dataset X. We first compute the upper and lower bounds on the latent space distribution parameters (line 3). We then compute the weighted loss LCIVET FT by first computing a support set Ss, for each delta, 6, with the FINDSUPPORT (FS) algorithm (line 4, 7). We can now use an existing deterministic bounding algorithm to compute the worst-case loss over 0a on each Ss, (line 5,8). Algorithm ( shows a binary search algorithm for finding support sets. Note that if we reach the maximum depth we return the upper bound as it is sound overapproximation. CIVET is the first algorithm specialized for certified training of VAEs which does not impose lipschitz restrictions the encoder and decoder networks.
Algorithm CIVET Algorithm
Algorithm 2 FS (ubb. Pab, Tub: 6, l, J)
1: for x C X do
I: m = (1+u)) u)
2:
pib, Mub, Tlb. uub IBP(O,. (z))
2: s = 4 (m) 4b (m - (1 6) 1)1/d1)
3:
Ss, + FS (H Huh, unb. 8,, 51, 1,0)
3: if Imax
(wu (0ub-Hub//1 /Hub)/ow ous then
4:
LOIVET
(1 81 Looe (0d, x, Ss.)
4: return (146 - Jub (u),
5:
for E [n. do
5:
Hlub + Tu (n))
6:
Ss. + FS Mub, uub, 81, 6 1.0)
6: if s < (14bb //ab)/ oub then
7:
LOIVET + LCIVET
7: return FS Pub, anb. 6, m, ú, + 1)
8:
+ 8,) Ldec x, S6,)
8: else
9:
Update 0z, Od using LCIVET
9: return FS Mub, Ju. 8,4, m. + 1)
4 EVALUATION
We compare CIVET to adversarial training and existing certifiably robust VAE training methods.
Experimental Setup. All experiments were performed on a Nvidia A100, We use the functional Lagrangian inspired probabilistic verifier proposed in [errada al. (202T) to perform certification. We additionally compare CIVET to baselines on empirical robustness obtained with adversarial attack methods: RAFA Liu et al. (2023) for wireless and Latent Space Attack (LSA) Kos et al. 2ax8/M Damage Attack (MDA) Camuto et al. (202T) for vision (see Section 4.4). We use Mirman et al. (2018) for our deterministic bounding algorithm for both verification and training- We perform our experiments in two target application areas: vision and wireless. Unless otherwise specified we train CIVET with D = [0.35, 0.2, 0.05] as our set of ōs. In (oction|4.3 we experiment with different sets of ōs. Results are averaged over the entire test set for each dataset and computed with 5 = 0.05. Certification/Atten radius is set to training c. Additional training parameters can be found in Appendix B
Wireless. In order to achieve MIMO capabilities in 5G, base stations need to know the downlink wireless channel from their antennas every client device. In FDD (Frequency Domain Duplex-
7

---

Published as a conference paper at ICLR 2025
Table 1:
Comparison of different training methods: standard training, adversarial training (PGD)
and CIVET on FIRE, results reported in SNR.
Dataset
Training Method
Baseline
Certified
RAFA
Standard
17.79 dB
4.12 dB
5.35 dB
15%
PGD
17.81 dB
6.89 dB
7.18 dB
CIVET
16.58 dB
15.02 dB
16.27 dB
Standard
17.79 dB
1.28 cB
4.32 dB
FIRE
20%
PGD
17.40 dB
4.69 dB
5.24 dB
CIVET
16.34 dB
14.61 dB
15.98 dB
Standard
17.79 dB
-2.35 dB
0.16 dB
25%
PGD
17.40 dB
3.17 dB
4.09 dB
CIVET
15.82 dB
12.88 dB
13.43 dB
Table 2: Comparison of different training methods: standard training, adversarial training (PGD) and CIVET on MNIST and CIFAR-10, 10, results reported as MSE.
Dataset
Training Method
Baseline
Certified
LSA
MDA
Standard
0.0023
0.1426
0.0652
0.0873
0.1
PGD
0.0025
0.0648
0.0093
0.0102
CIVET
0.0027
0.0089
0.0065
0.0078
MNIST
Standard
0.0023
0.1884
0.0764
0.0922
0.3
PGD
0.0027
0.0972
0.0154
0.0386
CIVET
0.0031
0.0274
0.0163
0.0261
Standard
0.0041
0.0340
0,0216
0.0188
PGD
0.0041
0.0167
0,0068
0.0049
CIVET
0.0049
0.0055
0.0053
0.0054
CIFAR-
Standard
0.0041
0,2098
0.0562
0.0801
PGD
0.0043
0.0760
0.0173
0.0093
255
CIVET
0.0062
0.0153
0.0087
0.0124
ing) systems, dominant in the United States, the client devices measure the wireless channel using extra preamble symbols transmitted by the base station and send it as feedback to the base station. However, this feedback is unsustainable and causes huge spectrum waste. Recent work [iu et al.) (222I) proposed FIRE which uses an end-to-end ML based approach to predict the downlink chan- nels. For this paper, we choose to evaluate against FIRE because it shows SOTA performance, uses a VAE architecture, and Liu et al. (2023) shows that FIRE vulnerable to real-world adversarial at- tacks. Errors in downlink channel estimates reduce the communication efficiency of multi-antenna systems (e.g.. MIMO). Robustly training FIRE will allow it to be safely deployed in real-world systems. Additional details FIRE and the choice of VAEs can be found in Appendix
For our wireless experiments, we do a best-effort re-implementation of FIRE Liu et al. (2021). We borrow the data and neural networks used by Liu al. (2023). The VAE has 7 linear layers both the encoder and decoder networks with a 50 dimensional latent space. Liu et al. (2023) collected 10,000 data points by moving the antenna randomly in a 10m by 7m space, and composed of many reflectors (like metal cupboards, split. We also adopt the same adversarial budget used by percentage of the average amplitude of the benign channel estimates. We use Signal-Noise Ratio (SNR) to report performance for wireless, similar to (Liu et al. [2021] 2023)).
bbared- etc.) and obstacles. We use the same 8:2 train/test
al, (003)): the perturbation allowed
Vision. We consider two popular image recognition datasets: MNIST Deng (2012) and CIFARI0
Krizhevsky et al. (2009). We use a variety of challenging 4.c. perturbation bounds common in ver- ification/robust training literature Xu al. (2021); Wang et al. 1) (Singh et al. (019 201 Sa); Shi et al. (20TT); Mueller et al. (202 y; Mao et al. (2023). We use a VAE with convolutional and linear layer for both the encoder and decoder. For MNIST
32 dimensional latent space and for CIFAR-10 10 we use a 64 dimensional latent space. Both MNIST and CIFARIO have a test set of 10,000 images. We compare the performance for both datasets using Mean Squared Error (MSE).
8

---

Published as a conference paper at ICLR 2025
Table 3: Comparison of CIVET and Lipschitz VAEs Barrett et al. 2022
MNIST and CIFAR-IO,
MSE is reported.
Dataset
Architecture
Training Method
Baseline
Certified
LSA
MDA
Lipschitz CIVET
0.0049
0.0253
0.0168
0,0211
0.1
0.0038
0.0230
0.0114
0.0197
MNIST
FC
Lipschitz CIVET
0.0064
0.0486
0.0366
0.0409
0.3
0.0043
0.0507
0.0412
0.0359
Lipschitz CIVET
0.0083
0.0105
0.0089
0.0096
255
0.0049
0.0055
0.0053
0.0054
CIFAR-10
Conv
Lipschitz CIVET
0.0112
0.0267
0.0178
0.0252
255
0.0062
0.0153
0.0087
0.0124
4.1
MAIN RESULTS
We compare CIVET to standard training and adversarial training on FIRE in Table [ and vision in Table Across all datasets and es we observe that CIVET obtains significantly better certified performance (e.g. 13.88 dB vs -2.35 dB for FIRE with e 25% and 0.0089 vs 0.01426 for MNIST with 0.1). CIVET obtains comparable performance on baseline metrics. Notably. CIVET still outperforms traditional non-ML baselines Liu al. (202T). Our results indicate that CIVET obtains significantly better certified performance while losing some baseline performance, inline with certified training approaches for other NN architectures (Shi et al. (202T): Gowal et al. (2018).
4.2 COMPARISON TO LIPSCHITZ VAES
In this section, we compare CIVET to Lipschitz VAEs proposed by Barrett al. (2022). A network f: 14 + Rdo is Lipschitz continuous for all X1 X2 E Rd.., fx (x2)]
<
M ||xx - X
for constant M E R+ The least M for which this holds is the Lipschitz constant of f. Barrett et al. (002) trains Lipschitz-constrainee
VAFS with fixed variances
the latent space. [Barrett et al.
2022 only reports results for fully connected MNIST VAEs. For MNIST, we follow their network architecture with a latent space of 10 and 3 fully connected layers. For CIFAR-10 10, we use our con- volutional network architecture with a latent space of 64, Barrett al. (022) only trains networks with GroupSort activation. Anil et al. (2019) shows that Lipschitz constrained networks are lim- ited in expressivity when using non- gradient norm preserving activations such sigmoid or ReLU introducing GroupSort an alternative (it can be shown that GroupSort is equivalent to ReLU when the group has size Anil et al. (2019)) Following Barrett et al. (022) we compare their networks with GroupSort to our networks with ReLU. Table 3 provides detailed results on the comparison of Lipschitz VAEs and CIVET. In some cases (CIFAR-10) CIVET almost doubles the performance of Lipschitz VAEs (0.0062 vs 0.0112 8/255 baseline, 0.0055 0.0105 2/255 certified). For MNIST with c 0.3 Lipschitz VAE outperforms CIVET for certified performance and LSA performance; however, CIVET still greatly outperforms in baseline performance (0.0043 0.0064). Therefore, CIVET is better on almost all benchmarks while generalizing to more network architectures.
4.3 ABLATION STUDIES
For our experiments we choose D [0.35, 0.2, 0.05) or [D] 3 and 17 0.15. In this ablation study, we compare results on FIRE at 25% perturbation budget while varying D. In Appendix H Figure 3 shows the average standard and certified SNR for networks trained using CIVET with varying Ds. In both graphs we see increasing standard SNR as either the size of D increases or the difference between each of the ås increases, but observe that certified SNR decreases past a certain point. Note that on the left side when (D) = 5 the largest 8 0.65 and on the right side when 7 = 0.25 the largest = 0.55. We hypothesize that adding such a large decreases regularization leading to improved accuracy, but no longer captures significant portion of the distribution leading to decreased certified SNR. We leave further study of D selection to future work. We also test the affect of combining CIVET with SABR Mueller et al. (022) in Appendix G

---

Published as a conference paper at ICLR 2025
4.4 PERFORMANCE AGAINST ATTACKS
Liu et al. (2023) proposes RAFA (RAdio Frequency Attack), the first hardware-implemenned adver- sarial attack against ML-based wireless systems. Specifically, Liu et al. (2023) shows that RAFA can severely degrade the performance of FIRE in the real-world. For our vision datasets we compare our results against SOTA VAE attacks. LSA Kos al. (2018) tries maximize the KL divergence in the latent space, while MDA Camuto et al. 2021) maximizes the reconstruction distance. We compare CIVET against the baselines on these attack methods Tables [ CIVET outperforms baselines on most benchmarks, when CIVET underperforms it is tied to its decrease in baseline accuracy.
4.5 RUNTIME ANALYSIS
For CIFARIO and = 8/255, standard training took 45 minutes, adversarial training took 68 min- utes, Lipschitz VAE took 73 minutes, and CIVET training took 296 minutes (runtimes for FIRE and MNIST can be found in Appendix [.. The main difference comes from taking 3 passes of the decoder network. CIVET using D 0.05] on CIFAR-I0 takes 86 minutes significantly closer to baseline timings while obtaining a baseline performance of 0.0075 and certified performance of 0.0219 still outperforming Lipschitz VAE on both metrics and all baselines in certified performance.
RELATED WORK
Deterministic DNN Verification. Neural network verification is generally NP-complete Katz al. (2017a) so most existing methods trade precision for scalability. Single-input robustness can be deterministically analyzed via abstract interpretation /Singh et al. (2019): Banerjee et al. (2024c) or via optimization using linear programming (LP) De Palma et al. (2021): Müller et al. a (2022), mixed
integer linear programming (MILP) [Singh al. (201 Tjeng al. (2018). Recent studies have
extended verification to incremental settings Ugare et al. (223 2024). hyperproperties Banerjee &
Singh (2024); Suresh et al. (2024): Banerjee et al. (2024b). and DNN interpretation Banerjee et al. (202aa).
Probablistic DNN Verification. Cardelli et al. (2019); Michelmore et al.
(2019) give statistical
confidence bounds the robustness of Bayesian Neural Networks (BNNs). Wicker al. (2020)
gives certified guarantees on the probabilistic safety of BNNs. Berrada et al. (202)) introduces the functional Lagrangian give general framework for giving certified guarantees probabilistic specifications, their formulation is general and can handle stochastic inputs, BNNs, and VAEs.
Certified Training of Deterministic DNNs. Shi et al. 2201); Mirman et al. (2018); Balunovid
& Vechev 22000); Zhang et al. (2019) are well-known approaches for certified training of standard DNNs. More recent works Mueller al. (2022); Xiao al. (2019); Fan & Li] (2021) Palma et al.)
(0044) integrate adversarial and certified training techniques to achieve state-of-the--e performance
in both robustness and clean accuracy.
Certified Training for Stochastic DNNs. Wicker et al. (2021) proposes an IBP-based certified training method for BNNs. |Wikker al. (202T) samples the parameters (weights and biases) of BNNs to generate set of deterministic networks. They then apply IBP to each of these determin- istic networks during training. While CIVET utilizes the same high-level idea of reducing certified training for stochastic networks to that of deterministic networks, it exploits the unique structure of VAFs. CIVET is also general for arbitrary differentiable deterministic bounding methods. |Barrett et al. (2022) trains certifiably robust VAEs by imposing lipschitz conditions and fixed variance. CIVET removes these restrictions handling a more general class of VAEs.
LIMITATIONS/CONCCUUSSO
We discuss the limitations of CIVET in Appendix F In this paper, we introduce a novel certified training method for VAEs called CIVET. CIVET is based our theoretical analysis of the VAE robustness problem and based on the key insight that it is possible to find support sets which over- approximate this loss, and that these support sets can then be analyzed using existing deterministic neural network bounding algorithms. CIVET lays the groundwork for a new set of certified training methods for VAFs and other stochastic neural network architectures.
10

---

Published as a conference paper at ICLR 2025
REPRODUCIBILITY STATEMENT
To assist with reproducibility and further research we have released the code used for our results publicly. Section gives details on our evaluation which is supplemented by Appendix Appendix contains full proofs of all Theorems and Lemmas stated in the paper, and all assumptions made have been stated the main body of the paper. Section Flass gives an overview of some additional assumptions made.
ACKNOWLEDGMENT
We thank the anonymous reviewers for their insightful comments. This work was supported in part by NSF Grants No. CCF-2238079, CCF-2316233, CNS-2148583.
REFERENCES
Filippo Amato, Alberto López, Eladia María Peña-Méndez, Petr Vañhara, Aleš Hampl, and Josef Havel. Artificial neural networks in medical diagnosis. Jourmal of Applied Biomedicine, 11(2), 2013.
Cem Anil, James Lucas, and Roger Grosse. Sorting out lipschitz function approximation. In Inter- national Conference Machine Learning, pp. 291-301. PMLR, 2019.
Mislav Balunović and Martin Vechev. Adversarial training and provable defenses: Bridging the gap. In 8th International Conference on Learning Representations (ICLR 2020)(virtual), International Conference on Learning Representations, 2020.
Debangshu Banerjee and Gagandeep Singh. Relational dnn verification with cross executional bound refinement. In ICML, 2024. URL https:: pttts:://openreveew wwtpeeiwwwwwwweeeeeeeeeeeeeeeeee met/fof hfr.uoorrm?dd
HCG80Yk4Gw
Debangshu Banerjee, Avaljot Singh, and Gagandeep Singh. Interpreting robustness proofs of deep neural networks. In The Twelfth International Conference on Learning Representations, 2024a.
URL httphttss///ppneeeeeeee net wtr.:oorrrmuirre/ wtt//orumm/ddd//// 1FF 9TWML
Debangshu Banerjee, Changming Xu, and Gagandeep Singh. Scalable relational verification and training for deep neural networks. International Conference on Computer Aided Verification, 2024b.
Debangshu Banerjee, Changming Xu, and Gagandeep Singh. Input-relational verification of deep neural networks. Proc. ACM Program. Lang., 8PLDDI, June 2024c. doi: 10. 10.1145/3656377. URL
1145/36561777
Ben Barrett, Alexander Camuto, Matthew Willetts, and Tom Rainforth. Certifiably robust variational autoencoders. In International Conference on Artificial Intelligence and Statistics, pp. 3663- 3683. PMLR, 2022.
Leonard Berrada, Sumanth Dathathri, Krishnamurthy Dvijotham, Robert Stanforth, Rudy R Bunel, Jonathan Uesato, Sven Gowal, and M Pawan Kumar. Make sure you're unsure: A framework for verifying probabilistic specifications. Advances in Neural Information Processing Systems, 34: 11136 11147, 2021.
Mariusz. Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, et al. End to end learning for self-driving cars. arXiv preprint arXiv: 16Xv::660.073316 2016.
Alexander Camuto, Matthew Willetts, Stephen Roberts, Chris Holmes, and Tom Rainforth. To- wards a theoretical understanding of the robustness of variational autoencoders. In International Conference on Artificial Intelligence and Statistics, pp. 3565-3573. PMLR, 2021.
Cardelli, Kwiatkowska, L Laurenti, Paoletti, A Patane, and M Wicker. Statistical guarantees for the robustness of bayesian neural networks. IJCAI-19, 2019.

---

Published as a conference paper at ICLR 2025
Kun Woo Cho, Marco Cominelli, Francesco Gringoli, Joerg Widmer, and Kyle Jamieson. Scalable multi-modal learning for cross-link channel prediction in massive iot networks. In Proceedings of the Twenty-Fourd International Symposium Theory. Algorithmic Foundations, and Protocol Design for Mobile Networks and Mobile Computing, MobiHoc '23, pp. 221-229, New York, NY, USA, 2023. Association for Computing Machinery. ISBN 9781450399265. doi: 10.1145/ 3565287 01128883660200
httt:p/s./oii..oor//...11//////3 361228
Alessandro De Palma, Harkirat Singh Behl, Rudy Bunel, Philip H. S. Torr, and M. Pawan Kumar. Scaling the convex barrier with active sets. International Conference on Learning Representa- tions, 2021.
Li Deng. The mnist database of handwritten digit images for machine learning research. IEEE Signal Processing Magazine, (41)):141-12,, 2012.
Zhihao Duan, Ming Lu, Zhan Ma, and Fengqing Zhu. Lossy image compression with quantized hi- erarchical vaes. In Proceedings of the IEEE/CVF Winter Conference on Applications of Computer Vision, pp. 198-207, 2023.
Ruediger Ehlers. Formal verification of piece-wise wise linear feed- forward neural networks. In Interna- fional Symposium on Automated Technology for Verification and Analysis, pp. 269-286. Springer, 2017.
Jiameng Fan and Wenchao Li. Adversarial training and provable robustness: A tale of two objec- tives. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pp. 7367- 7376, 2021.
David Gibb. A course in interpolation and numerical integration for the mathematical laboratory. G. Bell & Sons, Limited, 1915.
George Gondim-Ribeiro, Pedro Tabacof, and Eduardo Valle. Adversarial attacks on variational autoencoders. arXiv preprint arXiv: 006604446, 2018
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Ue- sato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv e-prints, pp. arXiv-1810, 2018.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Computer Aided Verification: 29th International Conference. CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30. pp. 97-117. Springer, 2017a.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 130. pp. 97-117. Springer, 2017b.
Diederik Kingma, Max Welling, et al. An introduction variational autoeneoders. Foundations and Trends@ in Machine Learning, 12(4):307-39) 2019.
Igor Kononenko. Machine learning for medical diagnosis: history, state of the art and perspective. Artificial Intelligence in medicine, 23(1):89-109, 2001.
Jernej Kos, Ian Fischer, and Dawn Song. Adversarial examples for generative models. In 2018 ieee security and privacy workshops (spw), pp. 36-42. IEBE, 2018.
Alex Krizhevsky, Geoffrey Hinton, et al. Learning multiple layers of features from tiny images, 2009.
Zikun Liu, Gagandeep Singh, Chenren Xu, and Deepak Vasisht. Fire: mimo systems. In Proceedings of the 27th Annual International Conference on Mobile Computing and Networking, pp. 628 641, 2021.
enabling reciprocity for fdd
12

---

Published as a conference paper at ICLR 2025
Zikun Liu, Changming Xu, Yuging Xie, Emerson Sie, Fan Yang, Kevin Karwaski, Gagandeep Singh, Zhao Lucis Li, Yu Zhou, Deepak Vasisht, et al. Exploring practical vulnerabilities of machine learning-bast -base wireless systems. In 20th USENIX Symposium Networked Systems Design and Implementation (NSDI 23), pp- 1801-1817, 2023.
Yuhao Mao, Mark Niklas Müller, Mare Fischer, and Martin Vechev. Taps: Connecting certified and adversarial training. arXiv e-prints, pp. arXiv-2305, 2023.
R Michelmore, M Wicker, L. Laurenti, L Cardelli, Y Gal, and M Kwiatkowska. Uncertainty quan- tification with statistical guarantees in end-to-end autonomous driving control. arxiv, 2019.
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for prov- ably robust neural networks. In International Conference on Machine Learning, pp. 3578-3586. PMLR, 2018.
Seyed-Mohsen -ezuuol,,,,,, Alhussein Fawzi, Omar Fawzi, and Pascal Frossard. Universal adversarial perturbations. In Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 1765-1773, 2017.
Mark Niklas Mueller, Franziska Eckert, Mare Fischer, and Martin Vechev. Certified training: Small boxes are all you need. In The Eleventh International Conference on Learning Representations, 2022.
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Prima: general and precise neural network certification via scalable convex hull approximations. Proceedings of the ACM on Programming Languages, 6(POPL):1-33, 2022.
Alessandro De Palma, Rudy R Bunel, Krishnamurthy Dj Dvijotham, M. Pawan Kumar, Robert Stanforth, and Alessio Lomuscio. Expressive losses for verified robustness via convex com- binations. In The Twelfth International Conference on Learning Representations, 2024. URL net.
https://appereviiee wwtp:neeetetoeeeeoeeeeeeoeooe Forumm?d==zyy242221
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, et al. Pytorch: An imperative style, high- performance deep learning library. Advances neural information processing systems, 32, 2019.
Dong Qian and William K Cheung. Enhancing variational autoencoders with mutual information neural estimation for text generation. In Proceedings of the 2019 Conference on Empirical Meth- ods in Natural Language Processing and the 9th International Joint Conference on Natural Lan- guage Processing (EMNLP-IJCNLLP), pp. 4047-4057, 2019.
Sriram Sankaranarayanan, Aleksandar Chakarov, and Sumit Gulwani. Static analysis for prob- abilistic programs: inferring whole program properties from finitely many paths. SIGPLAN Not., 48(6):447-458, June 2013. ISSN 0362-1340. doi: 10.1145/2499370.2422199 URL
/ttps::/doi.org//
Sina Shafaei, Stefan Kugele, Mohd Hafeez Osman, and Alois Knoll. Uncertainty in machine learn- ing: A safety perspective autonomous driving. In Computer Safery, Reliability, and Security: SAFECOMP 2018 Workshops. ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Västerås, Swe- den, September 18, 2018, Proceedings 37, pp. 458-464 Springer, 2018
Zhouxing Shi, Yihan Wang, Huan Zhang, Jinfeng Yi, and Cho-Jui Hsieh. Fast certified robust training with short warmup. Advances in Neural Information Processing Systems, 34:18335- 18349, 2021.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev, Fast and effective robustness certification. Advances in neural information processing systems, 31, 20.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certifica- tion of neural networks. In International conference on learning representations, 2018b.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for cer- tifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):1-30, 2019.
13

---

Published as a conference paper at ICLR 2025
Tarun Suresh, Debangshu Banerjee, and Gagandeep Singh. Relational verification leaps forward with RABBit. In The eighty-eighth Anmual Conference on Neural Information Processing Sys- tems, 2024. URL htt.:ttss//ppeeevvee..cccct http://we.....ooommmmooo0000000.
Vincent Tjeng, Kai Y Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations, 2018.
Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, and Gagandeep Singh. Incremental verifica- tion of neural networks. Proc. ACM Program. Lang.. 7(PLDI), June 2023. doi: 10.1145/3591299
URL
Shubham Ugare, Tarun Suresh, Debangshu Banerjee, Gagandeep Singh, and Sasa Misailovic. Incre- mental randomized smoothing certification. In The Twelfth International Conference on Learning
Representations, 2024. httpstss /ttctps://opere /tt:://
net/ forum? d= f
Aaron van den Oord, Oriol Vinyals, and koray kavukcuoglu. Neural discrete representation learn- ing. In I. Guyon, U. Von Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett (eds.), Advances in Neural Information Processing Systems, volume 30, Cur- ran Associates, Inc., 2017. saper/2017/f11ee 0tg.00/44......aoaaaaaeeeaee0000
www.eerrp....pppppeeeeeeeeeeeeee filesi les/
John D. Vedder. An invertible approximation to the normal distribution function. Computa- tional Statistics & Data Analysis, 16(1):119-123, 1993. ISSN 0167-9473. doi: https://oi..rr// 00.10160167--9474493)000000
URL httpt::////e/ sci wcwdecii wwweeeettccooc..ooooomoomo.omeet htt//scienccc ence/
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems 31: An- nual Conference Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Moniréal, Canada, pp. 6369-63699 6379, 2018. URLhittp::/papers.. wwt.sippps..cpppppceoeooecc forma sa fety ana
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 complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34, 2021.
Matthew Wicker, Luca Laurenti, Andrea Patane, and Marta Kwiatkowska. Probabilistic safety for bayesian neural networks. In Conference on uncertainty in artificial intelligence, pp. 1198-1207. PMLR, 2020.
Matthew Wicker, Luca Laurenti, Andrea Patane, Zhuotong Chen, Zheng Zhang, and Marta Kwiatkowska. Bayesian inference with certifiable adversarial robustness. In International Con- ference on Artificial Intelligence and Statistics, pp. 2431 12499. PMLR, 2021.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, pp. 5286-5295, PM.., 2018.
Kai Y. Xiao, Vincent Tjeng, Nur Muhammad (Mahi) Shafiullah, and Aleksander Madry. Training for faster adversarial robustness verification via inducing reLU stability. In International Confer- ence on Learning Representations, 2019. URL hettps://openreviie net forum?id- BJfIVjAckm
Changming Xu and Gagandeep Singh. Robust universal adversarial perturbations. arXiv preprint
arXiv:2206. 10858, 2022.
Changming Xu and Gagandeep Singh. Cross-input certified training for universal perturbations. ECCV, 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 paral- lel incomplete verifiers. International Conference on Learning Representations, 2021. URL
https::/ net wtt.://///ooooo////////e
14

---

Published as a conference paper at ICLR 2025
Chao Yang, Xuyu Wang, and Shiwen Mao. Autotag: Recurrent variational autoencoder for un- supervised apnea detection with rfid tags. In 2018 IEEE Global Communications Conference (GLOBECOM), pp. 1-7, 2018. doi: 10. 10.1099GL00OM.20885555600000
Rem Yang, Jacob Laurel, Sasa Misailovic, and Gagandeep Singh. Provable defense against geo- metric transformations. In The Eleventh International Conference on Learning Representations, 2023. htt.tt:::/peeeeeeeeee.o net/ [omms
Huan Zhang, Hongge Chen, Chaowei Xiao, Bo Li, Duane Boning, and Cho-Jui Hsieh. Towards sta- ble and efficient training of verifiably robust neural networks. arXiv preprini arXiv: 1906.06366, 2019.
15

---

Published as a conference paper at ICLR 2025
A ADDITIONAL PROOFS
Theorem 1. For VAE with encoder N decoder N local input region (1(2)), ervor function M and probability threshold (1 - 6), if Z = {Z 2 = (=(x), x E (r(wo)) then for any support set foor Z the worst case error L Ne, Nd 2o) S (S) where Tus(S) maxzes (NN())).
Proof. Let, (v) (M(y) < 1o) be indicator where to (us(S). Then for any output distribution Y = (2)... P(M(Y) I (o) can be written as Sg+. Ita (N) x fz(=)dz where Z E 2 and fz is the probability density function of Z. Note here E Rd are vectors and dz dzi... dzd. Now since the support set S C g and to (x)) x fz()) Z for all R
/ (x)( x fz(z)dz
P(M(Y) S tt)
R
2 1o (N)( x f2(2)dz given S S R& and 4, (z) x f2(2) 2
2 / [2(2)dz to 4= (w)(S) implies To (z)) = 1
2 (1 8) S support so E P(Z (1
(3)
From Eq. 1 and 3 for any output distribution Y Nd(Z), T(Y) S to. Now, given for all
possible output distributions Y E y T(Y) for the worst-case loss (N N wo) maxyey yy T(Y) < to = (S). Note in all cases we assume the indicator function Ie, (3) is well behaved and both the integrals Is Io (N)) fz(z)dz and JR4 L (N) x fx(2)22 )z is well defined.
Let C(u, 1) = 20 - Pn where Pno R + [0, is the edf of the following gaussian distribution ((,,
Lemma 2. For fixed mean μ E Hurl and bounds 1 < pib. Hub S u. σ <
Tab
C(u,o,u, u, > C(p, Jub, u, I).
Proof.
C, = 4 (u)
+ pio (I)
u /
=
u H
4-1
$
+ Po.1
1 using (z) = 1 (o.1(-2) (4)
Now, since for any μ E [pa, Publ and
S Pib. (μ 1) 2 0, Jub
p-1 n-1
is monotonically increasing.
Hence, L |-_
<
L (=))
Similarly, we show that
do.1
< 2
#-#4
This gives us
4-1
u 4- H - 1 < Po.1
4 111
- p 1
+ Po.1
P
Ouh
Uub
Clu,oubs u, u(,,o,u1)) Using Eq.
4
Lemma 3. For fixed a [o awil and bounds 1 = 44b C, u pub + with Ç 2 0, for any E [bbb)
C(p,, a, u, 2 C(uu, o, 1,1) C(pub: 1,
16

---

Published as a conference paper at ICLR 2025
Proof. First, we show C(U,, u, is symmetric around Muu Ant i... C( + d.
C(Ho- - d, o, u, 1) for all d E [0, w/ 2/2 where w = (Hub pb) is the width of the interval [pio. publ.
C(uo + d, u, 4 Pootde (d $ to (1)
pn
1 - pn d
0
20,1
(5)
0
Now, 140 d Pub + (
Und H4i
Hus tHIB
po + d). Meb + { d -(1
1 Pu Pib - Huh
Mub
Mub
d
(u 14 + d)
2
Using Eq. 5
C(Ho + d, u1 = 10,1
140
d'
20.1
- 140 d
0
Mg + d
M40 + d o
Po.1
20.1
Mo + d 20,1
Ho + d
20.1
using (0,1 = 11-o)-1-00110 (-))
o
= =C(uo d,o,u,1
(6)
Eq.
6
proves C(uu; G, u, C(jub,, Jr u,1) for d = Hung Now we show that for di, d2
[0,
Aus Meh
di I d2 then C(uo + d1, o. 1) 2 C(po + d2, o, u).).
P
110
di
P
140
d2 1
d2
(u (u-1o) mo)
$
( (di (u
mo)
σ
σ
a
0
1
d2
exp (- (x
(u -mo))3
dx
(7)
2To
d1
202
Similarly
1 1o-40 Ho d1
[ (l- Po d2
1
(x (1 22))2
Lo.1
exp
dx
(8)
σ
V2TO
Jdz
20²
Eq 7 Eg
8
gives us
2TTa ( f(x)dx
C(po + 0,,01, - C(1o + 0,
(9)
(x (x- - exp
(x mo))
where (xx exp
20²
20²
Next, we show that f(x) for all [dl,
(x (u 20))² = (w + < x)² < (w + < + x)²
(x - (1 12)o since 0 < d1 S x s
(x- (u (u-))))
(x (1 (1- (1xx-(1_H)) Ho))
exp
> exp
20²
202
f(x) 2 0 where x E [d1, d2l
1 f(x) 2 0 from Eq. 9
C(Ho + d1, or u.() C(po + d2, 0,,1)
C(Ho + d, u.() 2 C(Ho + d,
This completes the proof because for any d [0, M C(po + u. 2 C(pub, o, u. and subsequently C(pa- d, a. u,l) 2 C(Hub; a, I),
Lemma 1. Given bounds pab. Hbub Tib, oub E R, probability threshold (1 (1- and & E R+ Let C(u,o,u,1) & (u) Pu Then dp [pan, [ptb, publ, [ous aut).
Hub S.14 () C(pute anbr Pub + P,b ()
17

---

Published as a conference paper at ICLR 2025
Furthermore,
Cl Jub. Hub + Mm () C(uub Jud. Mub + Meb ()
Proof.
C(u, o, Mub + Si14B - -() 2 C(u, Jubi Uub + C. pib
C) Using lemma 2
2 C(ub. aubs Mub + C. Mib
() Using lemma
The proof of C(uus Tub, Mub + 14 - 5) = C( Jubs Pub + S. Pib
() comes from Eq. 6
Theorem 2. Given {N(,,, σ) μ E Inl.. Mubl. a E [o Jubl]. probability threshold (1 6),
then [1 u] LuB Tu (po)) Mub + J -- (po)] satisfies Equation 2
Where
Po =
min pE((1- (116)
(1) Φ (p-(pp-( 8)) 2
Mib
Plab
Jub
Proof. We would like show that Vi [pmb publ, a E [ore, Cuu 0, Mub + - a (pod)))))) 2 (1- 6). By Lemma
we have vp E [p1 Publ E (ow, Jubl
C(u,o, o, Hub to (po), pmu - (po)) C(pab ubb Mub to ous
Therefore, it is sufficient to prove that
C(pub, Jub, Mub + ous (po), Mib Fus 2 (1-6)
We can start by expanding C(prbo Jubs Mub + ou (p), pib o (w)))
C(pubs uub + oub (p), (p), ows (w)
Musions (Pub ous
(w)) (p)) Mubiouu (146 - Tab -()))
ous Owb
146 ut $ - (01(p) (p) lbu
Jab
σud
x (p)) ②b
|1th
Hhuh
x (p1(pp)
Tub
p Φ
Mib
Pub
+ 11 (p)
Jub
Now, we want s.t.
14b - Mub x-1(p)
p - ①
2 (1-8)
Tub
p - (1 - 6) 2
1ip Hub
② -1p(p)
Tub
Φ 6-'(p- (1 6)) >
Hub
Tb (p)
ub
Φ Φ (1 8)) + Φ -'()) >
p4b
Hub
ub
Note that the t a strictly increasing function. Since Po is defined as the min that satisfies this condition, we have proved the Theorem.
18

---

Published as a conference paper at ICLR 2025
B EVALUATION DETAILS
We implemented CIVET in PyTorch Paszke et al. (0019). For additional details see our codebase. All networks are trained using the Adam optimizer with learning rate of 1e 4 and weight decay 1e - 5. All networks are trained with 100 epochs. We use a batch size 16 for MNIST and 32 for FIRE and CIFAR-10.
B.1 TRAINING METHODS
Standard. Standard training is done using combination of KL divergence loss on the mean/standard deviation and reconstruction loss on the output.
PGD. PGD training is done by mixing standard loss with an adversarial loss. The adversarial loss is computed by first computing an adversarial perturbation using PGD. PGD is instantiated with the same KL divergennccrreconsttuctioo loss combination standard training, we use a step size equal to 0.1 and perform 10 iterations. This adversary is added to the input and then fed through the network to compute the loss.
CIVET. Sticking with standard IBP protocols, we start by warming up with standard loss for the first 250 iterations (250 batches). For the next 250 batches we linearly scale e from and add the CIVET loss to the standard loss. After these warmup stages we compute CIVET loss and add it to standard loss.
CIVET-SABR. We perform the same steps CIVET training but first compute maximum damage attack (MDA) on the input using a radius of (1 7) e setting r 0.1. We then compute smaller ball around this adversarial example with radius and perform normal CIVET training.
B.2 DATASETS
Wireless. We use the same VAE architecture as Liu et al. (2021). The VAE encoder has 7 linear layers: starting with a hidden size of 1024 going down by factor of each time, the VAE decoder as the same sizes in the opposite direction. We use a latent dimension of 50. All layers use LeakyReLU activations with a tanh activation at the end. With e = 25%. standard training took 18 minutes, adversarial training took 25 minutes, and CIVET training took 1 118 minutes.
Vision. We use convolutional layers with a kernel size of 5, stride of 2, and a padding of 1. We use three convolutional layers starting with 16 (64 for CIFAR) channels and doubling each time. For MNIST we use latent dimension of 32 and for CIFARIO we use a latent dimension of 64. All layers use ReLU activations with sigmoid activation at the end. With training took 16 minutes, adversarial training took 18 minutes, and CIVET training took 93 minutes. For the fully connected MNIST network, there 2 hidden layers with size 512 and with size 10 for both the encoder and decoder. Lipschitz VAE with GroupSort activations took 24 minutes to train and /method with ReLU activations took 41 minutes train.
0.3 for MNIST, standard
C EXAMPLE FOR SAMPLE SELECTION
This section elaborates on the key steps of the support selection algorithm with an example. We consider the one-dimensional case for simplicity. Let the ranges of the mean and variance be the intervals [μb, (4b,) Mus]] and [ozs, ant), where μıb 0.0, Pub = 1.0, au = 1.0, and oub 2.0. For fixed 5 0.05 (i.e., a 95% confidence level), the algorithm computes an interval [1, u] that captures least 95% of the probability for all possible Gaussian distributions with μ [148, [ub] and [an, awol-
From Lemma [] for any S μul and μi I u, we know that the distributions specified by μib, Fub and Mub; Guh capture the least probability among all possible distributions. Additionally, since (1 11-8) 8)= 0.5, both and u automatically satisfy the constraints S μb and Pub I u. Therefore, finding the support set [,, ui] only requires ensuring that both the distributions specified by oub and pub. uub capture at least (1 - 5) probability. Finally, the bounds and u are obtained by applying Theorem
uub
where 1 0.0 3.54 3.54 and u 1.0 + 3.54 4.54.
19

---

Published as a conference paper at ICLR 2025
D JUSTIFICATION OF THE WEIGHTING SCHEME
In this section, we explain the rationale for using the weighing scheme to define the CIVET loss (Definition. 2) For Gaussian distribution, most of the probability mass is concentrated around the mean. This means that the support set [7, u] (or its length in the 1D case) grows significantly faster than the additional probability it captures. For instance, for any Gaussian distribution with parameters (14, o), the interval (u- 30, + 3øj captures 99.73% of the probability mass, while extending it to (0 - 44, + 4o] increases the coverage to only 99.99%. Thus, the support length must increase by 33% to capture just an additional 0.26% of the probability. Moreover, IBP with larger intervals accumulates greater approximation error. Using the suggested weighting scheme, (1 - C; would unnecessarily assign very high weights to larger intervals, which generally capture negligible additional probability mass compared to the smaller intervals (i.e., [l--1, Uj-1) corresponding to (1 - 64-1).
E ADDITIONAL DISCUSSION ON FIRE
FIRE Liu et al. (2021) uses a VAE architecture to predict downlink channels inspired by a physics- level intuition that both uplink and downlink channels are generated by the same process from the underlying physical environment. A VAE can first infer latent low-dimensional representation of the underlying process of channel generation by observing samples of the uplink channel, and then generate the downlink channel by sampling in this low-dimensional space. This allows the VAE to embed real-world effects in the latent space and therefore capture the generative process more accurately.
For FIRE we compare performance using SNR. The SNR of the predicted channel H can be com- puted by comparing to the ground truth channel Hgt by using the following:
[1 - Hgr
SN R(H, Hgt) -10logo
(10)
F LIMITATIONS
CIVET currently restricts support set selection to the interval domain; however, more precise sup- port selection may be possible with the zonotope domain (as commonly used in DNN verifica- tion (ingh et al. (200)228)) Sa)) or the octogon domain (as commonly used in probabalistic programming
Sankaranarayanan et al. (2013)) ) we leave this for future work explore. CIVET focuses on the gaussian distribution as commonly used in VAEs; however, it is possible to generalize our method to
families of distributions as in Berrada et al. (20TT) CIVET assumes an adversary is attacking with single-input adversarial examples; however, the RAFA attack used by Liu et al. (2023) to attack FIRE a universal adversarial perturbation which is a weaker attack model. It may be possible to obtain better performance by adjusting CIVET to handle universal attacks instead. Recent work in attacks Deosavi-Dezfooli et al. (2017); Liu et al. (2023); Xu & Singh (2022). certification Banerjee et al. (2024c); [Banerjee& & Singh (2024); Suresh et al. (2024) and certified training for UAPs Xu & Singh (2024) suggest that improved accuracy with similar robustness is possible when defending against these weaker attack models; however, leave this for future work.
G CIVET-SABR
We present results using SABR Mueller et al. 2022)) a state-of-thh--s certified training method.
SABR works by first computing an adversarial attack and then propagating a small adversarial box around that adversarial attack rather than propogating the entire input region. Mueller et al. (2022) note that although this training method is now unsound the approximation errors are significantly less resulting in lowered regularization and increased perfornace. We compute a maximum damage attack to find an adversarial example in the input space. We then compute smaller bounding box
(T 0.1, i.e. Lxo ball with tenth the attack radius) around the adversarial example propagating this box through the network. In our preliminary testing we found that for CIFAR- 8/255 we get baseline performance of 0.0054 < 0.0062 and certified performance of 0.0151 < 0.0153. Here
20

---

Published as a conference paper at ICLR 2025
find that using these smaller bounding boxes increases performance both metrics with an especially large increase in the baseline performance (inline with observations from SABR). Our paper focuses introducing the idea of support sets for certified VAE training and is orthogonal to developments standard certified training. We leave additional performance gains achievable by combing CIVET with other methods for future work.
H ABLATION FIGURE
Slandard
Standeri
15
14
14-
12-
13
0.10
pifference
Figure 3: Standard and Certified SNR while varying D. We consider sets with 8, 0.05 and
= 8141 + (let n [D]. the left, we vary the size of DD between I and while fixing
7 0.15. On the right, we fix [D] and vary 17 between 0.05 and 0.25.
21


Reviews:
[{"review_id": "rz2DbHDND2", "reviewer": "Reviewer_7PDy", "summary": "This paper explores the certification and related questions of VAEs. VAEs are a type of neural network with outputs that contain probability distributions; therefore, standard certifiable robust training does not work for them. The authors first introduce a theoretical framework called support sets to bound the worst-case loss, and then provide an algorithm to select a set of supports.  Based on this, the authors introduce the concept of CIVET loss and design a training algorithm using CIVET loss. They show that CIVET training performs better compared to standard and PGD training methods on various datasets and better than Lipschitz VAEs.", "questions": "1. Did the authors compare CIVET to more training methods?\n\n2. Between baseline and certified performance, does this paper consider one more important than the other?\n\n3. Is 3.8e-3 vs 4.9e-3 indeed a big improvement?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. This paper has a solid theoretical foundation and provides a results table to show its good performance. In Table 1, compared to standard and PGD training, CIVET training outperforms in all cases in the Certified column with a significant advantage. Compared to Lipschitz VAEs, CIVET training obtains better baseline performance with comparable certified performance.", "weaknesses": "1. Also in Table 1, in the Baseline column, CIVET training is never the best and is sometimes significantly worse, while PGD and standard trainings usually are close in performance. \n\n2. Compared to Lipschitz VAEs, the improvement in baseline performance (3.8e-3 vs 4.9e-3) does not look amazing, and for certified performance, CIVET is not better than Lipschitz VAEs. \n\nConsidering these two points, although CIVET shows good performance, it is hard to consider it as SOTA.", "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": "kYmbSb0AqX", "reviewer": "Reviewer_Wi5q", "summary": "The submission presents CIVET, a novel algorithm to perform certified training of VAEs.\nDifferently from a previous work that does this by building a low-Lipschitz network, the authors devise a way to do certified training using network relaxations (bounding techniques). \nIn order to be able to do so, the authors present a way to find a \"support set\": a set of allowed latent space perturbations that captures a probability mass (under the considered adversarial model) at least as large as the probability with which the networks needs to be verified.\nOnce this is in place, the computation of an upper bound to the worst-case loss to be employed at training time mirrors the procedure employed for standard feedforward networks.\nExperimental results on vision and on a wireless communications dataset are presented.", "questions": "- Can you please discuss the similarities and differences between your approach (mainly, the idea to use a support set), and the techniques to perform BNN verification and IBP training introduced by (Wicker et al., 2020) and (Wicker et al., 2021)? I believe they also rely on bounding boxes (on the weights perturbations) which then allow to rely on techniques from standard feedforward networks.\n- A series of certified techniques, including the cited (Balunovic and Vechev, 2020), (Mueller et al., 2022), (Mao et al., 2023) and [1,2,3], proposes to use a mix of adversarial training and network bounding to improve both certified accuracy and standard performance. It would be nice to acknowledge these developments in the related work section. It would be even better if the authors could test some of these ideas on CIVET: would such techniques improve performance in this context too?\n- Could you please elaborate on the choice of the specific weighting for the various losses associated to each delta? Why not something like $\\sum_i (1 - \\delta_i) \\mathcal{L}_i$? How was the $\\mathcal{D}$ set obtained in the experiments? Are these all hyper-parameters? Looking at Figure 3, it would seem like some tuning was carried out.\n- What is the $\\delta$ employed for the certification in Table 1, section 4.2 and Figure 3? \n- The output of a verification query is binary ({True, False}). What does certified performance mean, in this context, then? How is the provided number obtained from the framework from (Berrada et al., 2021)?\n- Could it be possible to compare against Lipschitz VAEs on CIFAR-10?\n- Can Table 1 include a comparison in terms of empirical robustness to previously-published VAE attacks? Many are cited in (Barrett et al, 2022).\n------\n\n[1] Xiao et al.. Training for faster adversarial robustness verification via inducing relu stability. ICLR, 2019.\n\n[2] Fan and Li. Adversarial training and provable robustness: A tale of two objectives. AAAI, 2021.\n\n[3] De Palma et al.. Expressive losses for verified robustness via convex combinations. ICLR, 2024.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "The idea of computing a \"support set\" associated with the desired verification probability to then be able to use techniques from standard feedforward networks to upper bound the worst-case loss is novel to the best of my knowledge. I think this is an elegant solution to the VAE certified training problem.\nThe technical contributions (how to determine the support set) are also non-trivial. \nThe wireless communication benchmark provides a very solid motivation to the approach, providing a compelling non-vision benchmark (not common in certified training).", "weaknesses": "I think the paper would definitely benefit from some polishing on the writing side, and from a more detailed and reproducible experimental section.\n\nOn the writing side, I think some examples (perhaps in an appendix) would definitely aid the reader in section 3. I found Figures 1 and 2 to be helpful in this regard, but not very readable when printed (especially if in black and white). \nSometimes concepts are introduced before being explained: for instance, in line 325 the fact that there is a list of deltas. It is not until the experimental section that it is clarified that these are given to the algorithm.\nSome design choices (such as the weighting of the for the various losses associated to each delta) are not well-justified.\nSection 4.2 would definitely benefit from a table view of the presented results.\nIt would also be nice to have an appendix providing more details on the FIRE dataset (why a VAE is used there, what is the rationale, etc).\n\nFurthermore, plenty of details are omitted from the experimental section (and the associated appendix). Given that the code is omitted (it is promised by the authors, yet not provided), at the very least one should get a complete description of the experiments. The training schedule and hyper-parameters are, for instance, unclear. Same goes for the (rather important) details of the adversarial training baseline. Additional examples in the questions below.\n\nConcerning the experiments themselves, I found some of the results/claims to be somewhat surprising, and worthy of further discussion. In certified training for feedforward networks, IBP typically incurs a very large standard performance cost. The authors, nevertheless, say that \"*CIVET obtains significantly better certified performance without sacrificing much baseline performance*\". It does not seem to be the case for more challenging datasets at larger perturbations (CIFAR-10, 8/255), where performance is significantly reduced. \nFurthermore, the results from the Lipschitz VAEs are provided only for MNIST. However, this is quite an important baseline. One could for instance extrapolate that Lipschitz VAEs perform better at larger epsilons. Would it be the case on CIFAR-10? \nFinally, I was also surprised to see that the only attack from previous work being tested as a UAE physical attack on the FIRE benchmark. Could the weakness of the attack (imposed, for instance, by the universality constraint) be behind the superior empirical robustness of CIVET compared to PGD? In the certified training literature, it is typically assumed that certified training comes at an empirical robustness cost, provided the adversarial training baseline is strong enough.", "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": "kSup3tq5DR", "reviewer": "Reviewer_BKMJ", "summary": "Variational Autoencoders (VAEs) have been shown to be susceptible to adversarial attacks, but can be trained to become more empirically robust to such attacks using adversarial training which employs an underapproximation of the worst-case loss. However, training certifiably robust VAEs is difficult due to the fact that for a given input, the encoder usually generates the parameters of a distribution in the latent space instead of a concrete vector. The authors show that by finding a support set for the latent space distributions, one can derive an upper bound of the worst case loss using standard interval propagation methods. The authors introduce a method for finding support sets in a restricted space which result in tight upper bounds. These sets can then be used to compute a concrete upper bound of the loss which forms part of the CIVET training algorithm presented in the paper. CIVET is evaluated on a VAE for a wireless networking problem and computer vision problems where it outperforms standard and adversarial training in terms of certified performance. When compared to Lipschitz VAEs as a baseline for certifiably robust VAEs, it achieves comparable certified performance while enjoying an improved standard performance.", "questions": "- What are the main reasons for the long runtime of the CIVET algorithms compared to other algorithms? Is there any way of possibly accelerating the proposed method?\n- Could the authors provide the training times for the Lipschitz VAEs?\n- Do the authors have any additional experimental results which compare their method to other method for obtaining certifiably robust VAEs?", "limitations": "", "rating": 5, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- The presented method is sound and theoretical results are accompanied by thorough proofs\n- CIVET achieves significantly higher certified performance than standard and PGD training\n- The method is novel and allows for certified training of standard VAE architectures", "weaknesses": "The experimental results are somewhat underwhelming. Table 1 shows that CIVET achieves lower standard performance than standard and PGD training but higher certified performance. The decreased standard accuracy is to be expected given the fact that certified training has an implicit regularisation effect [1]. The increased certified accuracy here is also expected given that the loss in standard and adversarial training does not favour certified robustness in any way. These are very weak baselines in terms of certified accuracy and it is not surprising that CIVET would outperform them in terms of certified performance. Section 4.4 also only compares CIVET to those baselines. The more interesting baseline are the Lipschitz VAEs since these are designed to be certifiably robust. I find the results in section 4.2 difficult to process in their current form, but they are not that convincing in my opinion (slightly better baseline performance and similar certified performance).\n\nGenerally, the experimental evaluation is somewhat underdeveloped since only two experiments which compare the approach to a baseline for certifiably robust VAEs are conducted ($\\epsilon=0.1$ and $\\epsilon=0.3$ on MNIST and one model). Additional experiments on different epsilon sizes/datasets or experiments varying the latent space dimensions/network depths should be run to provide a more thorough comparison.\n\nThe authors should also move at least some of the information on the runtimes to the main part of the paper. Training VAEs using CIVET takes ~10x as long as standard training. This is extremely expensive, even for a certified training method, yet is not discussed in the paper at all. A proper runtime comparison between the algorithms, including the time needed for training Lipschitz VAEs, should be added to make a comparison possible, for example using a table.\n\nDue to the above points I believe that this paper would significantly benefit from another revision cycle, allowing for the extension of the experiments section so a proper comparison between the work and other methods is possible.\n\n## Minor points\n- Line 490: CIVET maintains its lead against real-world attacks --> The decreased standard accuracy compared to other training methods could be mentioned here\n- The results in Section 4.2 should be summarised in a table, at the moment they are very hard to process since they're only given in the text\n\n## Literature\n[1] Mao, Y., Mueller, M.N., Fischer, M. & Vechev, M. (2023) Understanding Certified Training with Interval Bound Propagation.\n\n\n## Editorial\n- Line 93: an approximated posterior distributions --> an approximated posterior **distribution**\n- Line 102: The abbreviation \"SNR\" is used before it is explained\n- Line 131: Then refines the network --> **The method** then refines the network\n- Line 185: the worst case error (...) --> the worst case error **is**\n- Line 192: possible output distribution --> possible output distribution**s**\n- Line 203f: finding appropriate subset --> finding **an** appropriate subset\n- Line 203: compute non-trivial upper bound --> compute **a** non-trivial upper bound\n- Line 259: So only picking support --> So only picking **a** support\n- Line 264 (caption of Figure 2): The caption defines $S_\\delta = [\\mu_{lb} + \\zeta, \\mu_{ub} + \\zeta]$, I think this should be $S_\\delta = [\\mu_{lb} - \\zeta, \\mu_{ub} + \\zeta]$ (wrong sign for the lower bound of the interval)\n- Line 271: Let's first consider 1d case --> Let's first consider **the** 1d case\n- Line 278f: the interval $[l, u]$ always includes the interval $[\\mu_{lb} + \\mu_{ub}]$: Not sure what is meant here, should this be $[\\mu_{lb}, \\mu_{ub}]$\n- Line 318: gives us a way to find support set --> gives us a way to find **a** support set\n- Line 327: we weight them based on --> we **weigh** them based on\n- Line 365: implemented CIVET in in PyTorch --> implemented CIVET **in** PyTorch (remove one \"in\")\n- Line 459: A network is $f: [...]$ is Lipschitz continuous --> A network $f: [...]$ is Lipschitz continuous (remove one \"is\")\n- Line 466: Lipchitz --> Lip**s**chitz\n- Line 480: We leave further study of $\\mathcal{D}$ selectin --> We leave further study of $\\mathcal{D}$ selecti**o**n\n- Line 511: using IBP to obtain certfied --> using IBP to obtain cert**i**fied", "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)