Venue: ICLR 2018 conference

Reviews:

final_score: rating: 5: Marginally below acceptance threshold
review_content: Summary:

This paper:
- provides a compehensive review of existing techniques for verifying properties of neural networks
- introduces a simple branch-and-bound approach
- provides fairly extensive experimental comparison of their method and 3 others (Reluplex, Planet, MIP) on 2 existing benchmarks and a new synthetic one

Relevance: Although there isn't any learning going on, the paper is relevant to the conference.

Clarity: Writing is excellent, the content is well presented and the paper is enjoyable read.

Soundness: As far as I can tell, the work is sound.

Novelty: This is in my opinion the weakest point of the paper. There isn't really much novelty in the work. The branch&bound method is fairly standard, two benchmarks were already existing and the third one is synthetic with weights that are not even trained (so not clear how relevant it is). The main novel result is the experimental comparison, which does indeed show some surprising results (like the fact that BaB works so well).

Significance: There is some value in the experimental results, and it's great to see you were able to find bugs in existing methods. Unfortunately, there isn't much insight to be gained from them. I couldn't see any emerging trend/useful recommendations (like "if your problem looks like X, then use algorithm B"). This is unfortunately often the case when dealing with combinatorial search/optimization. 
review_title: review

final_score: rating: 6: Marginally above acceptance threshold
review_content: The paper studies methods for verifying neural nets through their piecewise
linear structure. The authors survey different methods from the literature,
propose a novel one, and evaluate them on a set of benchmarks.

A major drawback of the evaluation of the different approaches is that
everything was used with its default parameters. It is very unlikely that these
defaults are optimal across the different benchmarks. To get a better impression
of what approaches perform well, their parameters should be tuned to the
particular benchmark. This may significantly change the conclusions drawn from
the experiments.

Figures 4-7 are hard to interpret and do not convey a clear message. There is no
clear trend in many of them and a lot of noise. It may be better to relate the
structure of the network to other measures of the hardness of a problem, e.g.
the phase transition. Again parameter tuning would potentially change all of
these figures significantly, as would e.g. a change in hardware. Given the kind
of general trend the authors seem to want to show here, I feel that a more
theoretic measure of problem hardness would be more appropriate here.

The authors say of the proposed TwinStream dataset that it "may not be
representative of real use-cases". It seems odd to propose something that is
entirely artificial.

The description of the empirical setup could be more detailed. Are the
properties that are being verified different properties, or the same property on
different networks?

The tables look ugly. It seems that the header "data set" should be "approach"
or something similar.

In summary, I feel that while there are some issues with the paper, it presents
interesting results and can be accepted.
review_title: Interesting study with some flaws

final_score: rating: 3: Clear rejection
review_content: The paper compares some recently proposed method for validation of properties
of piece-wise linear neural networks and claims to propose a novel method for
the same. Unfortunately, the proposed "branch and bound method" does not explain
how to implement the "bound" part ("compute lower bound") -- and has been used 
several times in the same application, incl.:

Ruediger Ehlers. Planet. https://github.com/progirep/planet,
Chih-Hong Cheng, Georg Nuhrenberg, and Harald Ruess.  Maximum resilience of artificial neural networks. Automated Technology for Verification and Analysis
Alessio Lomuscio and Lalit Maganti.  An approach to reachability analysis for feed-forward relu neural networks. arXiv:1706.07351

Specifically, the authors say: "In our experiments, we use the result of 
minimising the variable corresponding to the output of the network, subject 
to the constraints of the linear approximation introduced by Ehlers (2017a)"
which sounds a bit like using linear programming relaxations, which is what
the approaches using branch and bound cited above use. If that is the case,
the paper does not have any original contribution. If that is not the case,
the authors may have some contribution to make, but have not made it in this
paper, as it does not explain the lower bound computation other than the one
based on LPs.

Generally, I find a jarring mis-fit between the motivation (deep learning
for driving, presumably involving millions or billions of parameters) and
the actual reach of the methods proposed (hundreds of parameters).
This reach is NOT inherent in integer programming, per se. Modern solvers
routinely solve instances with tens of millions of non-zeros in the constraint
matrix, but require a strong relaxation. The authors may hence consider
improving the LP relaxation, noting that the big-M constraint are notorious
for producing weak relaxations.
review_title: no original contribution

Meta-review: All three reviewers are in agreement that this paper is not ready for ICLR in its current state. Given the pros/cons, the committee feels the paper is not ready for acceptance in its current form.
Decision: Reject