Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 6: Marginally above acceptance threshold
review_content: The authors show that certain complete neural network verifiers can be mislead by carefully crafted neural networks that exploit round-off errors, which when large magnitude values overwhelm low magnitude values. Such a construction can be obfuscated by taking advantage of the compounding effect when there are many layers of the network. This can also be used to add backdoors to existing networks, albeit in a way that looks quite artificial.

I definitely agree with the authors that is important to draw attention to edge cases where complete verifiers can fail given that "completeness" can lead to a false sense of security.  For that alone, I think this paper merits attention, even if 'numerical errors can mess up neural networks' is a well-known fact. 

That being said, I think there are a few significant drawbacks to this work.

(1) Presentation of the paper. The paper at times feels like more of a discussion than a detailed exploration of a certain attack type. As an example of why this is not optimal, it makes it difficult to figure out at a glance what each table is referring to. Also, it obfuscates the experimental results, of which there are quite a few in the paper. I believe the paper can benefit from a more formal style with paragraph headings and subsections breaking up the text, and the conclusions clearly highlighted as opposed to being spread throughout the text.

(2) Flipping the answer from 'yes' to 'no' for a binary function requires a small perturbation near the decision boundaries, so the fact that numerical computations can lead to wrong answers in and of itself is not surprising. What would be much more interesting is the _degree_ to which such attacks can shift a continuous function. I believe that the method is this work leads to arbitrarily large differences, but I think this is something that should be explicitly explored.
review_title: Shows that complete neural network verifiers can be fooled by backdoors that exploit numerical errors

final_score: rating: 7: Good paper, accept
review_content: The paper shows that it is possible to fool exact verifiers using numerical instabilities. It proposes network architectures that can exploit numerical issues in order to get certificates from verifiers based on architecture such as MIPverifiy and that can at the same time accepts adversarial examples within the certificated epsilon-ball using a simple trigger. 
This raises important security issues and as the author suggest, I do believe that such problem car arise in many situations. 

The problem is first put into light on a very simple architecture and then on more complex ones and then with a added backdoor on existing network. Sereval optimizer for the verifiers are compared and behave similarly. A defence to this behavior is proposed, making all network parameters slightly noisy. 
While I'm convinced on the importance of the subject and I understand that it is probably mainly for illustration purposes, I have some questions mainly on the backdoor concept:
* how can it be invisible to the verifier in section 5 (here I understand the only the original architecture and weights are provided to MIPVerify?) and detected in section 6 ? I miss a point there.
* about the defence, I wish there were more experimental results with different epsilon values, to have a better intuition on the global behavior of the defence. I also think there could be more details on how the verifier detects the backdoor, as mentioned in previous point. 
review_title: An important issue about numerical instabilities for network security

final_score: rating: 6: Marginally above acceptance threshold
review_content: This paper argues that, although existing complete neural network verifiers can provide some guarantees on the robustness, these verifiers have overlooked potential numerical roundoff errors in the verification, and in such cases the provided guarantees may be invalid. To show such a phenomenon, the authors propose to construct “adversarial neural networks” that can cause the complete verifier to produce imprecise results in floating point arithmetics and can thereby fool the verifier. They also showed it is possible to insert a backdoor to the network such that the backdoor is missed by the verifier while it can trigger some behavior desired by the attacker. Although this paper has also discussed a possible defense, I find the corresponding section not very clearly written.

Pros:
* This paper raises an interesting problem in complete verifiers about potential numerical errors. This can be important to ensure the robustness of complete verifiers against some potential adversarial networks or backdoors.
* The authors demonstrated the existence of the numerical error problem via constructing adversarial networks to fool complete verifiers.

Cons:
* The structure of adversarial networks or inserted backdoors is not made to match some actual neural network architectures. E.g., in Figure 2, the network has a series of linear layers but has no activation between, and thus it does not look like an actual NN structure. Is it possible to construct adversarial networks on realistic architectures, e.g., MLP or CNN with ReLU activations? 
* Although defending against adversarial networks has been discussed in the paper, the writing appears inconsistent and unclear. (See additional comments below.)

Additional comments:
* I find Sec. 6 is probably not very consistently and clearly written. In the beginning, it is said that adversarial networks are sensitive to weight perturbations (“The key insight is that some of the parameters of our adversarial network are rather sensitive to noise whereas non-adversarial networks are naturally robust to a very small perturbation of their parameters”), and later it is said that “the network with the backdoor appears to be robust to noise”. This looks confusing to me. Can you elaborate more whether you think the adversarial network is or is not robust to small noise? And the later paragraphs look difficult to understand. 

==========================================================================================

Updates after rebuttal:

Thanks to the authors for the reply. I have read the author response and understand that actually there are activations in the networks but just omitted from the figures. I am increasing my recommendation to 6.
review_title: An important problem for complete verifiers but it may need studies on realistic NN structures 

final_score: rating: 6: Marginally above acceptance threshold
review_content: The paper presents a method to create neural networks that, due to floating-point error, lead to wrong robustness certifications on most input images by a so-called "complete verifier" for neural network robustness. The authors show how to make their networks look a bit less suspicious and they discuss a way to detect neural networks that have been manipulated in the way they suggest.

To me, it was obvious a priori that any "complete verifier" for neural network robustness that treats floating-point arithmetic as a perfect representation of real arithmetic is unsound.
However, I think works like the current one are important to publish such as to practically demonstrate the limitations of the "guarantees" given by certain robustness certification systems and to motivate further research. Therefore, I expect the target audience of the paper to be informed outsiders who have not so far questioned the validity of robustness certification research that did not explicitly address floating-point semantics. In light of this, the paper has several weaknesses related to presentation:
- Terminology is often used in a confusing way. For example, the approach that is practically demonstrated to be unsound is called a "complete verifier" with the "strongest guarantees", wrongly implying that all other verifiers must be at least as unsound.
- The related work is incomplete. For example, unsoundness due to floating-point-error has been previously practically observed in Reluplex: https://arxiv.org/pdf/1804.10829.pdf (in this case, it produced wrong adversarial examples, without any special measures having been taken to fool the verifier).
- The related work is not properly discussed in relation to floating-point semantics. Some of the cited works are sound with respect to round-off, others are not. I would expect this to be the central theme of the related work section such as to properly inform the reader if and why certain approaches should be expected to be unsound with respect to round-off. The current wording that "all the verifiers that work with a model of the network are potentially vulnerable" is not fair to all authors of such systems; some have taken great care to ensure they properly capture round-off semantics.
- I did not find obfuscation and defense particularly well-motivated. What is the practical scenario in which they would become necessary?
- The paper sends a somewhat strange message: it (exclusively) suggests to combat floating-point unsoundness by employing heuristics to make it harder to find actual counterexamples. What about just employing verifiers with honest error bounds that explicitly take into account floating-point semantics? It may not be possible in the near-term to actually make correct "complete verifiers", but at least authors of incomplete verifiers will not have to succumb to pressure to make an unsound "complete" version in order to match precision, performance and/or "guarantees" of their competitors.

The technical sections are written well enough to be understandable, and the main technical contribution is a pattern of neurons we can insert into a neural network in order to make it behave in an arbitrary way that is invisible to the considered verifier. This is interesting and disproves any claim of "completeness", but scenarios where this would be a way to attack a system seem a bit contrived. Ideally, there would be an approach that can exploit round-off within a non-manipulated verified neural network to arbitrarily change the classification of a given input without changing the network. The paper might benefit from a discussion of this possibility and an explanation why it was not attempted.

---
The new section 2.4 is appreciated, though it seems the paper still does not say that incomplete methods can deal with round-off error by sound overapproximation.
review_title: Interesting paper with a somewhat flawed presentation

Meta-review: The authors demonstrate that complete neural network verification methods that use limited precision arithmetic can fail to detect the possibility of attacks that exploit numerical roundoff errors. They develop techniques to insert a backdoor into networks enabling such exploitation, that remains undetected by neural network verifiers and a simple defence against this particular backdoor insertion. 

The paper demonstrates an important and often ignored shortcoming of neural network verification methods, getting around which remains a significant challenge. Particularly in adversarial situations, this is a significant risk and needs to be studied carefully in further work.

All reviewers were in agreement on acceptance and concerns raised were adequately addressed in the rebuttal phase, hence I recommend acceptance. However, a few clarifications raised by the official reviewers and public comments should be addressed in the final revision:
1) Acknowledging that incomplete verification methods that rely on sound overapproximation do not suffer from this shortcoming.
2) Concerns around reproducibility of MIPVerify related experiments brought up in public comments.
Decision: Accept (Poster)