Venue: ICLR 2020 Conference

Reviews:

final_score: rating: 6: Weak Accept
review_content: 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. 

To 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.

However, 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. 

As 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. 
review_title: Official Blind Review #1

final_score: rating: 3: Weak Reject
review_content: summary:
The 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.  

Decision & supporting arguments:
Conceptually 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:
1) 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.
2) 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. 
3) 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.

Due to the above reasons I currently score the paper as a ‘weak reject’.

Further detailed questions/comments:
Consistency Score
Q1: 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? 

Experiment Results:
Q2.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.
Q2.2: Why is the L1 score used for training the classifier instead of bernoulli which seems more natural for binary attributes?
Q2.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)?
Q2.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?

Readability:
Q3: 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. 


review_title: Official Blind Review #2

final_score: rating: 3: Weak Reject
review_content: Summary

This 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.

Positive aspects:
- Rigorous work, I did not spot much typos. 
- First proofs given for generative models.

Negative aspects:

My main concern about this work is that the presentation is not didactic enough. 
- 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.
- 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. 
- Then follows without transition two pages of background that are mostly definitions but without a proper motivation, these are difficult to process.
- The work, an extension of the Exact-line approach, only gives a 5 lines description which is not insufficient to understand the approach. 

Perhaps 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.         
Minor:
of of in caption of Fig 2
last line of page 5: J -> j
I found the equivalence sign in the last equation of page 6 confusing, is it really supposed to be an equivalence here? 
Page 6 : attribute detector... described below -> in appendix

After seeing the authors changes in the manuscript the paper does look better, but similarly to Reviewer 2 I still judge it difficult to understand. 
review_title: Official Blind Review #3

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