Verification of Generative-Model-Based Visual Transformations
Authors: Matthew Mirman
Timon Gehr
Martin Vechev
Venue:  (2020)
Keywords: robustness certification
formal verification
robustness analysis
latent space interpolations

Abstract: Generative networks are promising models for specifying visual transformations. Unfortunately, certification of generative models is challenging as one needs to capture sufficient non-convexity so to produce precise bounds on the output. Existing verification methods either fail to scale to generative networks or do not capture enough non-convexity. In this work, we present a new verifier, called ApproxLine, that can certify non-trivial properties of generative networks. ApproxLine performs both deterministic and probabilistic abstract interpretation and captures infinite sets of outputs of generative networks. We show that ApproxLine can verify interesting interpolations in the network's latent space.

Under review as a conference paper at ICLR 2020
VERIFICATION OF VISUAL TRANSFORMATIONS
GENERATIVE-MODEL-BBBHH
Anonymous authors Paper under double-blind review
ABSTRACT
Generative networks are promising models for specifying visual transformations. Unfortunately, certification of generative models is challenging as one needs capture sufficient non-convexity so to produce precise bounds on the output. Existing verification methods either fail to scale generative networks or do not capture enough non-convexity. In this work, we present new verifier, called APPROXLINE, that can certify non-trivial properties of generative networks. APPrOXLInE performs both deterministic and probabilistic abstract interpretation and captures infinite sets of outputs of generative networks. We show that APPROXLINE can verify interesting interpolations in the network's latent space.
INTRODUCTION
Neural networks are becoming increasingly used across a wide range of applications, including facial recognition and autonomous driving. So far, certification of their behavior has remained predominantly focused on uniform classification of
balls (Gehr et al. 2018) Katz et al.
2017 Wong et al. 2018 Gowal et al., 2018 [Singh al., 2018 Raghunathan al. 2018: Tieng et al. 2017 Dvijotham et al. 2018h Salman et al. 2019 Dvijotham et al. 2018c Wang et al. 2018
which to capture invisible perturbations.
However, a system's 's safety can also depend on its behavior on visible transformations. For these reasons, investigation of techniques certify more complex specifications has started take place
(Liu et al. 2019 Dvijotham et al., 22118| Singh et al. 2019). Of particular interest is the work of Sotoudeh Thakur (2019) which shows that if the imputs of network are restricted to line segment, the verification problem can sometimes be efficiently solved exactly. The resulting method has been used to certify non-norm- norn-buudeed properties of ACAS Xu networks (Julian et al. 2018) and improve Integrated Gradients (Sundararajan et al. 2017).
This work We extend this technique in two key ways: (i) we demonstrate how to soundly approximate EXACTLINE, handling significantly larger networks faster than methods based on sampling can (a form of deterministic abstract interpretation), and (ii) we use this approximation provide guaranteed bounds the probabilities of outputs given distribution over the inputs (a form of probabilistic abstract interpretation). We believe this is the first time probabilistic abstract interpretation has been applied in the context of neural networks. Based on these techniques, we also provide the first system capable of certifying interesting properties of generative networks.
Main contributions Our key contributions are:
A verification system APPROXLINE, capable of flexibly capturing the needed non-convexity.
A method to compute tight deterministic bounds on probabilities with APPROXLINE, which is to our knowledge the first time that probabilistic abstract interpretation has been applied to neural networks.
An evaluation on autoencoders for CelebA, where we prove for the first time the consistency of image attributes through interpolations.
The first demonstration of deterministic verification of certain visible. highly non-convex specifications, such as that classifier for "is bald" is robust to different amounts of "moustache," that classifier n. is robust different head rotations, shown in Figure

---

Under review as a conference paper at ICLR 2020
TE
13
35
Exact Execution
1
32
A
C1
C22
35
APPROXLINE
.13
.1:3
Execution
72
.09
.12
72
LDG
07
Figure I: Using APPROXLINE to find probability bounds for a generative specification over flipped images. Green polygonal chains represent activation distributions at each layer exactly. Blue boxes are relaxations segments highlighted by yellow boxes. We label regions with their probabilities.
2 OVERVIEW
Here, we introduce the terminology of robustness verification and provide an overview of verification technique. Let N: Rm + R= neural network with m inputs and n output classes which classifies an input æ E 1 class arg max; (x)).
Specification A robustness specification is a pair (X, Y) where X C R is a set of input activations and V IR is set of permissible outputs for those inputs.
Deterministic robustness Given specification (X, Y). a neural network N is said to be (X, Y))robust for all E X, we have N (a:) Y. In the adversarial robustness literature, the X is usually an 12- or -ball, and Y is a set of outputs that correspond to specific classification. In case, X shall be line segment connecting two encodings. The deterministic verification problem is to prove (ideally with 100% confidence) that network is deterministically robust for a single specification. As deciding robustness is NP-hard (Katz al.) 2017), the problem frequently relaxed to permit false negatives (but not false positives) and solved by sound overapproximatiio.
Probabilistic robustness Even if N not completely robust, it may still useful to quantify its lack of robustness. Given a distribution μ over X. we are interested in finding provable bounds on the robustness probability Prz=p (N(x)) E YJ. which we call probabilistic [robustness] bounds.
2.1
VERIFYING INTERPOLATION SPECIFICATIONS
It is well known that certain generative models appear to produce interpretable transformations between outputs for interpolations of encodings in the latent space (Dumoulin et al. 2016 Mathieu
al. 2016
Bowman al.) 2015 Radford et al. 2015 Mescheder et al. 2017 7 Ha & Eck 2017 Dinh
et al.
Larsen et al. 2015 Van den Oord et al. 2016 Lu et al. 2018 He et al. 2201)) I.c., as we move from one latent vector another, there interpretable attributes of the outputs that gradually appear or disappear. This leads to the following verification question: given encodings of two outputs with number of shared attributes. what fraction of the line segment between the encodings generates outputs sharing those same attributes? To anwer this question, we can verify a generator using trusted attribute detector, or we verify an attribute detector based on trusted generator. For both tasks, we have to analyze the outputs of neural networks restricted to line segments.
2016
piecewise- linear neural networks restricted to such line segments AB R" It is visualized in the top row of Figure where a line segment eTe9 C IR" between encodings produced by an encoder neural network ne is passed through decoder n. and attribute detector 72,4. In more detail, the primitive P(N l computes polygonal chain (P,..., Pk) in IR" representing the line segment AB, such that the neural network N is affine on the segment P. P..... 1 for all 0 < i k. As consequence, the polygonal chain (N (N(P))..... N(P))) represents the image of AB under N.
EXACTLINE Sotoudeh Thakur (2019) computes succinct representations
2

---

Under review as a conference paper at ICLR 2020
To compute this, one incrementally compute normalized distances the input segment AB for the output of each layer i of the network, N, Specifically, we find = t,,1 S .... S tikk, = 1 B)), and keep track of the nodes (A + (A B)). In the case of afîne operations such as matrix multiplication or convolution, one can simply apply that operation to each node and leave the distances unchanged. The case of ReLU more segments may be introduced. To compute ReLU, one can apply it per-dimension, d, and check for each 0 j < k2 whether [A + (A - B))a < 0 < (A + t1.++ (A - B))a- In this case, a new distance is computed: t' = tz.j (N B.
such that N; is affine on (A + (A - (A + t1.-
This is done analogously in the case where the segment is decreasing in dimension d insteed of increasing.
(4
We extend EXACTLINE to perform exact probabilistic inference by associating with each segment Pj in the chain a probability distribution My over that segment, and probability Pj. In the case of the uniform distribution, as in Figure] D
every μj is also a uniform distribution, and pj 1,+1 1j-
APPROXLINE Unfortunately, EXACTLINE sometimes scales poorly for tasks using generative models, because too many line segments are generated. We improve scaling by introducing a sound overapproximation. APPROXLIIE. Instead of maintaining single polygonal chain, APPROXLINE maintains a list of polygonal chains and a list of interval constraint such that the neural network's activations are guaranteed to either lie on one of the polygonal chains or to satisfy one of the interval constraints. We introduce a novel relaxation heuristic, which chooses subsets of line segments in polygonal chains and replaces them with interval constraints that subsume them. Our relaxation heuristic attempts to combine line segments that are adjacent and short.
To perform probabilistic inference, each element also carries its probability. For feed-forward network, each operation acts on the elements individually, without modifying the probability associated with it. This is shown in the bottom row of Figure [ Here, the probabilities of the segments that get approximated are shown by the yellow regions in the top row. One can observe that they remain unchanged when converted to intervals (in blue) in the bottom row. One can also observe that probabilities associated with intervals do not change, even when the intervals change substantially. Python pseudocode for propogation of APPROXLINE is shown in Appendix A
To understand the interaction between probabilistic inference and the relaxation heuristic, it is best to work through a contrived example. Suppose we have an EXACTLINE in two dimensions with the nodes (1, 1), 2), (3, (5, 1), (7,5) with weights 0.1, 0.1, 0.5, 0.3 on its segments. The weights the output being on each segment respectively, where distributions on describe the probabilities uniform. Our relaxation heuristic might combine the line segments with the segments themselves
nodes (1, 1), (2, 2) and (2. 2), (3, 2) and approximate them by a single interval constraint with lower bound (1, 1) and upper bound (3. 2). (Lee., the first component is between 1 and 3, and the second component is between and 2.) In this case, we can understand the output of approximation as an APPROXLInE: An interval constraint with center (2, 1.5), radius 0.5) and weight 0.1 + 0.1 0.2, as well as a polygonal chain formed of the segment (3, 2), 1) with weight 0.5 and the segment (5, 1),7, 5) with weight 0.3. To compute a lower bound on the robustness probability, we would sum the probabilities of each element where it can be proven there is violation. For example, assume that only the point (1, 2) is disallowed by the specification. The inferred robustness probability lower bound would be 0.8. To compute an upper bound on the robustness probability, we sum the probabilities of each element where it can be proven that at least one point is safe. Here, we obtain 1.
RELATED WORK
Dvijotham et al. (2018a) verify probabilistic properties universally over sets of inputs by bounding the probability that dual approach verifies the property. In contrast, our system verifies properties that are either universally quantified or probabilistic. However, the networks we verify are multiple orders of magnitude larger. While they only provide upper bounds on the probability that a specification has been violated, we provide extremely tight bounds on such probabilities from both sides. PROVEN (Weng al.) 2018) uses sampling to find high confidence bounds (confidence intervals) the probability of misclassification. While PROVEN only provides high confidence bounds (99.99%), APPROXLINE provides bounds with 100% confidence. Nevertheless, our method is much faster and
I Lists of abstract domains are described later Union and Powerset domains.
3

---

Under review as a conference paper at ICLR 2020
produces better results than similar sampling- canplingg-bsed technique for finding confidence intervals using Clopper & Pearson (1934) (used by smoothing methods). Another line of work smoothing, which
provides defense with high confidence statistical robustness guarantees (Cohen et al. 2019 Lecuyer et a 2018 Liu et al. 2018 Li et al. 2018 Cao & Gong 2017). In contrast, APPROX LINE provides deterministic guarantees, and is not defense.
4 REVIEW OF ABSTRACT INTERPRETATION
We briefly review important concepts. closely following their presentations given in previous work (Gehr et al. 2018) where applicable. In our work, we assume that we can decompose the neural network as sequence of piecewise-lineal layers: N = [ .... L1.
An abstract domain (Cousot & Cousot 1977) is a set of symbolic representations of sets program states. We write An to denote an abstract domain whose elements each represent an element of P(RR), ), in our case set of vectors of n neural network activations. The concretization function 7n An P(R") maps symbolic representation
A,, to its concrete interpretation as a set
X E P (R") of neural network activation vectors.
The concrete transformer Ty: P(RT) + P(RR) of some function f: R E maps subsets
X S 1nTh of the domain of f to their image under f. i... Tx(X) = {f(x) x E Xj. Using this notation, the (X, robuustesss property of neural network N can written as (X C Y.
An abstract transformer T. Am + An transforms symbolic representations to symbolic representations overapproximating the effect of the function f: IR" + R", which means it is required to satisfy Ty(mm (a)) S (T (a)) for all a E Am.
Abstract transformers are compositional: For given functions f: RR and g: RM + R' with abstract transformers T A. + A., and T# Am + Ar. we can define an abstract transformer T Am + An, for their composition go R + R". namely T/ = T o T# We will follow this recipe for the neural network N, abstracting as T T ..... T
Abstract interpretation provides sound, typically incomplete method to certify neural network robustness. Namely, to show that a neural network N: R + Rn is (X, Y)-robust, it suffices to show that (T (a)) S Y. for some abstract element E Am with X C (a).
Box domain An element of the box domain B, is pair of vectors b (c, d) where c, d R". The concretization function is (c. d) = {c + diag(d) :3 B e [-1, 1]" Abstract interpretation with the box domain equivalent bounds propagation with standard interval arithmetic.
Powerset domain Given an abstract domain A. elements of its powerset domain P(A), are (finite) sets of elements of A,, The concretization function is given by 7n (a) = Un Vn (a') (using the concretization function of the underlying domain A). We can lift any abstract transformer for A to an abstract transformer for (AA) by applying the transformer to each of the elements.
Union domain Given abstract domains A and A', an element of their union domain is a tuple (a,a') a') with a E An and a' A', The concretization function is 7n (a, a') = 7h (a) U (a'). We can apply abstract transformers of the same function for A and A' to the tuple elements independently.
4.1 PROBABILISTIC ABSTRACT INTERPRETATION
We denote as ID, the set of probability measures over R Probabilistic abstract interpretation is an instantiation abstract interpretation where deterministic points from 1 are replaced by measures from D.,. Le., a probabilistic abstract domain (Cousot & Moneraul 2012 is set of symbolic representations of sets of measures over program states. We again use subscript notation to determine the number of activations: probabilistic abstract domain A, has elements that each represent an element of P PDD.). ). The probabilistic concretization function 7n2 A,, - P(D,.) maps each abstract element the set of measures it represents.
4

---

Under review as a conference paper at ICLR 2020
For measurable function f: Rm - R", the corresponding probabilistic concrete transformer Ty: P(Dm) + ((),)) maps a set measures M _ Dm to a set measures M' [ Dn, given by
M'
Pr [f(z)) E V p e M zmp
where Y ranges over measurable subsets of IR..
A probabilisticc abstract transformer T Am - An abstracts the probabilistic concrete transformer in the standard way: it satisfies Va Am (y(m E (T (a)), as in the deterministic setting.
Probabilistic abstract interpretation provides sound method to compute bounds on robustness probabilities. Namely, to show that PVv Y [L, u]. it suffices show that r/() [1. u] for each / E Yn NT (a))
for some a with j E Yim (a).
Domain lifting Any deterministic abstract domain can be directly interpreted as probabílistic abstract domain, where the concretization of an element is given as the set of probability measures whose support subset of the deterministic concretization. The original deterministic abstract transformers can still be used.
Convex combinations Given two probabilistic abstract domains A and A', we can form their convex combination domain, whose elements are tuples (a, a' p) with E Ans a' A', and p E [0, 1]. The concretization function given by (a, a p) = {(1 p) u p p μ E 7n. 1d' 7/n (a')). We can apply abstract transformers of the same function for A and A' to the respective elements of the tuple independently, leaving intact.
Similarly, given a single probabilistic abstract domain A, elements of its convex combination domain are tuples (a, A) where a E A A [0, 11 and Σ A = 1 for some k. The concretization of an element is given by (n, A) {Σ X #4 μ4 7n (a:), i (1,...,k)} We can apply abstract transformers for independently to each entry of a, leaving À intact.
APPROXLINE
Here we define APPROXLINE, its non-convex relaxations, and its usage for probabilistic inference.
5.1 DEFINITION AS AN ABSTRACT DOMAIN
First, note that we can use EXACTLINE to create an abstract domain E. The elements of &,, are polygonal chains (PI,... ......,,, Pk) in 1" for some k. The concretization function 7n maps a polygonal chain (PI,...,P) Pt) in I2 to the set of points in R that lie on For piecewise- lineer function f: T. + R", its abstract transformer 7 Em + En maps a polygonal chain (PI...., Ps) in RT to a new polygonal chain in IR" by concatenating the results the EXACT primitive on consecutive line segments P,P++1. eliminating adjacent duplicate points and applying the function If to all points. The resulting abstract transformers are exact, i.e., they satisfy the subset relation in Va E Am. Ty (7m((a) S (T (a)) with equality.
Our abstract domain is the union of the powersets of the EXACTLINE and box domains. Therefore, abstract element is tuple of set of polygonal paths and set of boxes, whose interpretation is that the activations the neural network in a given layer are on one of the polygonal paths or within one of the boxes. For 31, R", write S(11, element that represents single line segment connecting x2 and xzg Like Ex EXACTLING we focus on the case where the abstract element describing the input activations captures such line segment.
(((x1, }, ()) to denote the abstract
Note that if we use the standard lifting of abstract transformers T for the EXACTLINE and box domains into our union of powersets domain, propagating a segment (Z) through the neural network = L o
L1 using the abstract transformer T = T o... T is equivalent to using only the EXACTLINE domain: As the standard lifting applies the abstract transformers to all elements of both sets independently, we will simply obtain an abstract element ([(P)....,PP, ()), where (Pi,... Pt) is polygonal path exactly describing the image of 21 under N.
... ....
5

---

Under review as a conference paper at ICLR 2020
Relaxation Therefore, our abstract transformers may. before applying lifted abstract transformer, apply relaxation operators that turn an abstract element a into another abstract element such that (a)(a) S Yn (a'). We use two kinds of relaxation operators: bounding box operators remove single line segment, splitting the polygonal chain into at most two new polygonal chains (at most one on each side of the removed line segment). The removed line segment is then replaced by its bounding box. Merge operators replace multiple boxes by their common bounding box.
Carefully applying the relaxation operators, we can explore a rich tradeoff between the EXACTLINE domain and the box domain. Our analysis generalizes both: if we never apply any relaxation operators, the analysis reduces to EXACTLINE, and will be exact but potentially slow. we relax the initial line segment into its bounding box, the analysis reduces to box and be will be imprecise but fast.
Relaxation heuristic For our evaluation, we use the following relaxation heuristic, applied before each convolutional layer of the neural network. The heuristic is parameterized by relaxation percentage p E [0, 1] and a clustering parameter &o E N. Each chain with t > 1000 nodes is traversed from one end the other, and each line segment is turned into its bounding box, until the chain ends, the total number of nodes visited exceeds 1/k or we find a line segment whose length is strictly above the p-th percentile, computed over all segment lengths in the chain prior applying the heuristic. All bounding boxes generated in one such step (from adjacent line segments) are then merged, the next segment (if any) is skipped, and the traversal is restarted on the remaining segments of the chain. This way, each polygonal chain is split into some new polygonal chains and a number of new boxes.
5.2 PROBABILISTIC INFERENCE
The EXACTLINE domain can be extended such that it captures a single probability distribution on a polygonal chain. For each line segment (P., P:+1) 1) on the polygonal chain (PI...., Px) in R", we additionally store a symbolic representation of a measure 14, on [0, 1], such that Σk-1 (4, 1]) = 1.
The abstract element (PI.M1.1 P2. Pk- 1k- Pk)) then represents the probability measure
Σ M4 ((
x (1P---- P.1l2 meXNPPPH)
Pilla
where X ranges over measurable subsets of R" Le., we have (a) = (2}. Whenever an abstract transformer splits line segment, it additionally splits the corresponding measure, appropriately applying affine transformations, such that the new measures each range over [0, 1] again. Note that if measures are uniform, it suffices to store 14, ([0 1)) as the symbolic representation of 14:
Our probabilistic abstract domain is the convex combination of the convex combination domains of this probabilistic EXACTLINE domain and the standard lifting of the box domain as a probabilistic abstract domain. In practice, it is convenient to store abstract element with p probabilistic polygonal chains and probabilistic boxes as
a= -[(((p()) (1)
14 ...... Mby ) ...... (P(P) (p) (4)
(1)
(p) .11 ................................ MR - p(.) )), ((0)) ....., ((9)), A)),
such that ΣL Dim1 Lj=1 11
Ei d Its concretization is then given as 1 (10, 1J)
v E nn (p("), / /w.. / P(.)) E macobrs) 
P
(a) Σ ways +
Xuy
#=1
( where wi Eド= My ((o, 1)). Our input always captures uniform distribution line segment.
Relaxation and heuristic Our deterministic relaxations can be extended to work in the probabilistic setting. When we replace a line segment by its bounding box, we use the total weight in its measure as the new entry in the weight vector À corresponding to the box. When we merge multiple boxes, their weights are added to give the weight for the the resulting box. We then use the same relaxation heuristic as we described previously also in the probabilistic setting.
Computing bounds Given probabilistic abstract element above, describing the output distribution of the neural network, we want to compute optimal bounds on the robustness probabilities P (u(Y) | E (a)). The part of the distribution tracked by the probabilistic

---

Under review as a conference paper at ICLR 2020
EXaCTLine domain has all its probability mass in perfectly determined locations, while the probability mass in each box can be located anywhere inside it. We can compute bounds
ul.u) (min P, max
(e+ (e+IzEL Xj, e+ Eyeu where E'= (Y), with (u) -nn ( 11 /u....,,...... (1) / P(.))
{i E (I......4) 7/ (b0)) 3 W) and
Rs
U == Li E (l...., m1(0)) ny + 03. Here, we used the deterministic box concretization 7/-
EVALUATION
We write APPROXLINE to denote our analysis (deterministic and probabilistic versions) where the relaxation heuristic uses relaxation percentage p and clustering parameter k. We implement APPROXLINE in the DiffAl framework, taking advantage of the GPU parallelization provided by PyTorch (Paszke et al., 2017). Additionally, we use our implementation of APPROXLINE to compute exact results without approximation. To get exact results, suffices to set the relaxation percentage p to 0, in which case the clustering parameter & can be ignored. Verification using A APPROXLINE,, is equivalent to EXACTLINE up to floating point error. To distinguish our GPU implementation from the original CPU implementation, we call our method EXACT instead of EXACTLINE. EXACT is additionally capable of doing exact probabilistic inference. We run on machine with GeForce GTX 1080 with 12 GB of GPU memory, and four processors with a total of 64 GB of RAM.
6.1 GENERATIVE SPECIFICATONS
For generative specifications, we use decoders from autoencoders with either or 64 latent dimensions trained in two different ways: VAE and CycleAE, described below. We train them to reconstruct CelebA with image sizes 64 x 64. We always use Adam Kingma & Ba (2014) with a learning rate of 0.0001 and a batch size of 100. The specific network architectures are described in Appendix Our decoder always has 74128 neurons and the attribute detector has 24676 neurons.
VAE, is variational autoencoder Kingma& & Welling, 2013) with latent dimensions.
CycleAE; is a repurposed CycleGAN (Zhu et al. 2017) with latent dimensions. While these were originally designed for unsupervised style transfer between two data distributions, P and Q. we use it to build an autoencoder such that the generator behaves like a GAN and the encodings are distributed evenly among the latent space. Specifically, embedding/latent space with a small feed forward network Dp as the latent space discriminator, The distribution the image distribution, and for its discriminator Di we use the BEGAN method (Berthelot et al. 2017), which determines an example's 's realism based on an autoencoder (also with / latent dimensions), which is trained to reproduce the ground-truth distribution Q and adaptively to fail to reproduce the GAN generator's 's' distribution.
normal distribution in I dimensions for the
Attribute Detector is trained to recognize the 40 attributes provided by CelebA. Specifically, the attribute detector has linear output. We consider the attribute i to be detected as present in the input image if and only if the i-th component of the output of the attribute detector is strictly greater than 0.5. The attribute detector is trained using Adam, minimizing the LI loss between either I and the attribute (if it present) or 0 and the attribute (if it absent). We train it for 300 epochs.
6.2 SPEED AND PRECISION RESULTS
Given a generative model capable of producing interpolations between inputs which remain on the data manifold, there are many different verification goals one might pursue: E.g., check whether the generative model is correct with respect to trusted classifier or whether classifier is robust to interpretable interpolations between data points generated from a trusted generative model. Even trusting neither the generator nor the classifier, we might want to verify that they are consistent.
We address all of these goals by efficiently computing the attribute consistency of a generative model with respect an attribute detector: For a point picked uniformly at random between the encodings e and e2 of two ground truth inputs with matching attributes, we would like to determine the probability that its decoding will have the same attribute We define the attribute consistency
Cinam (e1, e2, 1)
Pr (nA(nD((1 a)ei + oee)); > 0.5 < 1).
a-,(().))
7

---

Under review as a conference paper at ICLR 2020
Time(s) Per Specification
Prob Bound Width
60s
54.4
40s
36.53
1
0.89
0.8
26.06
0.5
20s
0.01
1.85 10
08
HZono
Sampling
EXACT
APPROXLINE
HZono
Sumpling
EXACT
APPROXLINE
(a)
(h)
Figure 2: A comparison of different methods that compute probabilistic bounds for C.
where is the ground truth for attribute We will frequently omit attribute detector n and decoder from C if it is clear from context which networks are being evaluated.
In this section, we demonstrate that probabilistic APPROXL.NE is precise and efficient enough to provide useful bounds the attribute consistency for interesting generative models and specifications on a reasonable dataset. To this end we compare APpROXLINE to a variety of other methods which also capable of providing probabilistic bounds. We do this for CycleAEgz trained for 200 epochs.
Specifically, suppose P a set of unordered pairs {a, b} from the data set with ag > 0.5 > bA. > 0.5 for each of the k attributes where a ground truth attribute labels of Using each method, we find bounds on the true value of average attribute consistency as Cn nt, ng) meang, DeP.e,, (ng (a), ng (b), aA. > 0.5) where is the encoding network. Each method finds probabilistic bound, [2, m/., such that 1 < Ć <
We call its width.
We compare probabilistic APPROXLINE against two other probabilistic abstract domains, EXACT (=APPROXLINEE). and HZono (Mirman et al. 2018) lifted probabilistically. Furthermore, also compare against sampling with binomial confidence intervals on using the ClopperPearson interval.
For probabilistic sampling, take samples and recalculate the ClopperPearson interval with confidence of 99.99% until the interval width below 0.002 (chosen to be the same as our best result with APPROXLINE). To avoid an incorrect calculation, we discard this interval and prior samples, and resample using the estimated number of samples. Importantly, the probabilistic bound returned by the abstract domains guaranteed be correct 100% of the time, while for sampling it is only guaranteed to be correct 99.99% of the time.
For all methods, we set timeout of 60s, and report the largest possible probabilistic bound if timeout or out-of-memory error occurs. For APPROXLINE if an out-of-memory error occurs, we refine the hyperparameters using schedule clock). Figure 2 shows the results of running these P 100 pairs of matching celebrities with matching attribute labels, chosen uniformly at random from CelebA (each method uses the same P).
Appendix C and restart (without resetting the timeout
The graph shows that while HZono is the fastest domain, it is unable to prove any specifications. Sampling and EXACT do not appear to be significantly slower than APPROXLINE, but it can be observed that the average width of the probabilistic bounds they produce is large. This is because Sampling frequently times out, and EXACT frequently exhausts GPU memory. On the other hand, OPROXXLINE provides average probabilistic bound width of less than 0.002 in under 30s with perfect confidence (compared with the lower confidence provided by sampling).
6.3
USE CASES FOR APPROXLINE
Here, demonstrate how an attribute detector. We do this for two possible generative specifications: (i) generating rotated heads using flipped images, and (ii) adding previously absent attributes faces. For the results in this section, we use schedule B described in Appendix
domain check the attribute consistency of model against
Comparing models with turning heads It is known that VAEs are capable of generating images with intermediate poses of the subject from flipped images of the subject. An example of this transformation is shown in Figure 3b Here, show how effectiveness different autoencoding models performing this task. To this, we trained all 4 architectures described above for 20 epochs. We then create line specification over the encodings
APPROXLINE to compare the
8

---

Under review as a conference paper at ICLR 2020
(a)
(b)
(c)
Figure 3: Examples of equally spaced interpolated images. The original images at the Oth and 10th positions, and their immediate neighbors are their respective reconstructions. (a) is between the same person with the attributes using CycleAEg2 trained for 200 epochs. (b) between horizontally flipped images using CycleA trained for 20 epochs. (c) is between an image and the addition of the "mustache" feature vector using CycleAE32 again.
Figure 4: Comparing the different models using probabilistic 20 to provide lower bounds for > (nn((a), ng (Flipped(a)), dA.i), where and Flipped(()) ()) are the images shown in Figure 3b) The width of the largest probabilistic bound was smaller than 3 x 10-6, so only the lower bounds are shown. Less than 50 seconds were necessary compute each bound, and the fastest computation was for CycleAEs1 at 30 seconds.
Lower Bound Correctness
0.9
0.85
0.8
VAEg2
VAΣsı
CycleAEşz CycleAEst
of the flipped images shown in Figure 3b For human face that is turned in one direction, ideally the different reconstructions will correspond to images of different orientations of the same face in 3D space. As none of the CelebA attributes correspond to pose, the attribute detector should recognize the same set of attributes for all interpolations. We used deterministic APPROXLINE 0.02 to demonstrate which attributes provably remain the correct for every possible interpolation (as visualized in Appendix E. While we are able to show in the worst case, 32 out of 40 attributes are entirely robust to flipping, some attributes are not robust across interpolation. Figure demonsttraes the results of using probabilistic ApproXLing LINE to find the average lower bound on the fraction of the input interpolation encodings which do result in the correct attribute appearing in the output image.
Verifying attribute independence Here, we demonstrate using APPROXLINE that attribute detection for one feature is invariant to a transformation in an independent feature. Specifically, verify for single image the effect of adding mustache. This transformation is shown in Figure To do this, we find the attribute vector m for "mustache" (i = 22 in CelebA) using the 80k training-set images in the manner described by Larsen al. (2015). , and compute probabilistic bounds for C, (ng(() (o) + 2m, OA.)) for j * 22 and the image o. Using APPROXI JINE we are able to prove that 30 out of the 40 attributes are entirely robust through the addition of mustache. Among the attributes which can be proven to be robust are i 4 for "bald" and i 39 for "young". We are able to find that the attribute i 24 for "NoBeard" is not entirely robust to the addition of the mustache vector. We find a lower bound on the robustness probability for that attribute of 0).85222 and an upper bound of 0.83528.
LINE
CONCLUSION
In this paper presented a highly scalable non-convex relaxation to verify neural network properties where inputs are restricted to a line segment. Our results show that our method is faster and more precise than previous methods for the same networks, including sampling. This speed and precision permitted us to verify properties based on interesting visual transformations induced by generative networks for the first time, including probabilistic properties.

---

Under review as a conference paper at ICLR 2020
REFERENCES
David Berthelot, Thomas Schumm, and Luke Metz. Began: Boundary equilibrium generative adversarial networks. arXiv preprint arXiv: 10717, 2017.
Samuel R Bowman, Luke Vilnis, Oriol Vinyals, Andrew M Dai, Rafal Jozefowicz, and Samy Bengio. Generating sentences from a continuous space. arXiv preprint arXiv: 2015.
Xiaoyu Cao and Neil Zhenqiang Gong. Mitigating evasion attacks deep neural networks via region-based classification. In Proceedings of the 33rd Annual Computer Security Applications Conference, pp. 278-287. ACM, 2017.
Charles Clopper and Egon S Pearson. The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika, 26(4):404 413, 1934.
Jeremy M Cohen, Elan Rosenfeld, and Zico Kolter. Certified adversarial robustness via randomized smoothing. arXiv preprint arXiv: 190Xiv1902.000 02918, 2019.
Patrick Cousot and Radhia Cousot. Abstract interpretation: unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Symposium on Principles of Programming Languages (POPL), 1977.
Patrick Cousot and Michael Monerau. Probabilistic abstract interpretation. In Helmut Seidl (ed.), Programming Languages and Systems, pp. 169-193, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. ISBN 978-3-642-288669-2
Laurent Dinh, Jascha Sohk-Dickstein, and Samy Bengio. Density estimation using real nvp. arXiv preprint arXiv: /tt5::/600.888000 2016.
Vincent Dumoulin and Francesco Visin. guide convolution arithmetic for deep learning. arXiv preprint 16X3v:6603.077 2016.
Vincent Dumoulin, Ishmael Belghazi, Ben Poole, Olivier Mastropictro, Alex Lamb, Martin Arjovsky, and Aaron Courville. Adversarially learned inference. arXiv preprint arXiv::606.00770 2016.
Krishnamurthy Dvijotham, Marta Garnelo, Alhussein Fawzi, and Pushmeet Kohli. Verification of deep probabilistic models. arXiv preprint arXiv: /8/2.02795, 2018a.
Krishnamurthy Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovic, Brendan O' O'Donoghue, Jonathan Uesato, and Pushmeet Kohli. Training verified learners with learned verifiers. arXiv preprint arXiv: 1805. 1026, 2018b.
Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A Mann, and Pushmeet Kohli. dual approach to scalable verification of deep networks. In UAI, pp. 550-559, 2018c.
Timon Gehr, Matthew Mirman, Petar Tsankov, Dana Drachsler Cohen, Martin Vechev, and Swarat Chaudhuri. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In Symposium on Security and Privacy (SP), 2018
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint 1rXiv:1810.122 12715, 2018.
David Ha and Douglas Eck. A neural representation of sketch drawings. arXiv:1704.088: 2017.
arXiv preprint
Zhenliang He, Wangmeng Zuo, Meina Kan, Shiguang Shan, and Xilin Chen. Attgan: Facial attribute editing by only changing what you want. IEEE Trunsactions on Image Processing, 2019.
Kyle D Julian, Mykel J Kochenderfer, and Michael P Owen. Deep neural network compression for aircraft collision avoidance systems. Journal of Guidance, Control, and Dynamics, 42(3):598-44 -088, 2018.
10

---

Under review as a conference paper at ICLR 2020
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, 2017.
Diederik P Kingma and Jimmy Ba. Adam: method for stochastic optimization. arXiv preprint orXiv:/412.000 2014.
Diederik P Kingma and Max Welling. Auto-encoding variational bayes. arXiv preprint arXiv:1312.6114 2013.
Anders Boesen Lindbo Larsen, Søren Kaae Sønderby, Hugo Larochelle, and Ole Winther. Autoencoding beyond pixels using a learned similarity metric. arXiv preprint arXiv: 2015.
Mathias Lecuyer, Vaggelis Atlidakis, Roxana Geambasu, Daniel Hsu, and Suman Jana. Certified robustness to adversarial examples with differential privacy, arXiv preprint 2018.
Bai Li, Changyou Chen, Wenlin Wang, and Lawrence Carin. Second-order adversarial attack and certifiable robustness. arXiv preprint arXiv:1809.03/13, 2018.
Chen Liu, Ryota Tomioka, and Volkan Cevher. On certifying non-uniform bound against adversarial attacks. arXiv preprint arXiv:1903.cmm 160.:0903306603, 2019.
Xuanqing Liu, Minhao Cheng, Huan Zhang, and Cho-Jui Hsich. Towards robust neural networks via random self-ensemble. In Proceedings of the European Conference Computer Vision (ECCV), pp. 369-385, 2018.
Yongyi Lu, Yu-W Yu-Wing Tai, and Chi-Keung Tang. Attribute-gun guided face generation using conditional cyclegan. In Proceedings of the European Conference on Computer Vision (ECCV), pp. 282-297, 2018.
Michael F Mathieu, Junbo Jake Zhao, Junbo Zhao, Aditya Ramesh, Pablo Sprechmann, and Yann LeCun. Disentangling factors of variation in deep representation using adversarial training. In 2016.
Advances in Neural Information Processing Systems, pp.
Lars Mescheder, Sebastian Nowozin, and Andreas Geiger. Adversarial variational bayes: Unifying variational autoencoders and generative adversarial networks. In Proceedings of the 34th International Conference on Machine Coarning-Volunee 70, pp. 2391-2400. JMLR. org, 2017.
Matthew Mirman, Timon Gchr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In International Conference on Machine Learning (ICML), 2018.
Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary Vito,, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in pytorch. 2017.
Alec Radford, Luke Metz, and Soumith Chintala. Unsupervised representation learning with deep convolutional generative adversarial networks, arXiv preprint arXiv:1511.06434, 2015.
Aditi Raghunathan, Jacob Steinhardt, and Perey Liang. Certified defenses against adversarial examples. arXiv preprint arXiv:1801.093322 2018.
Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robust verification of neural networks. arXiv preprint arXiv: 1902299722222 2019.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Plishell, and Martin Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems, pp. 10825-10836, 2018
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):41, 2019.
11

---

Under review as a conference paper at ICLR 2020
Matthew Sotoudeh and Aditya V Thakur. Computing linear restrictions of neural networks, arXiv preprint arXiv:1908.066 190.:19908.00,44, 2019.
Mukund Sundararajan, Ankur Taly, and Qiqi Yan. Axiomatic attribution for deep networks, In Proceedings of the 34th International Conference on Machine EeaarningVVolmme 70, pp. 3319-3328.
JMLR. org, 2017.
Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:/711.07356, 2017.
Aaron Van den Oord, Nal Kalchbrenner, Lasse Espcholt, Oriol Vinyals, Alex Graves, et al. Conditional image generation with pixelenn decoders. In Advances in neural information processing systems, pp. 4790-4798, 2016.
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, pp. 6367-6377, 2018.
Teu Weng, Pin- Yu Chen, Lam M Nguyen, Mark S Squillante, Ivan Oseledets, and Luca Daniel. Proven: Certifying robustness of neural networks with probabilistic approach. arXiv preprint arXiv:1812.08329, 2018.
Eric Wong, Frank Schmidt, Jan Hendrik Metzen, and J Zico Kolter. Scaling provable adversarial defenses. arXiv preprint arXiv: 1805. /805./2514,, 2018.
Jun-Yan Yan Zhu, Taesung Park, Phillip Isola, and Alexei A Efros. Unpaired image-to-image translation using cycle-consistent adversarial networks. Proceedings of the IEEE international conference on computer vision, pp. 2222-2222222 2017.
12

---

Under review as a conference paper at ICLR 2020
A APPROXLINE PROPOGATION PSEUDOCODE
Algorithm I: Pseudocode for the APPROXLINE class. Here only demonstrate propogation and not final computation of probabilities.
class ApproxLine ():
def --init_- (self, elements, probs) self elements = clements
self probs probs
def multiply -ddd_y-addddae return ApproxLine ([e. multiply_ add_relu merge () for in self elements () self, probs)
add_ relu www.rrreeeeeeeeeeeeeeeee
seege(self (self, matrix, bias):
Algorithm 2: Pseudocode for Interval propogation.
class Interval ():
def __init_- (self, a, b, center_radius False) if center_radiir center
= b
else:
self center = (b a) 2 = (b abs /
def aepplyy_dddrell_mmee
matrix, bias): center self. center multiply (matrix) bias radius gelf.radio multiply (matrix. ())()) return Interval radius, self prob)
def expandsself node):
max max_point = self center + self radius min-point self. center self radius
return Interval (self, minimum ( max point, node), maximum ( (max_poiin (max-point, node ))
13

---

Under review as a conference paper at ICLR 2020
Algorithm 3: Pseudocode for the ExactLine class. This is not how it is implemented in either our framework or by Sotoudeh Thakur (2019) but is useful for pedagogical purposes.
class ExactLine ():
def -_init__ (self, nodes, dists):
self nodes nodes self dists = dists ddssss( 1)
def multiply add relu merge ( matrix, bias):
new_nodes node matrix + bias for node in self nodes ]
ndw-dists self. dists
# compute ReLUs inneficiently per dimension (pedagogically)) for d in range new new_node [0]. dimensions):
nodes []
relu-dists = []
for in range (len new (nd_es 1):
curr node = new new -odes [n]
next node new nodes + 1]
curr_dist = new_dists [n] next_dist = new-dists [n + 1]
dist_to.curr next_dist curr_dist
relu.nodes += [ curr relu
if (curr nore_ [d] 0 and next next_node > 0)
or hourr_nodele [d] > and nexe [d] < 0):
www_disttto_curr
dist_to-curr min cunncuur.node [d]. next_ [d]). abs ()
(next
curr [d])
relu-nodes
relu nodes +=
[(next_node curr curr_node)) new diisttto.curreuurr..oo
relu_dists += [curr_dist + new relu relu_nodes += [next_node relu ()
relu_dists += [ext_dist]]
new nodes relu nodes new dists = relu dists
# now cluster and merge return ExactLine (Le. aultiply_add_rest () for in self elements ())) merge ()
14

---

Under review as a conference paper at ICLR 2020
Algorithm 4: Pedagogical pseudocode for merge (as part the ExactLine class) based on relaxation heuristic described in more detail in Section 5.1] This is not the most efficient possible implentation as done for our framework. becomes part of either an ExactLine an Interval, and counted twice.
important to ensure that every edge
def merge (self):
cluster_mapp heuristic (self) []
unclustered []
unclustered.probs for in range(len) (new .ow_e) 1):
if in cluster.map
cluster
cluster map clusters (clusterr map. indexes to clusters [i]]
cluster. interval expand (self _ (i]es(ii)
cluster interval expand (self. nodes + 1])
cluster-map probs [cluster_ map self dists [i + 1] self dists
+=
else:
unclustered unclustered.segmeent segments += [ExactLine (self.. modes[i], self nodes [i+1])] unclustered.prohs +=
self dists[itl] - self nodes[i]]
return ApproxLine cluster map clusters + unclustered ,cluster_man .mp. probs + unclustered probs)
15

---

Under review as a conference paper at ICLR 2020
B NETWORK ARCHITECTURES
For both models, we use the same encoders and decoders (even in the autoencoder descriminator from BEGAN); and always the attribute detectors. Here denote a convolution which produces C' channels, with a kernel width of W pixels and height of H, with stride of and padding of 1. FC is fully connected layer which outputs neurons. a s. x W x H is a transposed convolutional layer (Dumoulin & Visin 2016) with a kernel width and height of W and !! respectively and stride of and padding of I and out-padding of p. which produces C' output channels.
Conv, W H to
Latent Descriminator is fully connected feed forward network with 5 hidden layers each 100 dimensions.
Encoder is standard convolutional neural network:
I Conv 322v x x 3 + ReLU + Conv232 x 4 x - ReLU + Conv 64 x x 3
ReLU Conv 4 x 4 + ReLU FC 512 - ReLU + FC 512 -
Decoder is transposed convolutional network which has 74128 neurons:
FC 400 ReLU FC 2048 ReLU + Conv 22 16 x 3 3 + ReLU + Conv LanvT1,02 x 3 x +
Attribute Detector has 24676 neurons:
I 16 4 ReLU Conv232 4 ReLU + FC 100 + 40.
C APPROXLINE REFINEMENT SCHEDULE
While many refinement schemes start with an imprecise approximation and progressively tighten it, we observe that being only occasionally memory limited and rarely time limited, it conserves more time to start with the most precise approximation we have determined usually works, and progressively try less precise approximations as we determine that more precise ones can not fit into GPU memory. Thus, we start searching for a probabilistic robustness bound with APPROX and we run out of memory, try APProx IINE (1.5p.1) min...p)))))))
(3,.1) max (0.95.V.5 for schedule A, and APPROX max (0.95095
for schedule B. This procedure is repeated until a solution is found, or time has run out.
D EFFECT OF APPROXIMATION PARAMETERS ON SPEED AND PRECISION
Time
Prub Bound Width
20.
0.5
10s
Us
.8667
100
75
50
100
75
30
100
T5
30
100
75
50
100
75
50
100
75
50
100
TO.
50
100
75
50
(a)
Figure A comparison of speed (a) and Probabilistic Bound Widths (b) of APPROXLINE for different approximation hyperparameters, on CycleAEg4 trained for 200 epochs.
Here we demonstrate how modifying the approximation parameters, and N of APPROXLINE", effect its speed and precision. Figure [ shows the result of varying these x-axis. The bottom number, N is the number clusters that will be idcally made, and the top number is the percentage of nodes which are permitted to be clustered.
16

---

Under review as a conference paper at ICLR 2020
VAE32
CycleAE32
VAE61
CycleAEe1
Figure 6: Blue means that the interpolative specification visualized in Figure 3b has been deterministically and entirely verified for the attribute (horizontal) using 2PPROXLINE Red means that the attribute not be verified. In all cases, this is because the specification robust for the attribute. One can observe that the most successful autoencoder is CycleAEss-
E COMPARING THE DETERMINISTIC BINARY ROBUSTNESS OF DIFFERENT MODELS
Figure uses deterministic 2PPROXLIN to demonstrate which attributes provably remain the same and correct (in blue) for every possible interpolation.
17


Reviews:
[{"review_id": "rkgJpdFCKr", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper proposes APPROXLINE, which is a sound approximation to EXACTLINE and is able to compute tight deterministic bounds on probabilities efficiently when the input is restricted on a line. It is a nonconvex relaxation, therefore it is able to capture the nonconvexity of neural networks. APPROXLINE is applied to generative models to verify the consistency of image attributes through linear interpolations on the latent variables. \n\nTo me, the most significant part is that the proposed approach has the potential to become a reliable metric for evaluating whether a generator disentangles latent representations, as long as a reliable attribute classifier can be trained. I would suggest the authors to emphasize this part in their future versions.\n\nHowever, the current version is quite difficult for me to understand, and I guess it is difficult for a broad range of audiences without background in program analysis. Somehow I think the same message can be conveyed better without abusing terms from abstract interpretation. I would also suggest the authors to reduce such abuse of notations. At least, pseudocode could be provided. \n\nAs a result, I cannot give a confident judgement about whether the contribution of this paper is significant given the existence of EXACTLINE. Still, I tend to accept this paper for its potential to become a good metric for generative models. ", "extra_scores": {"experience_assessment": "I have published one or two papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I made a quick assessment of this paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I did not assess the derivations or theory."}, "extra_text": {}}, {"review_id": "rJen8KnatS", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "summary:\nThe paper proposes a method to efficiently verify that generative models are consistent with respect to some known (latent) attribute. The authors defines attribute consistency by 1) mapping pairs of input (x1, x2) with matching attribute to a latent space using an encoder n_E(x) and 2) measuring how correctly an auxiliary classifier will classify the known attribute using (decoded) linear interpolations between the two latent encodings. Importantly, the proposed method gives guaranteed bounds on this consistency score, as opposed to simply evaluating the classifier on a fixed set uniformly sampled points between x1 and x2. In experiments the authors use their method to test for attribute independence as well as consistency under left-right flipping of an image using two different autoencoder models (VAE and CycleAE) obtaining tighter bounds on the ‘attribute consistency’ score than competing methods.  \n\nDecision & supporting arguments:\nConceptually I found the paper very appealing, and it tackles an important problem in generative modelling. However I have some concerns with respect to the paper in its current state:\n1) It is not clear to me why the attribute consistency score, a key component in the paper, is a good measure of consistency in generative models. Notably, I miss motivation for why linear interpolations between encoded inputs should necessarily keep the attribute stable.\n2) Although I found the experiments interesting, I did not find the experimental section completely comprehensive. There is no discussion or experiments probing the dependency on the quality of the auxiliary classifier or the encoder/decoder model used. \n3) I did not find the description of the proposed method to be reasonably self-contained. Especially section 3 which describes the proposed method is challenging to follow. The background material in section 2 reads very much like a set of definitions. Since ICLR has a quite broad audience, I think the paper should be written in a more pedagogical way, with for instance clarifying examples. An example of a sentence that is incredibly hard to parse is on page 4, describing domain lifting: “Any deterministic abstract domain can be directly interpreted as a probabilistic abstract domain, where the concretization of an element is given as the set of probability measures whose support is a subset of the set produced by the deterministic concretization.” I think making this paper more pedagogical requires major rewriting.\n\nDue to the above reasons I currently score the paper as a ‘weak reject’.\n\nFurther detailed questions/comments:\nConsistency Score\nQ1: What is the motivation behind the definition of the consistency attribute score. Especially, why is an attribute considered consistent if it is stable to linear interpolations in the latent space? \n\nExperiment Results:\nQ2.1: Did you perform any experiments on how the L1 score of the auxiliary classifier affects the consistency score? I would also like to see some quantitative numbers on the auxiliary classifier.\nQ2.2: Why is the L1 score used for training the classifier instead of bernoulli which seems more natural for binary attributes?\nQ2.3: Similarly, I would like to see some numbers on the quality of the encoder/decodes. Simply inspecting the interpolations in figure 3) the reconstructions seem quite blurry, likely due to the relatively small models used. Is it prohibitively expensive to run the proposed method on bigger models (e.g. ResNet based encoder/decoders or Unet-style models)?\nQ2.4: I believe it would be more informative to show the actual confidence intervals in figure 2b) instead of only the width of the confidence intervals?\n\nReadability:\nQ3: I found it quite challenging to understand how the proposed is implemented in practice - My suggestion is that the authors add a pseudo-code / algorithm to section 3 clarifying exactly how the bounds reported in the experimental section are calculated. \n\n", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I did not assess the derivations or theory."}, "extra_text": {}}, {"review_id": "H1xHn7EwKH", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Summary\n\nThis work aims to provide warranties on the outputs of generative models by providing bounds on robustness (over adversarial attacks for instance, or other transformation in this case). The specific case of restricting the inputs to a line segment allows performing verification of robustness exactly (Exact-line approach, NeurIPS'19). The authors extend this work and apply it to verify robustness of some VAE and BEGAN like models.\n\nPositive aspects:\n- Rigorous work, I did not spot much typos. \n- First proofs given for generative models.\n\nNegative aspects:\n\nMy main concern about this work is that the presentation is not didactic enough. \n- From the beginning, key concepts are not clearly defined, such as network certification, specification, and the \"verification problem\". In the definition of robustness, a reference to a \"safe set of outputs\", as in Gehr et al. would help the understanding.\n- The introduction is too short and lacks context. Figure 1 is not referred in the text and is not understandable with notations that are not yet introduced. \n- Then follows without transition two pages of background that are mostly definitions but without a proper motivation, these are difficult to process.\n- The work, an extension of the Exact-line approach, only gives a 5 lines description which is not insufficient to understand the approach. \n\nPerhaps my assessment is too negative because I am unfamiliar with the certification literature, but since the work present applications in generative modeling, I think it should be understandable by readers from this background as well.         \nMinor:\nof of in caption of Fig 2\nlast line of page 5: J -> j\nI found the equivalence sign in the last equation of page 6 confusing, is it really supposed to be an equivalence here? \nPage 6 : attribute detector... described below -> in appendix\n\nAfter seeing the authors changes in the manuscript the paper does look better, but similarly to Reviewer 2 I still judge it difficult to understand. ", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The goal of verification of properties of generative models is very interesting and the contributions of this work seem to make some progress in this context. However, the current state of the paper (particularly, its presentation) makes it difficult to recommend its acceptance.
Decision: Reject