Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 4: Ok but not good enough - rejection
review_content: This paper focuses on the floating point unsoundness of neural network verification procedures, and shows that the results from such verifiers can not be trusted. To drive home the message of the paper, the authors take MIPVerify (which doesn't ensure FP soundness) and shows that they are able to construct adversarial examples for the cases that are returned as verified by MIPVerify. 

It is an interesting nice paper but the contribution is weakened by two  facts: One, it is already known that MIPVerify doesn't ensure FP soundness; which is also acknowledged by its authors. Second, when FP soundness is not ensured, and given the fact that adversarial examples are widely present, it is no surprise that one could find adversarial examples. 

So I am split on the paper. From a formal methods perspective, the discovery of the paper is not surprising as Floating point computations are known to be important (this is one of the reasons that SMT solvers put a lot of emphasis on FP). But perhaps from ML practitioner, it may be interesting. 
review_title: Interesting Paper but lacks sufficient contribution

final_score: rating: 4: Ok but not good enough - rejection
review_content: Summary:
The authors develop a method to generate pairs of sample that are separated by a small adversarial perturbation, that have different class, but with the specificity that the a complete verifier would returns a result indicating that this sample admits no adversarial perturbation (despite the fact that it does, as evidenced by the second element of the pair). 
These samples are obtained by considering a brightness perturbation of the image and finding the parameter (alpha) at which the verifier switch from returning "safe" to "unsafe". The resulting perturbed image is going to have adversarial examples very close to the boundary of the region considered, so small floating point errors might result in returning incorrect results.

Main thoughts:
The problem that the author discuss is very well highlighted and explained. It is clear what vulnerability they identified, as well as the mechanism that they use to highlight it. 
On the other hand, in terms of importance, I would rank it more as an interesting observation that an actual critical problem. If we assume, that what I'm caring is robustness of my image classification system for perturbation of size epsilon=0.1, then it seems that the worst that can happen is that some samples that I verified to be robust for epsilon=0.1, are in practice only robust for epsilon=0.09999? This doesn't seem overtly critical and would result in essentially the same result in any application.

Questions:
- The choice of what solver to use as a backend for a MIP formulation of the Neural Network verification problem is an implementation detail. MIPVerify could well be implemented with a different solver? (MIP solvers returning incorrect result due to floating point errors is not a new problem and there seems to be some literature in how to adress these problems if they are considered of importance "Safe bounds in linear and mixed-integer linear programming, Neumaier & Shcherbina")
In addition, could this problem be solved by simply adjusting the tolerance parameters of the solver? I did not see any discussion of this by the authors, but I imagine that the default parameters used by the verifier might be geared more towards speed than towards perfect accuracy.
- The authors mention verifiers that incorporate proper handling of floating point errors (ERAN) but then reject it by saying that it rely on specific implementation details of the inference algorithm. This seems strange because that's exactly the recommendation that the authors make. Page 2: "any sound verifier for this class of networks must reason about the specific floating point error characteristics of the neural network implementation at hand."

Minor questions:
In Figure 1.a, it seems like for the first 4 graphs, the dotted lines which I assume implies what the difference should be are lines with slope 1. Why would the change in the logit vector vary at the same rate as the perturbations? Shouldn't there be a slope dependent on the corresponding gradient coefficient?
review_title: Good presentation but problem of limited impact.

final_score: rating: 8: Top 50% of accepted papers, clear accept
review_content: The paper presents a method to find adversarial inputs for neural networks in regions where the networks can be "proven" not to admit any such adversarial examples, practically demonstrating the unsoundness of a "complete verifier" as well as an "incomplete verifier".
While it was already obvious to me that "verifiers" that assume floating-point arithmetic is the same as real arithmetic are unsound, the paper is a service to the community in that it also makes this very obvious to informed outsiders who may not have already questioned the validity of robustness verification research that does not model round-off and even ignores it in its own implementation. The related work section does a good job of surveying the state of the art as it relates to floating-point soundness. The authors also took some space to discuss how their findings relate to current and future research on robustness verification, which I think is important in this case.

Perhaps there could be a short discussion of challenges that different approaches face to become sound with respect to floating-point semantics. (For example, it seems particularly challenging for approaches based on duality, as the correctness of certificates depends non-trivially on closed-form solutions to optimization problems as well as associativity of addition.)

The technical sections are mostly well-written, though I was not able to figure out some details. For example, it is not so clear how precisely binary search is used to find α and δ simultaneously. Section 4.2 is a bit dense and its presentation could probably be improved.


"inevitable presence of numerical error in [...] the verifier".
It is not inevitable that the verifier is subject to "error". We could encode the precise floating-point semantics of the neural network as a SAT formula (and then watch the SAT solver time out, but this does give a sound and complete method).

review_title: A service to the community

final_score: rating: 3: Clear rejection
review_content: In the recent literature there has been a rise in the number of papers which attempt to verify neural networks. The specification of the verification problems often gets adapted according to the application in mind. More specifically, for image classification networks, the problem is to prove that the output of the neural network does not flip for small perturbations to the pixel values. For a robotic setting, the problem is often safety and convergence to some goal state. Where the neural network operates in closed loop with the system dynamics. 

The authors in this paper present an adversarial attack model on neural networks, which is deemed correct by some verifier. More specifically , given a neural network which can be shown to be robust to adversarial perturbations around some input, the authors exploit numerical errors in the computations to attack the network. Demonstrating the presence of loop holes in the proving engines itself. This is due to the approximation errors introduced by using floating point numbers.

In my opinion, the notion of input sets in the space of images, is not a very useful one. Mainly because the interval valued sets representing  perturbations of the input image, is far removed from the intended specification.  It's a step in the right direction, if the verification of computer vision task was a well defined problem. Since it's not clear what to verify in the first place, the use case of this paper  is not a very convincing one in my opinion. The problem of verifying neural networks in a robotic setting has a more meaningful specification.  Hence, i don't think that this paper in itself will be interesting to the general theme of the conference. 
review_title: Verification of neural networks for computer vision tasks is not well defined. Hence, analyzing attack models on the verification engines is not well grounded.

Meta-review: There are many recent methods for the formal verification of neural networks. However, most of these methods do not soundly model the floating-point representation of real numbers. This paper shows that this unsoundness can be exploited to construct adversarial examples for supposedly verified networks. The takeaway is that future approaches to neural network verification should take into account floating-point semantics.

This was a borderline paper. On the other hand, to anyone well-versed in formal methods, it is not surprising that unsound verification leaves the door open for exploits. Also, there is prior work (Singh et al., NeurIPS 2018) on verification of neural networks that explicitly aims for soundness w.r.t. floating-point arithmetic. On the other hand, it is true that many adversarial learning researchers do not appreciate the value of this kind of soundness. In the end, the decision came down to the significance of the result. Here I have to side with Reviewer 1: the impact of this problem is limited in the first place, and also, the issue of floating-point soundness has come up in prior work on neural network verification. For these reasons, the paper cannot be accepted this time around.
Decision: Reject