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 considers developing a sound and complete verification method for robustness certification of polynomial networks (PNs) against norm-based perturbations. The verifier developed here combines input splitting with $\alpha$-convexification. The main algorithmic contribution is in computing this convexification which involves interval bound propagation (IBP) to bound the lower bounding hessian $L_H$ of the PNs and employing a standard power method to compute the $\alpha$ on the $L_H$. Comparisons against Gurobi and IBP show that the proposed method can enable more precise and scalable verification. 
strengths_and_weaknesses: Strengths:

+ The problem considered here is novel and well-motivated. There is not much work on the certification of polynomial networks which have also been shown to be vulnerable to adversarial attacks. 

+ While $\alpha$-convexification and IBP are known techniques in the literature, their combination has not been applied for NN verification before to the best of my knowledge. Further, the proposed framework is general and can be extended to other neural network architectures with twice differentiable activation functions.

+ While there are some issues with the writing that I point out later, I enjoyed reading the paper overall. It is well-organized and relatively easy to follow. 


Weakness:

- Since the primary operation in PNs is multiplication, I am not sure why the authors cannot compare with other methods in the literature (e.g., https://dl.acm.org/doi/abs/10.1145/3453483.3454056, https://openreview.net/forum?id=BJxwPJHFwS) that can handle multiplication more precisely than IBP. In my opinion, IBP is a very weak verifier for networks that are not trained to be easy to verify. Adding comparisons against these baselines will make the evaluation more compelling. Note I am not so concerned about the size of the networks/datasets. In many real-world applications, the small NNs are trained on datasets with much smaller dimensionality than STL10 (e.g., see security classifiers here: https://arxiv.org/abs/2105.11363, or the ones in Bio https://ieeexplore.ieee.org/abstract/document/9680252), therefore even though your verifier does not scale to large Vision/NLP datasets yet, there is still some practical value to your work. In fact, I also encourage the authors to consider these domains for their method in the future to enable more real-world impact of their work instead of focusing only on vision/NLP models which are often limited to academic/industrial competition and still not widely employed in the safety-critical settings due to their brittleness.
questions: * On line 119, $\lambda_{min}$ is undefined (I assume its minimum eigenvalue). In eq. (5) how is $z_i$ related to $z$ (I assume these are components of z)? What is $\mathcal{U}(A)$ in (13)? 

* In Section 3.3, how is the initial vector $v_0$ chosen? Does the initialization affect the speed of the method? Do you always converge or using a value before convergence can still lead to sound verification? 

* The input splitting strategy used by your algorithm appears suboptimal. There are better strategies available in the literature that can improve the results of your method (e.g., Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis, AAAI 2020). Any particular reason why you chose the suboptimal strategy?

* How difficult it is to compute the lower bound of the eigenvalue of the Hessian with relational analysis such as DeepZ/Fast-Lin or DeepPoly/CROWN?

* For ReLU-based networks, do you need to use Clark jacobians for your method to work as done in https://dl.acm.org/doi/abs/10.1145/3498718, or non-differentiability at x=0 does not affect your method? If it does not, then why?

* "We take advantage of the low-rank decomposition characterizing PNs to efficiently perform a power method over the lower bounding Hessian." so your method works for only PNs with this property? If yes, then an extension to regular NN with Sigmoid/Tanh activation may not be possible?
limitations: The authors adequately addressed the limitations of their method in Section 6. The proposed work has no potential negative societal impact.
review_title: null

final_score: rating: 5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.
review_content: summary: This paper is a direct application of complete formal verification  against robustness applied to polynomial networks. They propose a new efficient computation of the Hessian bound in order to guarantees property wit the BaB method (a recent MILP verification method). They applied their method to 3 datasets, MNIST, CIFAR10 and STL10 for 1 model and different noise level +  comparison with IBP for multiple PN models on MNIST.
strengths_and_weaknesses: Strengths:
Novelty of the approach: complete verification of DNN specific family 
Important topic
Sound proof of the Hessian bounds
Clarity of the paper
Very fast verification

Weaknesses
Poor experiments comparison: Not comparison with SAT based method, no comparison with other  BaB methods. I understand it is not PN based verification but still important (https://arxiv.org/abs/2005.03597 and https://arxiv.org/abs/2103.06624). For example evry verification paper gives the resultas for 0.3 MNST and 2/255 for cfar10 
Poor verifiable accuracy results compared to results above.
Poor explications of why PN is an interesting family to explore (compared to BNN for example) in term of theory or application (NLP - graphNN - image generation...)



questions: Explicit the last point of weakness (Poor explications of why PN is an interesting family to explore (compared to BNN for example) in term of theory or application (NLP - graphNN - image generation...)) can improve my opinion on the paper.
But I think the verifiable accuracy is too low compared to state of the art.
However, if there is a clear proof of PN model application for industry then  
limitations: cf. last point on question.
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: This work introduces a method to prove robustness of polynomial networks against $l^\infty$ perturbations. The method relies upon finding multivariate polynomials of degree 2 called $f_\alpha$ lower bounding the differences in the classification score $g(z) = f(z)_t - f(z)_a$. The lower binding function $f_\alpha$ relies on the parameter $\alpha$ which is estimated via a combination of branch and bound and interval arithmetic. Crucially, the approach relies on the twice differentiable structure of polynomial networks and the combination with branch and bound over the input make the method complete. The approach is evaluated on MNIST, CIFAR10 and STL10 and compared against standard of the shelf solvers (Gurobi) as well as interval arithmetic. The code was provided together with the submission. 
strengths_and_weaknesses: Verifying new architectures is a challenging, interesting and important field of research. Polynomial networks show strong performance along a range of tasks, justifying the authors interest. The paper is mostly well written and the notation is clearly explained. Further, the Limitations are stated clearly in the section for this purpose. The might also be applicable to ReLU networks, as the authors state. Input refinement based approach to make sound verification complete where also considered earlier (see https://arxiv.org/pdf/1804.10829.pdf, https://arxiv.org/abs/1809.08098), the authors may want to have a look. 

The approach does not seem to scale to large models or challenging datasets, which is also clearly stated by the authors. However, it would have been interesting, so see some larger (more accurate) models if feasible for CIFAR10 and STL10 in order to increase the number of correct classified inputs. Further, the hardware (GPU) is not specified. A comparison to other complete & non complete methods (evaluated on other networks) would have given an indication how polynomial networks with this certification compares to say standard ReLU convolutional networks performing the same task. Some details of the approach remained unclear, an explicit example illustrating the method would have been helpful. 

## After the rebuttal:
The authors clarified all my questions and provided in the general response an informative comparison, solidifying their evaluation. I think that this paper presents new and useful ideas for the field. I recommend acceptance. 
questions: - Have the authors considered the possibility to split the sum in Eq. 5, thus maybe enabling different $\alpha$ to increase precision of the approach? Would this be possible? If yes, how would the runtime complexity change? 
- In Eq. 13: how is A defined?
- In Eq. 15: usually for the power method, the sequence is defined by $v_k = \tfrac{M v_{k-1}}{\| M v_{k-1} \|}$. Is there a specific reason to have $M$ twice as in Eq. 15? 
- The power method numerical, thus has an approximation error. Is this approximation error handled soundly for the later analysis? Similarly, in Line 127-129, for PGD also there is a numerical approximation issue. 
- Do I assume correctly that the method is not floating point sound? (I think this is not central but I am curious anyhow)
- Can more complex networks used for CIFAR10 and STL10 that offer higher precision?
- Please speculate: Can and if how can you use your certification method to train the polynomial network? 
- Could the input splitting technique be improved by i.e. weighting the interval distance in each dimension by the diagonal entry of the hessian? (i.e. weighting by the second derivatives of the dimension in question?)
- in Line 110: are the sets really disjoint? Wouldn’t the interval [1,3] be spliced in [1,2] and [2,3] having non-empty intersection?
limitations: The limitations are appropriately addressed.
review_title: null

Meta-review: metareview: The authors propose a novel verification technique for polynomial neural networks. They compare their approach against competitive baselines and demonstrates improvements in the quality of bounds obtained and their ability to verify input-output properties.

The reviewers agreed that the paper contains novel and interesting ideas and all concerns brought up by the reviewers were thoroughly addressed in the rebuttal phase.

Hence, I recommend acceptance.
confidence: Certain
Decision: Accept