Provably Bounding Neural Network Preimages

Summary

This paper presents a novel approach to bounding the preimages of neural networks using a sequence of relaxations. Results are provided for a toy controls problem and a robustness verification task.

Strengths

1. The paper addresses an important recent developement in the literature. 2. The paper is well presented and motivated. I like the direct correspondence between the visualization in Figure 1 and the derivation of the method in Section 3. 3. The proposed approach is novel and has some promising results for toy problems. I believe all the steps in the derivation of the approach are correct, although I have not checked them carefully.

Weaknesses

1. My main concern is that the main experiment that the approach is evaluated on (reachability analysis) is very small (12 + 7 + 2 neurons), even by verification standards. It is true that these optimization-problem flavored verification approaches are generally evaluated on small networks, ab-CROWN for example can be evaluated for substantially larger networks on datasets like CIFAR-10. Given that these approaches incur exponential runtime with network size, I am skeptical that they can ever be relevant for networks of a practical size. 2. Similarly, many proposed details scale poorly with input data dimension (as mentioned in the limitations). I believe that the number of sampled c would need to grow exponentially with input dimension, as would the branch-and-bound scheme. 3. I recommend the authors tone down their presentation somewhat. In 2.2, it should be claimed that only an approximation of the convex hull is computed (not the exact convex hull). Also referring to the controls problem as an "established benchmark" is somewhat of a stretch as this is a recent unpublished preprint with only a couple citations.

Questions

1. I am not sure why the controls benchmark task is referred to as a "robot moving on the floor of a room." This is a double integrator task, as described in the cited work that originally presented the problem. Of course this can be considered a planar system with strange dynamics, but it's not clear why that would be done when the dynamics have a classic double integrator structure. 2. I'm confused on the discrepancy between the reported results for the baseline method. Specifically, the approximation ratio of ReBreach is about 4000, which is orders of magnitude higher than what I would expect based on the results in the original paper (errors less than 10x the true volume). What is causing this discrepancy? 3. In Figure 3, on the left side without input splitting, why is the convex hull so loose? I would expect it to tightly wrap around the green circles.

Rating

7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.

Confidence

3: You are fairly confident in your assessment. It is possible that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.

Soundness

3 good

Presentation

4 excellent

Contribution

2 fair

Limitations

The main limitations are mentioned explicitly.

Summary

The authors propose INVPROP, an algorithm for constructing certified bounds on the pre-image of neural networks with ReLU activations. The method constructs a convex over-approximation of the pre-image by implicitly optimizing the dual relaxation of a MILP problem. Empirical evaluation shows considerable improvement over the state of the art.

Strengths

The authors' method is elegant and clear. Furthermore, I can see how it could be used as the baseline for many future works. Inverting neural networks is a notoriously difficult problem, and I commend the authors for proposing a workable solution.

Weaknesses

The paper is dense to read at times, and the connection to existing works is often left to the reader. More specifically, most of the related work is presented at the end of the paper (Section 6). The state-of-the-art methods in neural network inversion (Rober 2022, Everett 2022) are mentioned for the first time in lines 249 and 256. Furthermore, no mention of earlier works in neural network inversion (see examples below) leave the reader with the feeling that this is a new problem that was never studied before: Kindermann, Linden, 1990, "Inversion of neural networks by gradient descent" Saad, Wunsch, 2007, "Neural network explanation using inversion" I think the authors' contribution would shine even more if they introduced a little more historical perspective on the topic. While reading the paper, I found a few minor writing issues, which I list below. For more detailed algorithmic question, see the "questions" and "limitations" secvtions of this review. Many unnumbered equations make referencing difficult. See for instance lines 89, 144 and 166 in the main paper, lines 525-526 in Appendix E. Lines 50-53. This contribution is difficult to parse without a strong understanding of ab-CROWN and local robustness problems. Robustness verification is presented in Section 5. Given the structure of the paper, I believe it should be in Section 4.3. Line 314, "forumalation" should be "formulation". Appendix E, the output domain weights H and d are not present in the proof, which I guess it is for clarity, but the authors do not acknowledge this. Appendix E, in lines 525-526 there is an extra term \sum c^ix^i in the objective that is not explained. The formatting of figures and tables in Section 4 is ugly. At least, all tables and figures in page 8 should be flushed to the top, in order to avoid having a piece of main text in between them.

Questions

Line 77. Why is inverting a neural network an intractable problem? It is clearly possible to compute it, albeit expensive to do so. In the end, f is a Lipschitz-continuous function, thus locally invertible. After line 89, why is the first matrix not the identity? Surely the robot cannot teleport on the x_1 dimension. Also, why can the policy only control diagonal movement along the line [0.5, 1]? If these numbers are chosen just for illustration purpose, then why presenting the "robot in a 2d environment" story altogether? How are the concrete bounds [l,u] computed? Algorithm 1 says "cheap bound propagation", but these are only applicable for the forward verification problem. how to compute them for a general problem? At Line 166, the proposed bounds yield a parallelogram domain around ReLU(x), whose shape is regulated by z. Why not using the classic, traingular domain from DeepPoly? What are the advantages of your parallelogram domain here?

Rating

7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

3 good

Presentation

3 good

Contribution

3 good

Limitations

The authors are not up-front on the fact that c in Equation (1) is extracted at random. The problem of how to do so is finally discussed in Sections 4 and 7. However, it is not clear how the choice of c impact the tightness of the pre-image. More specifically, in line 247, sampling 40 random planes may be ok for this particular 2-dimensional problem. Similarly, I can see how this works well for the OOD task in Section 4.2. At the same time, it is unclear how well that works for the MNIST task in Section 5. The authors offer no comment about this therein.

Summary

The paper considers verified neural network inversion. Given a set of output values, the goal is to compute the pre-image of these, i.e., the inputs that lie within this output set (given as a linear constraint over the output space). To address this, the authors propose INVPROP, an algorithm that computes an over-approximation of the convex hull of the pre-image. This set is represented as the intersection of multiple half-space constraints. Given a direction vector finding the corresponding half-space constraint can be phrased as an optimization problem. Formulating this as a mixed-integer linear program (MILP) allows to recover a tight convex hull (assuming enough direction vectors are used). To improve efficiency at the cost of tightness this MILP can be relaxed into a LP. This is similar to the same problem in standard forward verification, however, in contrast to there, a constructive closed-form solution to the LP is not available. Inspired by the CROWN verification algorithm the authors propose to consider the dual of the LP. This formulation allows to obtain a lower bound of the LP and thus a over-approximation to the convex hull. This approach, termed INVPROP, now can be solved by traversing the neural network back-to-front and obtaining neuron bounds via gradient ascent. As in forward verification, this can be tightened by branching the problem and obtaining bounds for sub-problems. INVPROP is evaluated: on backward-reachability for neural control policies, out-of-distribution detection, and robustness verification (combined with a forward verification algorithm), where it achieves strong results.

Strengths

- Creative and Novel Approach - The mathematical results appear sound and well motivated - Good empirical results, though -- other than the improvements in certified robustness -- on niche benchmarks and settings - Well connected with related and prior work

Weaknesses

- While overall quite easy to read/follow, the presentation appears a bit sloppy and rushed - There is no discussion of the limitations and scalability of the approach, other than the mention of per-neuron branching - While the evaluation highlights why the approach is useful, it does not provide a good understanding of the limitations of the approach, i.e. the first two tasks are rather low-dimensional and the verification task is only discussed very briefly See the below questions for more details and addressable points.

Questions

- What is $z$ in (2a)? Is it a typo and not needed for the optimization problem? - Line 267 refers to Figure 4 which is just found in the appendix. Even with the Figure the description in line 267/268 is not clear to me. Can you clarify the setting in the OOD approach? - Can you discuss the scalability of the approach? What are the key limiting factors? How large is the role of the input dimensionality? Ideally, this is also shown through further experiments, but I understand that this is hard within the constraints of the rebuttal. EDIT POST REBUTTAL: My questions have been answered, thereby addressing the above weaknesses. I have thus updated my score.

Rating

7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

4 excellent

Presentation

2 fair

Contribution

3 good

Limitations

There is some discussion of limitations though it is not very clear to me what the key limiting factors, e.g. on the scalability of the approach are. (See questions.) Societal impact is discussed in a manner appropriate to the paper.

Summary

The paper considers the problem of computing approximations of the set of inputs for which a given neural network satisfies certain output constraints. To solve the problem, the paper discusses adaptations of a number of approaches from standard neural network verification, including MILP and LP formulations, and motivates the development of bound propagation methods and optimisations of the Lagrangian duals. Experimental results of the resulting method are reported on (i) backward reachability analysis for neural feedback loops; (ii) OOD Detection; (iii) robustness verification.

Strengths

The problem studied is well motivated and its applicability is sufficiently exemplified. The adaptation of the α,β-Crown method to solve the problem is novel. The efficacy of the resulting method is evaluated on a range of benchmarks, where it is shown to outperform the state-of-the-art in backward reachability analysis. The connection of backward propagation to standard forward verification is brilliant to see, especially its utilisation towards more efficient forward verification.

Weaknesses

The contribution is incremental to the α,β-Crown method. At its present stage the method is limited to low-dimensional networks. Also, no scalability is discussed with respect to big (but still low-dimensional) networks. An important feature of the α,β-Crown framework on which the method is based, namely node branching, is not discussed but left as future work, thereby giving a "preliminary" feel to the paper.

Questions

Could you please discuss the overhead of the incorporation of the output constraint to forward verification when larger, i.e., with millions of ReLU nodes, networks are considered?

Rating

7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

3 good

Presentation

3 good

Contribution

3 good

Limitations

Adequately addressed.

Reply

I thank the authors for their response. The rebuttal indeed addresses most of my concerns and I'm particularly delighted by the scope of the additional experiments. I currently do not have further questions and have updated my score in the light of the new results and explanations.

Thank you for the response

Thank you for the detailed response which addresses the minor concerns of my review. I have thus increased my score from 6 to 7.