Expressivity of ReLU-Networks under Convex Relaxations

We thank the reviewer for their high-quality review and the interesting questions they raised. We are happy to hear that they find our approach novel and research question both important and interesting. Below we address their remaining questions.

Q1: Can you discuss the relevance of your results in the heavily restricted univariate domain? What are the implications of your negative results for the $\Delta$-relaxation in the multivariate setting?

First, we want to clarify that the $\Delta$-relaxation is strictly more precise than the DeepPoly and IBP relaxations. Thus, our negative result for the $\Delta$-relaxation in the multivariate setting directly implies negative results for the other, less precise relaxations (DeepPoly-0, DeepPoly-1, and IBP), even for extremely simple functions. We believe this result to be of great importance as the majority of neural network verifiers are upper bounded in their analysis precision by the so-called “convex relaxation barrier”, realized by the $\Delta$-relaxation [1]. Only a few, very recent methods use multi-neuron-relaxations (at great computational cost) to break this barrier [2,3]. This highlights that even extremely simple functions can not be encoded as ReLU networks such that these simpler verifiers can analyze them precisely and agrees well with the fact that the latter methods have recently dominated the international neural network verification competition [4].

However, as even simple multivariate functions can not be encoded such that their analysis is precise using any single neuron domain $D$ ($D$ is IBP, DeepPoly-0, DeepPoly-1 or $\Delta$), we can not separate them with respect to their expressivity in this setting. To do so and investigate if the more complex domains improve expressivity, we study the univariate case, and indeed show positive results and separation between methods, both in terms of expressivity and size of resulting solution spaces.

Q2: Why do you not discuss multi-neuron relaxations in the multi-variate setting?
We agree with the reviewer that this is an interesting question and have given it some thought, but remain unable to prove either a positive or negative result. We note that the first (to the best of our knowledge) constructive proof by He et al (2020) [9] showing that arbitrary CPWL functions can be encoded by (finite) ReLU networks was only published recently, highlighting the difficulty of this question even in the non-robust setting. Unfortunately, a multi-neuron analysis of the networks constructed in this proof is not precise, thus an altogether different construction would be required which would be out of scope for this already dense work. To show a negative result with our technique, we would require a network simplification strategy (and counterexample) for multi-neuron relaxations. However, simple functions with one non-linearity (such as the max function) can be analyzed precisely using multi-neuron relaxations and more complex functions/subnetworks with two or more non-linearities can not generally be simplified to fewer layers, necessitating a completely different approach. Thus we believe this to be out of the scope of this work.

Further, to provide some context to the contributions made in this work, we want to again highlight that prior work [6] considered only a single relaxation method (the simple IBP), while we consider four relaxations, the univariate and multivariate setting, and four function classes.

References:
[1] Salman, et al. "A convex relaxation barrier to tight robustness verification of neural networks." NeurIPS 2019
[2] Ferrari et al. "Complete verification via multi-neuron relaxation guided branch-and-bound." ICLR 2022
[3] Zhang et al. "General cutting planes for bound-propagation-based neural network verification." NeurIPS 2022
[4] Müller et al. "The third international verification of neural networks competition (VNN-COMP 2022): summary and results." arXiv 2022
[6] Mirman et al. “The fundamental limits of neural networks for interval certified robustness”, TMLR 2022
[7] Baader et al. “Universal approximation with certified networks”, ICLR 2020
[8] Wang et al. “Interval universal approximation for neural networks”, POPL 2022
[9] He, et al. "ReLU deep neural networks and linear finite elements." JCM 2020
[10] Müller et al. "Certified training: Small boxes are all you need."ICLR 2023
[11] Mao et al. "Connecting Certified and Adversarial Training." NeurIPS 2023
[12] De Palma et al. "Expressive Losses for Verified Robustness via Convex Combinations." arXiv 2023

We thank the reviewer for their review, high-quality summary, and great outline of the strengths of our paper. However, we have identified some misconceptions and factual errors in the listed weaknesses which we address below while answering the remaining questions.

Q1: Can you discuss why you focus exclusively on ReLU networks instead of considering sigmoid or tanh activations?
We decided to focus on ReLU networks for two key reasons. Firstly, they are much more widespread and thus relevant in the certified robustness community, e.g., the international verification of neural networks competition last year considered ReLU activations in all 12/12 benchmark classes, sigmoids in only one, and tanh in none at all [1]. Secondly, finite sigmoid and tanh networks can not exactly encode (to the best of our knowledge) any commonly used function class, making the question of exact analysis less relevant and interesting. Given the limited space and already “dense and mathematical” writing of our work, we decided to focus on the most relevant class of networks.

Q2: You seem to only consider fully connected feedforward networks. Can you discuss the extensibility of your results to other architectures?
We already consider arbitrary ReLU networks with any architecture including arbitrary skip connections, which include both CNNs and ResNets (see the first paragraph in Section 2 and Theorem 17). We have made this more clear.

Q3: Why do you only consider deterministic neural networks and not stochastic networks?
As our work is motivated by (deterministic) neural network verification (where all state-of-the-art methods are based on convex relaxations), we focus on the general type of network typically considered in the field, i.e., deterministic networks. In particular, we are not aware of any such method considering stochastic networks. Perhaps the reviewer can point to a specific class of stochastic networks that would be relevant in this setting.

Q4: You only seem to study standardized datasets and perturbation sets. Can you discuss to what extent your results generalize beyond that?
As we do not study any specific data(set) anywhere in the paper but argue about general function classes, our results will generalize to any applicable dataset. For univariate functions, we show a positive result for the general case of continuous bounded perturbation sets, subsuming all $\ell_p$-norm bounded perturbations, typically studied in the field. In the multivariate case, we show a negative result even for the more restrictive (but very commonly used) $\ell_\infty$-norm bounded perturbations. That is, even extremely simple functions can not be expressed for box input regions. This entails that these functions can also not be expressed for more general classes of perturbation sets. We note that Theorem 19 and thus 20 can be trivially extended to other $\ell_p$-norms and have added a corresponding Theorem (Thm. 24) to Appendix A.

Q5: While hypotheses are provided for certified training, no experiments are conducted to validate the conjectured benefits.
First, we want to highlight that our general results agree well with multiple recent empirical works as discussed in “Implications of our Results for Certified Training” (Section 1). While validating our conjecture of more precise relaxations being beneficial for certified training is an interesting item for future work, it is beyond the scope of this theoretical work, as no current certified training method supports more precise relaxations, as current approaches are non-differentiable.

Q6: The writing seems to be quite dense and mathematical - how accessible is it to a general AI audience?
As work on certified adversarial robustness [2,3,4], in general, and closely related prior theoretical work [5,6], specifically, is frequently published at general AI venues (including ICLR), we believe our work to also be accessible to the audience of these venues, given that multiple reviewers highlighted the good presentation.

References:
[1] Müller et al. "The third international verification of neural networks competition (VNN-COMP 2022): summary and results." arXiv 2022
[2] Xu et al. “Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers” ICLR 2021 [3] Ferrari et al. "Complete verification via multi-neuron relaxation guided branch-and-bound." ICLR 2022
[4] Müller et al. “Certified training: Small boxes are all you need” ICLR 2023
[5] Baader et al. “Universal approximation with certified networks”, ICLR 2020
[6] Mirman et al. “The fundamental limits of neural networks for interval certified robustness”, TMLR 2022
[7] Pilanci and Ergen, Neural Networks are Convex Regularizers: Exact Polynomial-time Convex Optimization Formulations for Two-layer Networks, ICML 2020

I'd like to thank the authors for their detailed responses. The rebuttal clarified some of my concerns therefore I increase my score.

We thank the reviewer for their candid admission that they are not an expert in the field and are happy to provide a significantly extended version of the background, which we believe addresses all the reviewer's questions. We have incorporated some of these extensions (including a better intuition for Definition 3) into Section 2 in an effort to make our work more accessible.

Extended Background

Problem Setting
For clarity of exposition, we focus on the most common case of adversarially robust classification. We call a classifier $h: \mathcal{X} \to \mathcal{Y}$ locally robust around some input $x$ if it predicts the same, correct class for all similar inputs $\mathcal{B}^\epsilon_p(x) := \\{ x' \in \mathcal{X} \mid \| x - x' \|_p \leq \epsilon \\}$. Thus, to prove that a classifier is locally robust, we have to show $\forall x' \in \mathcal{B}, h(x') = h(x) = y$. For a neural network that predicts the class $h(x) \:= argmax_i f(x)_i$, we can equivalently show that the logit of the target class is always greater than that of all other classes, by solving the following optimization problem:

$0 < \min_{x' \in \mathcal{B}, i \neq y} f(x')_y - f(x')_i$

Convex Relaxations for Efficient Solution
Unfortunately, solving this problem exactly is NP-complete [1] as the neural network $f$ is highly non-linear and non-convex. Thus, state-of-the-art neural network verifiers use convex relaxations (combined with a branch-and-bound approach), to relax the above non-convex optimization problem to a (convex) linearly constrained linear program which can be solved much more efficiently [2]. More concretely, the non-linear activation layers (ReLUs), which can be seen as non-linear constraints in the original problem, are replaced with a set of linear constraints (the element-wise inequalities) in their input-output space. Intuitively, we relax the non-convex graph of the ReLU function with the convex over-approximations illustrated in Figures 1-4. However, as these convex-relaxations introduce an (over)-approximation error, these relaxed problems might be too imprecise to prove robustness even when the network is robust. In this work, we study for which classes of functions there exist ReLU networks such that this analysis does not lose precision depending on the relaxation method used.

Relevance of a $D$-Analysis
Solving the above optimization problem can geometrically be interpreted as linearly projecting the graph of the network (set of input-output tuples) for inputs in $\mathcal{B}$ to the 1d-line $f_y - f_i$ corresponding to the output difference for every $i \neq y$. While this projection is computationally efficient, computing the exact graph is still NP-complete. Thus, we can instead use convex relaxations to compute and then project (often in one step) an over-approximation of this graph and then check whether all points in this over-approximation are classified correctly. We call this over-approximate graph the $D$-analysis depending on the convex relaxation $D$ that was used. As the analysis with relaxation $D$ is precise if and only if the 1d projection of the exact graph and the $D$-analysis agree, this is a very natural and intuitive perspective on the problem.

We can now reformulate our above question as “For which function classes exist ReLU networks such that the 1d projection of their $D$-analysis (over-approximation of the graph) is precise, i.e., agrees with the projection of the exact graph?”. For “expressivity under convex relaxation” we thus do not only require that a given function can be encoded by a network (the default notion of expressivity and already shown for CPWL functions and ReLU networks by prior work [3]) but additionally require the analysis of the resulting network using the $D$ relaxation to be precise. Thus, $D$-expressivity depends on both the relaxation $D$ and the function class $F$.

For a more in-depth explanation of (certified) adversarial robustness including examples and visualizations, we recommend the excellent blog post by Eric Wong: https://locuslab.github.io/2019-03-12-provable/

Notation
All inequalities between vectors are element-wise. We have added a corresponding note to the Notation paragraph. Thanks for the pointer.

We are looking forward to the reviewer’s reply and are happy to provide further explanations or references and answer any follow-up questions.

References:
[1] Katz et al. "Reluplex: An efficient SMT solver for verifying deep neural networks." CAV 2017
[2] Salman, et al. "A convex relaxation barrier to tight robustness verification of neural networks." NeurIPS 2019
[3] He, et al. "ReLU deep neural networks and linear finite elements." JCM 2020