Venue: ICLR 2020 Conference

Reviews:

final_score: rating: 6: Weak Accept
review_content: This paper proves the universal approximation property of interval-certified ReLU networks. Such a network achieves the best certified accuracy against l_infty adversaries at large epsilons on MNIST and CIFAR10, but the certified accuracy is still far from satisfaction. With the results from this paper, we can at least make sure the interval-certified ReLU networks is able to fit the robust classifier with arbitrarily small error if it exists. 

I did not check the details of the proofs, but I think such a theorem is a great reference for future work. 

However, we cannot conclude whether a network with a moderate size exists to fit the robust classifier well from this paper. From the construction of local bumps (nmin), the number of neurons needed to represent a bump function grows exponentially with the input dimension, which makes the size of the network vacuously large when the input is images. We are not getting any closer to improving the certified robustness with this paper.
review_title: Official Blind Review #1

final_score: rating: 8: Accept
review_content: Summary: 
This paper proves a theoretical result, that for every continuous function f, there exists a ReLU network approximating f well, and for which interval propagation will result in tight bounds.

The proof is by construction: the function to approximate is decomposed into a sum of functions (slices) with bounded range, which will be approximable to the correct precision. Each slices is approximated as a sum of local bumps, who essentially approximates an indicator function over a grid.

Comments:
* Equation (1) of Theorem 1.1, I assume that the left inclusion could be replaced by [l, u], given that interval propagation generate valid bounds? Or is the case that due to the approximating network being only an approximation, interval propagation on it might not give actual bounds on the real function?

Opinion:
The paper is very technical and takes some effort to parse to understand the construction, but the authors do a good job of providing examples and illustrations to make it at least intuitive. The content is clearly novel and the result is far from trivial.

The only thing that i'm slightly wary is the significance of what is proven. The paper shows that approximating a continuous function with a network such that bound propagation works well on it is feasible.
On the other hand, the motivation given is "given a dataset and a specification, is there a network that is both certified and accurate with respect to these", which is a slightly different problem. If this was proven to be yes, then we would know that when our robust training fails, this is due to optimization not being good enough or our not network not having enough capacity. The result proven here does not suffice, because it pre-suppose the existence of a correct function, that would match the dataset and specification, which is not guaranteed (see for example the proofs that robustness and accuracy are at odds, or you can just imagine verification of robustness for too-large radius which would lead to infeasible specification). I still like the paper and I think it might just be a matter of framing the abstract and introduction.

Do the authors have an implementation, even for only toy-size examples, of the generation of a Neural Network approximating a given function or is this purely theoretical? Especially when the proof is constructive like this, this can strengthen the confidence that no subtle mistakes have been made. If so, this should be mentioned.

Potential typos:
Page 4: "Further" -> "Furthermore"?
Page 5: "Increasing the fines" -> "Increasing the finesse?"
Page 6, just before Lemma 4.3, missing a mathcal before the N?

Disclaimer:
I carefully checked the derivations in the paper but only assessed the sensibility of the proofs in the appendix.

review_title: Official Blind Review #2

final_score: rating: 3: Weak Reject
review_content: The paper aims to show that there exist neural networks that can be certified by interval bound propagation. It claims to do this by showing that for any function f, there is a neural network g (close to f) such that interval bound propagation on g obtains bounds that are almost as good as one would get by applying interval bound propagation to f.

There are a couple issues with this paper. The first is that the main theorem does not imply the claimed high-level take-away in the paper in any practically relevant regime. This is because while the paper does show that there is a network that approximates f well enough, the size of the network in the construction is exponential (for instance, one of the neural network components in the construction involves summing over all hyperrectangles lying within a grid). The result is only plausibly practically relevant if there is a polynomially-sized network for which the bound propagation works.

The second issue is the comparison to related work, which omits both several key techniques in the literature and two related papers on universal approximation.

On universal approximation papers, see these two: https://arxiv.org/abs/1904.04861 and https://arxiv.org/abs/1811.05381. They consider a different proof strategy but more plausibly yield networks of reasonable size.

On key techniques in the literature: "typically by employing methods based on mixed integerlinear programming, SMT solvers and bound propagation" ignores several major techniques in the field: convex relaxations (SDP + LP), and randomized smoothing. Similarly, "specific training methods have beenrecently developed which aim to produce networks that are certifiably robust" again ignores entire families of techniques; Raghunathan et al. train SDP relaxations to perform well, while Cohen et al. train randomized smoothing to work well. Importantly, randomized smoothing is not about creating an over-approximation of the network but explicitly constructs networks that are smooth.

"some of the best results achieved on the popular MNIST (LeCun et al., 1998) and CIFAR10(Krizhevsky, 2009) datasets have been obtained with the simple Interval approximation (Gowalet al., 2018; Mirman et al., 2019)"
-Is this actually true? I just looked at Mirman et al. and it doesn't seem to explicitly compare to any existing bounds. My impression is that randomized smoothing (Cohen et al.) currently gets the best numbers, if we're allowed to train the network. If not allowed to train the network, Raghunathan et al. (Neurips 2018) performs well and is not compared to in the Mirman paper.

These omissions must be addressed as the introduction and related work is misleading in its current state.

Finally, some writing issues:
>>> While the evidence suggests "no", we prove that for realisticdatasets and specifications, such a network does exist and its certification can beestablished by propagating lower and upper bounds of each neuron through thenetwork

One cannot "prove" something for "realistic datasets", since "realistic datasets" is not a formal assumption. Please fix this.

>>> "the most relaxed yet computationally efficient convex relaxation"

What does most relaxed mean? Most relaxed would most straightforwardly mean outputting the entire space as the set of possibilities at each point, which is clearly not intended.
review_title: Official Blind Review #3

Meta-review: This work shows that there exist neural networks that can be certified by interval bound propagation. It provides interesting and surprising theoretical insights, although analysis requires the networks to be impractically large and hence does not directly yield practical advances. 
Decision: Accept (Poster)