Venue: NeurIPS 2022 Conference

Reviews:

final_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.
review_content: summary: The paper proposes an approach for neural network verification that combines zonotopes and Lagrangian decomposition. This is done by considering zonotope domains in each subproblem of the Lagrangian decomposition. The paper shows that solving these subproblems under zonotope domains is NP-hard (unlike box domains), and thus proposes a technique to relax the domain to a more tractable set by partitioning coordinates. In particular, it considers 2-dimensional zonotopes which are shown to have good properties in terms of tractability. An extended version merges partitions together, using MIP to solve the problem. Both are shown to produce good bounds at a reasonable time frame compared to other verification approaches.
strengths_and_weaknesses: Neural network verification is a widely studied area and the need for better algorithms is still important, as current relaxations do not scale well to the very large networks used in practice. This paper is a solid step towards that direction, combining two approaches in verification that were previously distinct, zonotope-based bounding and Lagrangian decomposition.

The paper starts off with the simple idea of using zonotope domains in the subproblems of Lagrangian decomposition, and winds up systematically producing interesting results and methods: it proves that these subproblems become NP-hard, finds a more tractable relaxation to solve the subproblems, and shows how to incorporate box bounds in the process. Although these results lean to the incremental side, I consider all of these to be valuable contributions to the area, and as far as I am aware I believe that these contributions are novel. Furthermore, the paper is overall well-written, but there are a few minor details that could be included in the main text here and there (see "Questions" section).

While there is an overhead in considering zonotopes in Lagrangian decomposition, the computational results show that it can push the bound significantly compared to other incomplete verification algorithms. That said, one issue is that it is difficult to know whether this approach is worth it end-to-end as it does not compare with approaches tuned for similar solve times, but it could be viewed as a reasonable middle ground between cheap and expensive methods. Moreover, even if it is not immediately clear as to what situations one might prefer this approach, I can imagine future papers building on this idea as one can consider tighter domains within Lagrangian decomposition.

Overall, while this work is incremental, it executes well in combining the two ideas from the literature, and I do not see any major concerns. Therefore, I recommend acceptance.
questions: Minor details to be addressed:

* The definition of the notation $\sigma$ (the ReLU operator) is missing.
* Please include $z_B$ in (3a) in the minimization terms for clarity.
* In line 284, BDD+ is referred to before it is defined in Section 6; add at least a citation and if possible a sentence explaining what it is (as in Section 6).
* In the initialization phase, it is not clear what the "very minor improvements to DeepZ" are (at least not without looking at the reference). Could you clarify this in the text?
* The main text only specifies the number of neurons for each network (e.g. MNIST-Deep). Given how dependent on depth verification methods are, at least include number of layers, and layer types if possible.
* Typos: "Lagangian" in line 30, "perfrom" in line 326, "bouds" in line 346, "slighctly" in line 359.
limitations: Appendix B carefully describes the limitations of the work in many ways, which is very much appreciated. I see no other limitations that need to be mentioned.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: The paper aims at verify outputs of neural networks for a given input range. Based on a branch-and-bound strategy, the paper develops an approach to approximating bounds by solving a verification problem of 2-layer neural networks, which is a subproblem obtained by a branching procedure that performs Lagrange decomposition of an entire verification problem. A key idea of the approach is to use zonotopes, which are expressive and easy to handle computationally.  The experiments demonstrate the usefulness of the proposed approach.  The paper also conducted experiments to demonstrate the usefulness of the approach.
strengths_and_weaknesses: ### Strength
- The interesting use of zonotopes for neural network verification.
- The complexity for the computation with zonotopes are provable given.

### Weakness
The presentation is hard to follow.  Specifically, I can't find the following in the paper.
- It is not clear for me how to ensure correctness of the bounds provided by the proposed approach.
- It is not clear how to read the figures and tables in the paper.  Thus, I can't check the claims in the paper is correct.
- It is not clear whether the bounds the paper provides are tighter than those provided by the approach in [25] theoretically or experimentally.  If the latter, where is a formal claim and proof for it?
- Why is Proposition 4.2 important?  In L160, the paper says "The second proposition describes an improved pushforward operator that offers improvements against DeepZ", but I'm not sure why Z' in the proposition is an improvement.

The following is minor.
- What is \sigma in (1c)?
- Why is Wk, not Wk+1, used in (3c)?
- What does "the most negative" mean in L252?

### Post-Response
Some of my concerns were addressed by the author response, so my score raised from 4 (borderline reject) to 6 (weak accept).
questions: Can the concerns and questions described as the weaknesses be addressed?
limitations: Limitations seem to be addressed adequately.
review_title: null

final_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.
review_content: summary: The paper proposes a solution to the problem of neural network verification based on dual Lagrangian optimization. The main insight here is bounding the range of dual variables using Zonotopes to capture inter-neuron dependencies not considered by prior work. However, using Zonotopes for Lagrangian optimization makes the optimization harder. To address this issue, the authors design new algorithms to evaluate the dual function efficiently. 
strengths_and_weaknesses: Strengths:
+ Neural network verification is a highly relevant problem for the NeurIPS audience. There have been several papers on the topic in recent years at NeurIPS.

+ The writing is rigorous yet understandable. The authors do a great job of presenting their technical ideas at the right level of abstraction.

+ The high-level idea of combining Zonotope analysis with dual Langrangian optimization for NN verification is novel and interesting. However, leveraging this insight to develop a scalable and precise verifier requires tackling several technical challenges. The authors develop solid algorithms to overcome these issues.

Weaknesses:
+ For neural network verifiers, the ultimate metric that matters are the number of verification instances verified. The results in Table 4 show that the method cannot outperform the state-of-the-art. Therefore the usefulness of the proposed approach is unclear.
questions: * In terms of theoretical precision, how does the proposed approach compare with other incomplete verifiers such as PRIMA/beta-crown (when not run in complete mode). Are they incomparable? If yes, then it will be good to investigate other cases where the proposed approach gets better results than these baselines.

* The statement "unlike PRIMA, ZD can directly be plugged into branching frameworks." is not true as the recent work of https://openreview.net/forum?id=l_amHf1oaK uses PRIMA based constraints for branch and bounds.

*  Have you experimented with higher dimensional Zonotopes (e.g., 3 or 4)? or it becomes not feasible beyond the 2D setting? if not, is it possible to maybe compute some sort of approximation (as PRIMA does for k-ReLU) in higher dimension to reduce the cost but still gaining precision?

* In Fig. 5, why not change also the scale factor of the Box informed Zonotope as done in [23]? Does it interfere with the convergence of your method?

* For handling the sigmoid activations, can a MILP approximation (as proposed in https://openreview.net/pdf?id=LQtlOn64EK6Y) be employed to convert the optimization defined over sigmoid functions to ReLU ones?

* "All prior dual approaches have chosen the sets $z_k$ to be axis-aligned hyperboxes" however $\beta$-CROWN is also dual based (as mentioned on line 370) and does not rely on hyperboxes?

limitations: The authors mention the limitations of their method. The paper does not make any contributions that can have a potential negative societal impact.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: The paper considers the ReLU-based neural network verification problem, where
it builds on the Lagrangian relaxation of the corresponding optimisation
problem by approximating intermediate layer bounds with zonotopes, which can be
partitioned when evaluating the dual with ReLU constraints. The approach is
experimentally evaluated and compared with the SoA on a number of networks
trained on the MNIST and CIFAR-10 datasets.

strengths_and_weaknesses: Strengths

- The method provides balances the strengths and weaknesses of fast but
  imprecise incomplete neural network verification  and exact but slow complete
  verification (for verification purposes this is useful in practice as the
  method can be used after methods with less precision have failed and before
  exact methods are used).

- It so does by connecting Lagrangian decomposition with zonotope-based neural
  network verification in a novel manner.

- The exposition of this is well written and presented.

- Good experimental evaluation.

Weaknesses

- Whilst the efficacy of the method relies on accounting of neuron interactions
  in the dual evaluation, it is not compared with semidefinite programming
  approaches that also account for these interactions.

questions: Please see comment on Weaknesses.
limitations: These are sufficiently addressed.
review_title: null

final_score: rating: 4: Borderline reject: Technically solid paper where reasons to reject, e.g., limited evaluation, outweigh reasons to accept, e.g., good evaluation. Please use sparingly.
review_content: summary: The authors present a novel algorithm to compute bounds on the values of neural network activations. 
Bounding algorithms heavily rely on bounds on the network intermediate activations, which are represented as hyper-boxes and neglect interactions across the neurons in the same layer.
Leveraging a modified version of a Lagrangian decomposition from the literature, the authors devise a technique to take zonotope constraints into account in the dual optimization, tightening the resulting bounds yet paying a price in terms of computational efficiency.
strengths_and_weaknesses: **Strengths.**
This is the first paper that employs zonotope domains for intermediate bounds in the context of neural network verification: the idea is definitely novel and interesting, and the authors provide non-trivial solutions to the technical problems associated to the formulation.

**Weaknesses.**
The paper has two major weaknesses: one experimental, the other related to the presentation.
The experiments fail to show that "ZonoDual outperforms the state-of-the-art baselines of the linear programming relaxation and the tightest dual verification methods, in terms of both the tightness of the bounds and runtime.". First of all, the trade-offs of a bounding algorithm need to be assessed within complete verification, which allows to evaluate the tightness of the bounds against their time and memory cost in a fair manner. In Table 4, Beta-CROWN attains significantly tighter bounds in less time than ZD, hinting at disadvantageous speed-accuracy trade-offs.
Furthermore, I am not convinced by the incomplete verification experiments. The authors fail to specify which intermediate bounds are employed for the baselines: I would assume bounds from the Kolter and Wong work, as in [9] and [25]. As shown by the authors, these bounds are necessarily looser than the zonotope domains (yet significantly cheaper to compute), so I believe this is not a fair comparison. Indeed, ZD is typically run for longer than some of the baselines, and zonotope intermediate domains are not guaranteed to be tighter than hyperboxes computed via CROWN or alpha-CROWN (or slope-optimized LiRPA). The authors should take this into account.

Finally, I think the quality of the presentation would be improved if the authors focused less on the supposed dichotomy between primal and dual bounding algorithms (many dual algorithms are formulated from primal relaxations, such as [9] and [25], which they can potentially solve due to strong duality), and more on the fact that they propose to employ zonotope-based intermediate bounds, as opposed to hyper-boxes.


LiRPA: https://arxiv.org/pdf/2002.12920.pdf
Alpha-CROWN: https://openreview.net/pdf?id=nVZtXBI6LNn
questions: - As commonly done in the related literature, the authors should evaluate their algorithm within BaB to test whether it still pays off for complete verification. 

- Run stronger incomplete verification baselines (e.g., alpha-CROWN on both intermediate bounds and output bounds, both via joint and sequential (yet parallel) optimization).

I believe the paper is potentially of great interest to the community, and could greatly benefit from addressing the questions above.
limitations: Except those associated to the questions outlined above, the authors adequately address the limitations of their work.
review_title: null

Meta-review: metareview: The authors develop a novel approach for verifying input-output properties of neural networks like adversarial robustness, combining the advantages of earlier work on abstract interpretation and Lagrangian decomposition. 

The reviewers agree that the paper presents a novel, sound and significant contribution to the literature on NN verification. One reviewer had concerns regarding whether the approach actually shows substantial benefits when used as part of a complete verifier in terms of the number of verified instances, but agreed that this is likely problem dependent and does not take away the significance of the work. Another reviewer raised more serious concerns that the author should address in the final version of the paper. In particular:
1) Fairness of comparing against baselines with weaker intermediate bounds: The authors should revise the paper stating that the baselines they compare against depend on the quality of the intermediate bounds and the SOTA versions of these methods use tighter intermediate bounds than the ones used by the authors.
2) Highlight the issues with tightness of verification vs speed of verification tradeoffs in the context of complete verification (ie branch and bound), and discuss how the authors' approach might compare with approaches like alpha-beta CROWN.
confidence: Certain
Decision: Accept