Convex relaxations are a key component of training and certifying provably safe neural networks. However, despite substantial progress, a wide and poorly understood accuracy gap to standard networks remains, raising the question of whether this is due to fundamental limitations of convex relaxations. Initial work investigating this question focused on the simple and widely used IBP relaxation. It revealed that some univariate, convex, continuous piecewise linear (CPWL) functions cannot be encoded by any ReLU network such that its IBP-analysis is precise.
To explore whether this limitation is shared by more advanced convex relaxations, we conduct the first in-depth study on the expressive power of ReLU networks across all commonly used convex relaxations. We show that: (i) more advanced relaxations allow a larger class of univariate functions to be expressed as precisely analyzable ReLU networks, (ii) more precise relaxations can allow exponentially larger solution spaces of ReLU networks encoding the same functions, and (iii) even using the most precise single-neuron relaxations, it is impossible to construct precisely analyzable ReLU networks that express multivariate, convex, monotone CPWL functions.

Expressivity of different relaxations.
Novel results are  red  and  green .
Previous results are in black (, ?).
M: monotone, C: convex, MC: monotone and convex.

$\bc{X}$     Relaxation     CPWL     M-CPWL     C-CPWL     MC-CPWL

-0     ?

-1     ?

§ INTRODUCTION

With the increased deployment of neural networks in mission-critical applications, formal robustness guarantees against adversarial examples [Biggio et al., 2013, Szegedy et al., 2014] have become an important and active field of research.
Many popular certification methods [Zhang et al., 2018, Singh et al., 2018, Singh et al., 2019, Singh et al., 2019] provide such safety guarantees by using convex relaxations to compute over-approximations of a network's reachable set w.r.t. an adversary specification.
However, despite significant progress, a wide and poorly understood accuracy gap between robust and conventional networks remains. This raises the fundamental question:

Is the expressivity of ReLU-networks under convex relaxations fundamentally limited?

Investigating this question, Mirman et al., 2022 prove that, the class of convex, continuous-piecewise-linear (CPWL) functions cannot be encoded as ReLU-networks such that their analysis with the simple -relaxation [Gehr et al., 2018, Gowal et al., 2018], is precise.

This Work: Expressivity of Common Relaxations
To investigate whether this limitation of is fundamental to all single-neuron convex relaxations, we conduct the first in-depth study on the expressive power of ReLU networks under all commonly used relaxations.
To this end, we consider CPWL functions, naturally represented by ReLU networks, and two common restrictions, convexity and monotonicity.
We illustrate our key findings in <ref>, showing novel results as  red  and  green  and previous results (, ) and open questions (?) in black.

Key Results on Univariate Functions In this work, we prove the following key results:

* The most precise single-neuron relaxation, (Wong & Kolter, 2018), and the popular -relaxation [Singh et al., 2019, Zhang et al., 2018] do not share 's limitation and can express univariate, convex, CPWL functions precisely.

* All considered relaxations, including , can express univariate, monotone, CPWL functions precisely.

* The -relaxation permits an exponentially larger network solution space for convex CPWL functions compared to the less precise -relaxation.

* Multi-neuron relaxations [Singh et al., 2019, Müller et al., 2022] can express all univariate, CPWL functions precisely using a single layer.

Having thus shown that, for univariate functions, the expressivity of ReLU networks under convex relaxations is not fundamentally limited, we turn our analysis to multivariate functions.

Key Results on Multivariate Functions  In this setting, we prove the following result:

* No single-neuron convex relaxation can precisely express even the heavily restricted class of multivariate, convex, monotone, CPWL functions.

Interestingly, the exact analysis of such monotone functions on box input regions is trivial, making the failure of convex relaxations even more surprising.
In fact, CPWL functions as simple as $f(x,y) = \max(x,y) = y + \RR(x-y)$ cannot be encoded by any finite ReLU network such that its -analysis is precise.
We thus conclude that, for multivariate functions, the expressivity of ReLU networks under single-neuron convex relaxations is fundamentally limited.

Implications of our Results for Certified Training
While we believe our results to be of general interest, they have particularly interesting implications for certified training.
In this area, all state-of-the-art methods [Müller et al., 2023, Mao et al., 2023, Palma et al., 2023] are based on the simple -relaxation even though it induces strong regularisation which severely reduces accuracy.
While Jovanovic et al., 2022 show that more precise relaxations induce significantly harder optimization problems, it remains an open question whether solving these would actually yield networks with better performance. Our results represent a major step towards answering this question.

Specifically in the univariate setting, we show that more precise relaxations increase expressivity (see <ref>) and lead to larger network solution spaces (compare <ref>). Thus, we hypothesize that using them during training yields a larger effective hypothesis space for the same network architecture. Importantly, this implies that networks with higher performance could indeed be obtained if we can overcome the optimization issues described by Jovanovic et al., 2022.

However, in the multivariate setting, perhaps surprisingly, we show that even the most precise single-neuron relaxations severely limit expressivity (see <ref>). This highlights the need for further study of more precise analysis methods such as multi-neuron or non-convex relaxations.

§ BACKGROUND ON CONVEX RELAXATIONS

Below, we first discuss notation and background before defining key concepts.

We denote vectors with bold lower-case letters $\va \in \R^n$, matrices with bold upper-case letters $\mA \in \R^{n \times d}$, and sets with upper-case calligraphic letters $\bc{A} \subset \R$.
We refer to a hyperrectangle $\bc{B} \subset \R^n$ as a box. Further, we consider (finite) ReLU networks $h$ with arbitrary skip connections.

§.§ Convex Relaxations in Neural Network Certification

Here, we discuss neural network certification methods based on convex relaxations. These methods cast the robustness problem as an optimization problem and make it tractable by replacing the non-convex activation functions with convex relaxations in their input-output space. Different choices of relaxations lead to different trade-offs between precision and computational cost.
Generally, all considered convex relaxations allow us to compute linear bounds on the output of a real-valued neural network $h$

\begin{equation*}
\{\mA_{l_i} \vx + b_{l_i}\}_{i \in \bc{L}} \leq h(\vx) \leq \{ \mA_{u_j} \vx + b_{u_j} \}_{j \in \bc{U}},
\end{equation*}

given an input region $\bc{B} = [\vl, \vu] \ni \vx$, where $\bc{L}$ and $\bc{U}$ are some index sets. These bounds can in-turn be bounded by $\vl_y = \min_{\vx \in \bc{B}} \max_{i \in \bc{L}}(\mA_{l_i} \vx + b_{l_i}) \in \R$ and $\vu_y = \max_{\vx \in \bc{B}} \min_{j \in \bc{U}}(\mA_{u_j} \vx + b_{u_j}) \in \R$. Hence, we have $\vl_y \leq \vh(\vx) \leq \vu_y$.

-relaxation (blue) of a ReLU with bounded inputs $v\in [l,u]$.

Interval bound propagation [Mirman et al., 2018, Gehr et al., 2018, Gowal et al., 2018] only considers elementwise, constant bounds of the form $\vl \leq \vv \leq \vu$. Affine layers $\vy = \mW \vv +\vb$ are thus also relaxed as

\begin{equation*}
\resizebox{.99\linewidth}{!}{$\tfrac{\mW (\vl+\vu) - |\mW|(\vu-\vl)}{2} + \vb \leq \mW \vv +\vb \leq \tfrac{\mW (\vl+\vu) + |\mW|(\vu-\vl)}{2} +\vb,$}
\end{equation*}

where $|\cdot|$ the elementwise absolute value. ReLU functions are relaxed by their concrete lower and upper bounds $\RR(\vl) \leq \RR(\vv) \leq \RR(\vu)$, illustrated in <ref>.

DeepPoly (DP)

-1 (blue) and -0 (green) abstraction of a ReLU with bounded inputs $v \in [l,u]$.

DeepPoly, introduced by Singh et al., 2019, is mathematically identical to CROWN [Zhang et al., 2018] and based on recursively deriving linear bounds of the form

\begin{equation*}
\mA_l \vx + \va_l \leq \vv \leq \mA_u \vx + \va_u
\end{equation*}

on the outputs of every layer. While this allows affine layers to be handled exactly, ReLU layers $\vy = \RR(\vv)$ are relaxed neuron-wise, using one of the two relaxations illustrated in <ref>

\begin{equation*}
\boldsymbol{\lambda} \vv \leq \RR(\vv) \leq (\vv-\vl) \frac{\vu}{\vu - \vl},
\end{equation*}

where product and division are elementwise.
Typically, the lower-bound slope $\lambda \in \{0,1\}$ is chosen depending on the input bounds $l$ and $u$. In this work, however, we analyze the relaxations obtained by always choosing the same lower-bound, which we denote with -0 (, green in <ref>) and -1 (, blue).

Triangle-Relaxation ()

-relaxation (blue) of a ReLU with bounded inputs $v\in [{l},{u}]$.

In contrast to the above convex relaxations, the -relaxation [Wong & Kolter, 2018, Dvijotham et al., 2018, Salman et al., 2019, Qin et al., 2019] maintains multiple linear upper- and lower-bounds on every network activation $v$. We write

\begin{equation*}
\begin{rcases} \mA_{l_1} \vx + \va_{l_1}, \\ \qquad\;  \vdots \\ \mA_{l_n} \vx + \va_{l_n}, \end{rcases} \leq \vv \leq \begin{cases} \mA_{u_1} \vx + \va_{u_1}, \\ \qquad\;  \vdots \\ \mA_{u_n} \vx + \va_{u_n}. \end{cases}
\end{equation*}

Unstable ReLU activation $\vy=\RR(\vv)$ with $\vl < \mathbf{0} < \vu$ are relaxed with their convex hull as illustrated in <ref>

\begin{equation*}
\begin{rcases} \mathbf{0} \\ \vv \end{rcases} \leq \RR(\vv) \leq (\vv-\vl) \frac{\vu}{\vu - \vl},
\end{equation*}

where again, product and division are elementwise.
Note that this can lead to an exponential growth (with the depth of the network) in the number of constraints for any given activation.

Multi-Neuron Relaxation ()

Comparison of a 2-neuron (green) and single-neuron (blue) relaxation projected into $y_2$-$v_1$-$v_2$-space for ReLU activations $y_i = \RR(v_i)$.

All methods introduced so far relax activation functions neuron-wise and are thus limited in precision by the (single neuron) convex relaxation barrier [Salman et al., 2019], i.e., the activation function's convex hull in their input-output space.

Multi-neuron relaxations, in contrast, compute the convex hull in the joint input-output space of multiple neurons in the same layer [Singh et al., 2019, Müller et al., 2022], or consider multiple inputs jointly [Tjandraatmadja et al., 2020]. We illustrate the increase in tightness in <ref> for a group of just $k=2$ neurons.

§.§ Definitions

We now define the most important concepts for this work.

We denote the set of continuous piecewise linear functions $f \colon \bc{X} \to \bc{Y}$ by $\cpwl(\bc{X}, \bc{Y})$. Further, if $\bc{X}$ is some interval $\I \subset \R$, then we enumerate the points where $f$ changes slope and call them $x_i$, where $0 \leq i \leq n$, $i < j$ implies $x_i < x_j$, and $\bc{X} = [x_0, x_n]$.

All $\cpwl$ functions $f\colon \I \to \R$ satisfy $f(x) = f(x_i) + (x - x_i) \tfrac{f(x_{i+1}) - f(x_i)}{x_{i+1} - x_{i}}$ for $x \in [x_i, x_{i+1}]$. We denote by M-CPWL, C-CPWL, and MC-CPWL the class of monotone (M), convex (C), and monotone & convex (MC) CPWL functions, respectively.
Next, we define the encoding of a function $f$ by a network $h$:

A neural network $h\colon \bc{X} \to \bc{Y}$ encodes a function $f\colon \bc{X} \to \bc{Y}$ if and only if for all $x \in \bc{X}$ we have $h(x) = f(x)$.

In the following, $D$ denotes a convex relaxation and can be , -0 (), -1 (), , or Multi-Neuron ():

Let $h\colon \bc{X} \!\to\! \bc{Y}$ be a network, $D$ a convex relaxation, and $\bc{B} \subset \bc{X}$ an input box. We denote by $h^D(\bc{B})$ the polytope in $h$'s input-output space containing the graph $\{(\vx, h(\vx)) \mid \vx \in \bc{B}\} \!\subseteq\! h^D(\bc{B}) \!\subseteq\! \bc{X} \times \bc{Y}$ of $h$ on $\bc{B}$, as obtained with $D$ and refer to it as the $D$-analysis of $h$ on $\bc{B}$.

For $\bc{Y} \subseteq \R$, we denote the interval bounds of $f$ on $\bc{B}$ by $[\underline{f(\bc{B})}, \overline{f(\bc{B})}] := [\min_{\vx \in \bc{B}} f(\vx), \max_{\vx \in \bc{B}} f(\vx)]$ and, similarly, the interval bounds implied by $h^D(\bc{B})$ as $[\underline{h^D(\bc{B})}, \overline{h^D(\bc{B})}] := [\min_{(\vx,y) \in h^D(\bc{B})} y, \max_{(\vx,y) \in h^D(\bc{B})} y]$.

As any $D$-analysis of $h$ captures the set of all possible outputs $h(\vx), \vx \in \bc{B}$, it is of key interest to us to investigate when the analysis does not lose precision.
Specifically, whether the linear output bounds $h^D(\bc{B})$ do not exceed the interval bounds of $f$ on $\bc{B}$ anywhere on $\bc{B}$:

Let $h$ be a network encoding $f \colon \bc{X} \to \bc{Y}$ and $D$ a convex relaxation. We say that the $D$-analysis is precise for $h$ if it yields precise lower and upper bounds, that is for all boxes $\bc{B} \subset \bc{X}$ we have that $[\underline{h^D(\bc{B})}, \overline{h^D(\bc{B})}] = [\underline{f(\bc{B})}, \overline{f(\bc{B})}]$.

In this work, we investigate the expressivity of ReLU-networks, that is, which function class they can encode such that their $D$-analysis is precise. Specifically:

Let $D$ be a convex relaxation, $\bc{F}$ a set of functions, and $\bc{N}$ a set of networks. We say that $\bc{N}$ can $D$-express $\bc{F}$ precisely, if and only if, for all $f \in \bc{F}$, there exists a network $h \in \mathcal{N}$, such that $h$ encodes $f$ and its $D$-analysis is precise.

We can often replace (sub-)networks to encode the same function but yield a (strictly) more precise analysis in terms of the obtained input-output polytope:

Let $h$ and $h'$ be $\RR$ networks, $\bc{B}$ a box, and $D$ some convex relaxation. We say $h'$ can replace $h$ with respect to $D$, if $h'^D(\bc{B}) \subseteq h^D(\bc{B})$ for all $\bc{B}$ and write $h \overset{D}{\rightsquigarrow} h'$.

§ RELATED WORK

Below, we give a brief overview of the most relevant related work.

Expressing CPWL Functions
He et al., 2020 show that ReLU networks require at least 2 layers to encode CPWL functions in $\R^d$ (for $d \geq 2$) with $\lceil \log_2(d+1) \rceil$ layers always being sufficient.

Expressivity with
Baader et al., 2020 show that for any continuous function $f \colon \Gamma \subset \R^n \to \R$ over a compact domain $\Gamma$ and $\epsilon > 0$, there exists a finite ReLU network $h$, such that its -analysis for any input box $\bc{B} \subset \Gamma$, denoted by $h^\boxd(\bc{B})$, is precise up to an $\epsilon$-error:

\begin{equation*}
[\underline{f(\bc{B})}+ \epsilon, \overline{f(\bc{B})}- \epsilon]
\subseteq
\subseteq
[\underline{f(\bc{B})}- \epsilon, \overline{f(\bc{B})}+ \epsilon].
\end{equation*}

An equivalent result immediately follows for all strictly more precise domains such as , , and .
Wang et al., 2022 propose a more efficient construction, generalize this result to squashable activation functions, and provide first results on the hardness of constructing such networks.

Investigating what class of functions allows for an exact -analysis, Mirman et al., 2022 show that for any function with points of non-invertibility, i.e., $x = 0$ for $f(x) = |x|$, there does not exist a ReLU network -expressing this function.

Certified Training
Certified training methods typically compute and then optimize an upper bound on the worst-case loss over some adversary specification computed via convex relaxations. Surprisingly, using the imprecise -relaxation [Mirman et al., 2018, Gowal et al., 2018] consistently yields better performance than tighter relaxations [Wong et al., 2018, Zhang et al., 2020, Balunovic & Vechev, 2020].
Jovanovic et al., 2022 investigate this paradox and identify two key properties of the worst-case loss approximation, continuity and sensitivity, required for effective optimization, with only possessing both.
However, the heavy regularization that makes trained networks amenable to certification also severely reduces their standard accuracy.

Neural Network Certification
We distinguish complete certification methods, which, given sufficient time, can decide any property, i.e., always compute precise bounds, and incomplete methods, which sacrifice precision for speed.
Salman et al., 2019 unify a range of incomplete certification methods including , , and , and show that their precision is limited by that of the -relaxation. They observe that for a wide range of networks and even when using the -relaxation, a substantial certification gap between the upper- and lower-bounds on robust accuracy remains.
Semidefinite programming based methods [Dathathri et al., 2020, Raghunathan et al., 2018] increase tightness at the cost of computational efficiency.

Early, complete certification methods directly leveraged off-the-shelf SMT [Katz et al., 2017, Ehlers, 2017] or MILP solvers [Dutta et al., 2018, Tjeng et al., 2019], limiting their applicability to small networks. To improve scalability, Bunel et al., 2020 formulate a branch-and-bound (BaB) framework, that recursively splits the certification problem into easier subproblems until they can be decided by cheap incomplete methods. This concept has been widely adopted and improved using more efficient solvers [Xu et al., 2021, Wang et al., 2021] and tighter constraints [Palma et al., 2021, Ferrari et al., 2022, Zhang et al., 2022].

§ CONVEX RELAXATIONS FOR UNIVARIATE FUNCTIONS

In this section, we differentiate all convex relaxations that are commonly used for neural network certification (, , , , and ) in terms of their expressivity, i.e., with respect to the function classes they can analyze precisely when encoded by a ReLU network.

We first show that finite-depth ReLU networks can -express M-CPWL functions precisely (<ref>).
This construction can be applied directly to the strictly more precise and relaxation and with slight modification also to .
We, then, show that while finite ReLU networks can both - and -express M-CPWL and C-CPWL functions, the solution space is exponentially larger when using the more precise -analysis.
Finally, we show that single-layer ReLU networks can -express arbitrary CPWL functions.
We defer all proofs and supplementary lemmata to <ref>.

§ CONVEX RELAXATIONS FOR MULTIVARIATE FUNCTIONS

§ CONCLUSION

We conduct the first in-depth study on the expressivity of ReLU networks under all commonly used convex relaxations and find that:
(i) more precise relaxations (, or ) allow a larger class of univariate functions (C-CPWL and M-CPWL) to be expressed precisely than the simple -relaxation (M-CPWL),
(ii) for the same function class (C-CPWL), a more precise relaxation (vs or ), can allow an exponentially larger solution space of ReLU networks,
(iii) -relaxations allow single-layer networks to express all univariate CPWL functions,
(iv) even the most precise single-neuron relaxation () is too imprecise to express multivariate, convex, monotone CPWL functions precisely with finite ReLU networks, despite their exact analysis being trivial.

While more precise domains improve expressivity for univariate functions, all single-neuron convex-relaxations are fundamentally limited in the multivariate setting.
Surprisingly, even simple functions that can be encoded with a single neuron $h = y + \RR(x-y) = \max(x,y)$, can not be -expressed precisely using any finite ReLU network.
This highlights not only the importance of recent, more precise multi-neuron- and BaB-based neural network certification methods but also suggests more precise methods might be needed for training.

^^JLASTBODYPAGE ^^J

[Baader et al., 2020]
Maximilian Baader, Matthew Mirman, and Martin T. Vechev.
Universal approximation with certified networks.
In Proc. of ICLR, 2020.

[Balunovic & Vechev, 2020]
Mislav Balunovic and Martin T. Vechev.
Adversarial training and provable defenses: Bridging the gap.
In Proc. of ICLR, 2020.

[Biggio et al., 2013]
Battista Biggio, Igino Corona, Davide Maiorca, Blaine Nelson, Nedim Srndic,
Pavel Laskov, Giorgio Giacinto, and Fabio Roli.
Evasion attacks against machine learning at test time.
In Proc of ECML PKDD, 2013.

[Bunel et al., 2020]
Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and
M. Pawan Kumar.
Branch and bound for piecewise linear neural network verification.
J. Mach. Learn. Res., 2020.

[Dathathri et al., 2020]
Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan,
Jonathan Uesato, Rudy Bunel, Shreya Shankar, Jacob Steinhardt, Ian J.
Goodfellow, Percy Liang, and Pushmeet Kohli.
Enabling certification of verification-agnostic networks via
memory-efficient semidefinite programming.
In Proc. of NeurIPS, 2020.

[Dutta et al., 2018]
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari.
Output range analysis for deep feedforward neural networks.
In Proc. of NFM, 2018.

[Dvijotham et al., 2018]
Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A. Mann, and
Pushmeet Kohli.
A dual approach to scalable verification of deep networks.
In Proc. of UAI, 2018.

[Ehlers, 2017]
Rüdiger Ehlers.
Formal verification of piece-wise linear feed-forward neural
In ATVA, 2017.

[Ferrari et al., 2022]
Claudio Ferrari, Mark Niklas Müller, Nikola Jovanovic, and Martin T.
Complete verification via multi-neuron relaxation guided
In Proc. of ICLR, 2022.

[Gehr et al., 2018]
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat
Chaudhuri, and Martin T. Vechev.
AI2: safety and robustness certification of neural networks with
abstract interpretation.
In S&P, 2018.

[Gowal et al., 2018]
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin,
Jonathan Uesato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli.
On the effectiveness of interval bound propagation for training
verifiably robust models.
ArXiv preprint, abs/1810.12715, 2018.

[He et al., 2020]
Juncai He, Lin Li, Jinchao Xu, and Chunyue Zheng.
Relu deep neural networks and linear finite elements.
Journal of Computational Mathematics, 0 (3), 2020.
ISSN 1991-7139.

[Jovanovic et al., 2022]
Nikola Jovanovic, Mislav Balunovic, Maximilian Baader, and Martin T. Vechev.
On the paradox of certified training.
Trans. Mach. Learn. Res., 2022.

[Katz et al., 2017]
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J.
Reluplex: An efficient SMT solver for verifying deep neural
ArXiv preprint, abs/1702.01135, 2017.

[Mao et al., 2023]
Yuhao Mao, Mark Niklas Müller, Marc Fischer, and Martin T. Vechev.
TAPS: connecting certified and adversarial training.
In Proc. of NeurIPS, 2023.

[Mirman et al., 2018]
Matthew Mirman, Timon Gehr, and Martin T. Vechev.
Differentiable abstract interpretation for provably robust neural
In Proc. of ICML, 2018.

[Mirman et al., 2022]
Matthew Mirman, Maximilian Baader, and Martin T. Vechev.
The fundamental limits of neural networks for interval certified
Trans. Mach. Learn. Res., 2022.

[Müller et al., 2022]
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus
Püschel, and Martin T. Vechev.
PRIMA: general and precise neural network certification via
scalable convex hull approximations.
In Proc. of POPL, 2022.

[Müller et al., 2023]
Mark Niklas Müller, Franziska Eckert, Marc Fischer, and Martin T. Vechev.
Certified training: Small boxes are all you need.
In Proc. of ICLR, 2023.

[Palma et al., 2021]
Alessandro De Palma, Harkirat S. Behl, Rudy Bunel, Philip H. S. Torr, and
M. Pawan Kumar.
Scaling the convex barrier with active sets.
In Proc. of ICLR, 2021.

[Palma et al., 2023]
Alessandro De Palma, Rudy Bunel, Krishnamurthy Dvijotham, M. Pawan Kumar,
Robert Stanforth, and Alessio Lomuscio.
Expressive losses for verified robustness via convex combinations.
CoRR, abs/2305.13991, 2023.

[Qin et al., 2019]
Chongli Qin, Krishnamurthy (Dj) Dvijotham, Brendan O'Donoghue, Rudy Bunel,
Robert Stanforth, Sven Gowal, Jonathan Uesato, Grzegorz Swirszcz, and
Pushmeet Kohli.
Verification of non-linear specifications for neural networks.
In Proc. of ICLR, 2019.

[Raghunathan et al., 2018]
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang.
Semidefinite relaxations for certifying robustness to adversarial
In Proc. of NeurIPS, 2018.

[Salman et al., 2019]
Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang.
A convex relaxation barrier to tight robustness verification of
neural networks.
In Proc. of NeurIPS, 2019.

[Singh et al., 2018]
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and
Martin T. Vechev.
Fast and effective robustness certification.
In Proc. of NeurIPS, 2018.

[Singh et al., 2019]
Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin T. Vechev.
Beyond the single neuron convex barrier for neural network
In Proc. of NeurIPS, 2019a.

[Singh et al., 2019]
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev.
An abstract domain for certifying neural networks.
Proc. of POPL, 2019b.

[Szegedy et al., 2014]
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan,
Ian J. Goodfellow, and Rob Fergus.
Intriguing properties of neural networks.
In Proc. of ICLR, 2014.

[Tjandraatmadja et al., 2020]
Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Patel,
and Juan Pablo Vielma.
The convex relaxation barrier, revisited: Tightened single-neuron
relaxations for neural network verification.
In Proc. of NeurIPS, 2020.

[Tjeng et al., 2019]
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake.
Evaluating robustness of neural networks with mixed integer
In Proc. of ICLR, 2019.

[Wang et al., 2021]
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and
J. Zico Kolter.
Beta-crown: Efficient bound propagation with per-neuron split
constraints for neural network robustness verification.
In Proc. of NeurIPS, 2021.

[Wang et al., 2022]
Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha.
Interval universal approximation for neural networks.
Proc. of POPL, 2022.

[Wong & Kolter, 2018]
Eric Wong and J. Zico Kolter.
Provable defenses against adversarial examples via the convex outer
adversarial polytope.
In Proc. of ICML, 2018.

[Wong et al., 2018]
Eric Wong, Frank R. Schmidt, Jan Hendrik Metzen, and J. Zico Kolter.
Scaling provable adversarial defenses.
In Proc. of NeurIPS, 2018.

[Xu et al., 2021]
Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and
Cho-Jui Hsieh.
Fast and complete: Enabling complete neural network verification with
rapid and massively parallel incomplete verifiers.
In Proc. of ICLR, 2021.

[Zhang et al., 2018]
Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel.
Efficient neural network robustness certification with general
activation functions.
In Proc. of NeurIPS, 2018.

[Zhang et al., 2020]
Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li,
Duane S. Boning, and Cho-Jui Hsieh.
Towards stable and efficient training of verifiably robust neural
In Proc. of ICLR, 2020.

[Zhang et al., 2022]
Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh,
and J. Zico Kolter.
General cutting planes for bound-propagation-based neural network
In Proc. of NeurIPS, 2022.

^^JLASTREFERENCESPAGE ^^J