Year: 2021

Abstract:
Deep equilibrium layers (DEQs) have demonstrated promising performance and are competitive with standard explicit models on many benchmarks. However, little is known about certifying robustness for these models. Inspired by interval bound propagation (IBP), we propose the IBP-MonDEQ layer, a DEQ layer whose robustness can be verified by computing upper and lower interval bounds on the output. Our key insights are that these interval bounds can be obtained as the fixed-point solution to an IBP-inspired equilibrium equation, and furthermore, that this solution always exists and is unique when the layer obeys a certain parameterization. This fixed point can be interpreted as the result of applying IBP to an infinitely deep, weight-tied neural network, which may be of independent interest, as IBP bounds are typically unstable for deeper networks. Our empirical comparison reveals that models with IBP-MonDEQ layers can achieve comparable or better `8 certified robustness than similarly-sized fully explicit networks.

heading: 1 INTRODUCTION
text: A recent development in neural network design has been the introduction of implicit layers (Amos & Kolter, 2017; Chen et al., 2018; Agrawal et al., 2019; Bai et al., 2019; 2020; El Ghaoui et al., 2021), where the output is defined implicity as the solution to certain sets of conditions, rather than explicitly, via closed-form functions. These layers are promising alternatives to standard explicit deep learning layers and have demonstrated improved expressivity and inductive biases in a variety of settings, for example, processing time series (Rubanova et al., 2019), generative modeling (Grathwohl et al., 2018), solving logical reasoning tasks (Wang et al., 2019), solving two player games (Ling et al., 2018), and many others. One particularly promising class of implicit layers is deep equilibrium layers (DEQs) (Bai et al., 2019), which define the output as the solution to an input-dependent fixed point equation. DEQ-based models have matched or outperformed traditional explicit models even in commonly benchmarked settings (Bai et al., 2019; 2020).
Though recent empirical successes of DEQs have been promising, their implicit nature and inherent mathematical complexity also give rise to basic concerns. In order for DEQs to realize their promise, these concerns should ideally be mitigated or resolved. For example, one major issue with DEQs is well-posedness – a solution to the fixed point equation defining the layer might not exist. On the other hand, explicit layers always have well-defined outputs. A recent line of work has focused on addressing this important concern (Winston & Kolter, 2020; Revay et al., 2020; Xie et al., 2021).
This paper tackles a less-studied, but also important, question for DEQs: certified adversarial robustness. Because robustness is a basic concern for safe deployment of deep models (Szegedy et al., 2013; Goodfellow et al., 2014), for explicit models there is a large literature dedicated to certifying robustness, or guaranteeing correctness of the predictions even when the input is subject to imperceptible adversarial perturbations (see e.g. (Raghunathan et al., 2018a; Wong & Kolter, 2018; Gowal et al., 2018; Dvijotham et al.; Xiao et al., 2018; Cohen et al., 2019)). Many certified robustness methods require opening up the black box of the model and therefore only work for explicit models. It is unclear how to certify robustness of DEQs, which are only defined implicitly.
The certified robustness method motivating this work is interval bound propagation (IBP) (Mirman et al., 2018; Gowal et al., 2018), a simple and cheap way to certify robustness to `8 perturbations. IBP computes layerwise upper and lower bounds for each coordinate of the adversarially perturbed hidden layers. These bounds follow basic rules of interval arithmetic and are simple to obtain in
closed form as explicit functions of a layer’s weights. However, it is unclear how to apply this idea when layers are only defined implicitly.
In this paper, we propose the IBP-MonDEQ, a deep equilibrium layer which is certifiably robust to `8 perturbations. Motivated by principles from IBP, we define the IBP-MonDEQ output as the solution of an augmented fixed-point equation involving 3 quantities: the unperturbed output of the layer and upper and lower interval bounds on this output. As with IBP for explicit models, interval bounds on the IBP-MonDEQ output are computed during the forward pass of the network and can be composed with other layers to certify robustness of the entire model.
More concretely, we build upon monotone operator deep equilibrium (MonDEQ) layers proposed by Winston & Kolter (2020), which take the preceding layer vpxq as input and outputs the solution z‹, which is guaranteed existence and uniqueness, to the following fixed-point equation:
z‹ “ σpWz‹ ` vpxqq (1.1) We propose an IBP-inspired fixed-point equation
„
sz‹ z‹
 “ σ ˆ„ pW q` pW q´ pW q´ pW q`  „ sz‹ z‹  ` „ svpxq vpxq ˙
(1.2)
which maps upper and lower interval bounds sv, v on v to sz‹ and z‹, which provide upper and lower interval bounds on z‹. Figure 1 depicts this process. The augmented fixed-point equation is derived by unrolling the computation of z‹ into an infinitely deep, explicit network and applying IBP to the forward pass of this network.
One immediate challenge is that it is not clear that a fixed point solution to (1.2) should always exist, especially given its interpretation as the result of applying IBP to an infinitely deep network. Indeed, a major drawback of IBP is that its performance degrades with deeper networks, as observed by Shi et al. (2021) and also shown in Figure 2 (left). One potential explanation for this failure is that IBP bounds tend to be unstable with depth and can diverge for deeper models (Figure 2, right).
On the other hand, we show that a unique fixed-point solution to (1.2) is guaranteed to exist whenW admits a simple unconstrained parameterization which is easy to enforce throughout training. Thus, our results pinpoint a class of infinitely deep networks for which IBP bounds are provably stable, which may be of independent interest.
We experimentally compare the proposed IBP-MonDEQ layer against IBP for standard explicit models. We consider common certified robustness benchmark settings and evaluate architectures of various sizes. Our results show that models with IBP-MonDEQ layers can achieve comparable or better `8 certified robustness relative to fully explicit models with similar parameter counts.
In summary, our contributions are as follows: 1) We study the certified robustness of DEQs, proposing the IBP-MonDEQ, a class of DEQs with a guaranteed unique fixed point with provable interval bounds on the fixed point value. 2) The proposed IBP-MonDEQs form an expressive class of infinitely-deep models for which IBP is provably stable, which may be of independent interest. 3) Our experiments demonstrate that IBP-MonDEQ layers are competitive with standard explicit layers for `8-certified robustness.

heading: 2 BACKGROUND
text: `8 certified robustness. Consider a K-way classification task with neural network classifier F : Rd Ñ RK . For a given input x with true label y, the classifier F is adversarially robust to `8 perturbations with radius if
min δPRd:}δ}8ď
F px` δqy ´ F px` δqy1 ą 0 @y1 ‰ y (2.1)
Safety-critical applications require certifying the robustness of F , i.e., verifying whether 2.1 holds. Directly optimizing over δ to verify (2.1) is challenging because the objective is non-convex (Madry et al., 2017). Thus, recent work on certified robustness has focused on verifying (2.1) via computationally tractable relaxations (Raghunathan et al., 2018a; Wong & Kolter, 2018; Dvijotham et al.; Raghunathan et al., 2018b; Weng et al., 2018; Gowal et al., 2018; Salman et al., 2019b).
Interval bound propagation. IBP is a computationally efficient method for certifying `8 robustness of neural networks (Mirman et al., 2018; Gowal et al., 2018). It proposes to verify (2.1) via a (potentially loose) upper bound on F px ` δqy ´ F px ` δqy1 which is obtained by computing propagating upper and lower bounds on each layer through the forward pass of the network.
More precisely, let zpxq compute some hidden layer of the network on input x. We say that szpx, q, zpx, q are interval bounds on z at x for perturbation if the following holds for all coordinates i:
pzpx, qqi ď min δPRd:}δ}8ď pzpx` δqqi ď max δPRd:}δ}8ď pzpx` δqqi ď pszpx, qqi (2.2)
We omit dependencies on x and when clear from context. Letting k denote the layer index, the bounds szk and zk are obtained inductively via simple interval arithmetic. For an affine layer zk “ Wzk´1 ` b and pre-computed bounds zk´1, szk´1, IBP computes szk, zk as follows:
„
szk zk
 “ „ pW q` pW q´ pW q´ pW q`  „ szk´1 zk´1  ` „ b b 
(2.3)
Here pW q` fi maxtW, 0u and pW q´ fi mintW, 0u denote the matrix W with negative or positive values truncated to 0. For simplicity we focus on ReLU networks, with σ denoting the ReLU activation. For layers zk “ σpzk´1q which apply σ coordinate-wise, IBP computes szk “ σpszk´1q and zk “ σpzk´1q. Initial bounds are obtained via psz0px, q, z0px, qq “ px` 1, x´ 1q, where 1 denotes the all 1’s vector.
The interval bounds are propagated through all layers of the network by following the simple rules above. To certify (2.1) for the whole network, one straightforward method is to confirm that the margins of the interval bounds on the logits are positive: pF px, qqy ´ p sF px, qqy1 ą 0 @y1 ‰ y. One important note about IBP is that the bounds should be optimized during training in order for the method to provide nontrivial robustness guarantees.
Monotone operator equilibrium networks. Proposed by Winston & Kolter (2020), MonDEQs are a class of DEQs inspired by monotone operator theory (Ryu & Boyd, 2016) which have guaranteed unique fixed point solutions to the following equilibrium equation:
z‹ “ σpWz‹ ` vpxqq (2.4) Let Ihˆh denote the identity matrix on h dimensions, with the subscript omitted when clear. A unique fixed-point solution is guaranteed for (2.4) for the following class of W : Proposition 2.1 ((Winston & Kolter, 2020)). Suppose W P Rhˆh satisfies that I ´W is positive definite (PD), i.e. I ´W ą 0. Then @vpxq P Rh, a solution z‹ to (2.4) exists and is unique.
Here 0 denotes the all 0’s matrix and A ą 0 indicates that uJAu ą 0 for all nonzero u (note that A does not need to be symmetric). Winston & Kolter (2020) guarantee that I ´ W is PD using the following unconstrained parameterization, which is enforced throughout training: W “ p1´mqI ´AAJ `B ´BJ, for positive hyperparameter m. Section 3.1 builds on these results to derive certified upper and lower bounds on z‹.

heading: 3 CERTIFYING ROBUSTNESS OF MONDEQS USING IBP
text: In this section, we describe our core methodology for developing certifiably robust MonDEQ layers. We will first demonstrate how to obtain interval bounds for MonDEQ layers by computing the
solution to a certain IBP-inspired fixed point equation (3.3). In Section 3.1, we characterize a new parameterization for W for which a unique fixed point exists. In Section 3.3, we provide theoretical justification that the resulting IBP-MonDEQ layers remain expressive.
Our aim is to derive upper and lower interval bounds sz‹ and z‹ for the fixed point solution to (2.4). A common interpretation of DEQs is that they compute an infinitely deep, unrolled explicit network (Bai et al., 2019; Winston & Kolter, 2020):
zk “ σpWzk´1 ` vq (3.1)
with limkÑ8 zk “ z‹. This equivalence is informal and mainly serves to motivate our derivation of the IBP-MonDEQ. Given interval bounds sv and v on v satisfying v ď v ď sv, where the inequalities hold elementwise, we can also follow IBP and (2.3) to iteratively obtain interval bounds on zk:
„
szk zk
 “ σ ˆ„ pW q` pW q´ pW q´ pW q`  „ szk´1 zk´1  ` „ sv v ˙
(3.2)
Just as we took limkÑ8 zk, we consider limkÑ8 szk, zk, motivating another fixed-point problem: „
sz‹ z‹
 “ σ ˆ„ pW q` pW q´ pW q´ pW q`  „ sz‹ z‹  ` „ sv v ˙
(3.3)
As shown in Figure 1, this IBP-inspired fixed point equation essentially maps the region tv1 : v ď v1 ď svu to the region tz‹1 : z‹ ď z‹1 ď sz‹u, where inequalities are coordinate-wise. If they exist, the fixed points sz‹ and z‹ will indeed lead to valid interval bounds (as defined in (2.2)) on z‹. Proposition 3.2 states this observation formally.

heading: 3.1 FIXED POINTS OF THE IBP-INSPIRED EQUILIBRIUM EQUATION
text: Following the derivation above, the IBP fixed point equation (3.3) can be interpreted as the result of applying IBP to an infinitely deep, weight-tied neural network. However, IBP is notoriously unstable for deeper networks, so it is unclear whether a fixed point solution to (3.3) always exists. This section characterizes a class of W for which (3.3) does have a fixed point (Theorem 3.1).
Figure 2 (left) demonstrates that the performance of IBP degrades for deep networks. We add linear layers to the architecture proposed by Gowal et al. (2018) for IBP, which is a wide but shallow network with 6 linear layers, and find that the final error certified by IBP increases with the depth of the model. This illustrates the challenge of getting IBP to work for deep models.
The challenges associated with depth also apply to the class of MonDEQs proposed by (Winston & Kolter, 2020). We will define xW fi „
pW q` pW q´ pW q´ pW q`

P R2hˆ2h to be the linear transformation
for IBP. Recall that Proposition 2.1 demonstrates existence and uniqueness of a fixed point solution to (2.4) when Ihˆh´W is PD, but this does not guarantee the positive-definiteness of I2hˆ2h´xW , which would be sufficient for a fixed point solution to (3.3). Indeed, Figure 2 (right) shows that the fixed-point solver fails to solve (3.3) for the standard MonDEQ, as the interval bounds diverge. Intuitively, this failure occurs because the spectral radius of xW is always larger than that of W (see Lemma 3.4), so repeated application of (3.2) diverges. Thus, further restrictions on W are required.
The following theorem exactly characterizes the class of W for which I2hˆ2h´xW is PD. For these W , existence and uniqueness of fixed points to (2.4) and (3.3) is guaranteed to hold.
Theorem 3.1. In the setting above, I2hˆ2h ´xW ą 0 if and only if W is parameterized as follows:
W “ D´1{2MD´1{2 (3.4)
where D,M P Rhˆh and D is a diagonal matrix satisfying Di,i ą p|M |1qi`p|M | J1qi
2 , where |M | P Rhˆh takes the entry-wise absolute value of M . Thus, for W parameterized by (3.4), unique solutions z‹, sz‹, z‹ to the standard (2.4) and IBP (3.6) equilibrium equations exist @ v, sv, v P Rh.
Theorem 3.1 is our main theoretical result, and proposes a simple class of W for which the IBP equilibrium equation has a guaranteed unique fixed point. In this characterization, M is an unconstrained matrix (and is also treated as an unconstrained parameter in our implementation, as described in Section 4). The scaling matrix D normalizes M . In Section 3.3, we theoretically analyze the expressivity of the induced class of DEQ layers. The proof of Theorem 3.1 is discussed in Section 3.2.
Next, it remains to check that sz‹ and z‹ do provide valid interval bounds on z‹, as the derivation in Section 3 was only heuristic. The following proposition makes this derivation rigorous.
Proposition 3.2. In the setting above, suppose xW satisfies I2hˆ2h ´xW ą 0, so that unique fixedpoint solutions sz‹, z‹ to (3.3) always exist. Define the fixed-point solution z‹pvq as a function of v as follows: z‹pvq “ σpWz‹pvq ` vq. Then for any v ď sv and all i, it must hold that
pz‹qi ď min vďvďsv pz‹pvqqi ď max vďvďsv pz‹pvqqi ď p sz‹qi (3.5)
We present the proof in Section A. Combining Theorem 3.1 and Proposition 3.2, we finally obtain the IBP-MonDEQ layer, which simultaneously solves two equilbrium equations to output both z‹ and valid upper and lower interval bounds sz‹, z‹ on z‹:
z‹ “ σpWz‹ ` vpxqq „
sz‹ z‹
 “ σ ˆ„ pW q` pW q´ pW q´ pW q`  „ sz‹ z‹  ` „ svpx, q vpx, q ˙
(3.6)
To include an IBP-MonDEQ layer in a deeper model, we set vpxq to be the output of the preceding layer, and choose svpx, q, vpx, q to be upper and lower interval bounds on vpxq. The interval bounds sz‹ and z‹ can be propagated through the rest of the network following the standard IBP methods.
LBEN parameterization. We can relax the restrictions imposed by the parameterization (3.4) by leveraging the Lipschitz-bounded equilibrium network (LBEN) parameterization proposed by Revay et al. (2020). Revay et al. (2020) show that a guaranteed unique fixed point of (2.4) still exists if the PD condition on I´W is relaxed to require Λ´ΛW ą 0 for Λ P Dhˆh` , the set of positive diagonal matrices. The following result exactly characterizesW such that DΛ P Dhˆh` : Λ´Λ|W | ą 0, which is also sufficient for guaranteeing a unique fixed point solution to (3.3).
Theorem 3.3. For weight matrix W , DΛ P Dhˆh` such that Λ´ Λ|W | ą 0 if and only if W can be parameterized as follows:
W “ ΓD´1{2MD´1{2Γ´1 (3.7)
for some Γ, D P Dhˆh` with D satisfying Di,i ą p|M |1`|M |J1q 2 .
For W parameterized by (3.7), we have the following immediate consequences: 1) unique solutions z‹, sz‹, z‹ to the equilbrium equations (3.6) exist for all v, sv, v P Rh, and 2) sz‹, z‹ are upper and lower interval bounds on z‹ in the sense of Proposition 3.2.
The proof is provided in Section A. Note that Theorem 3.3 improves the expressivity of the IBPMonDEQ layer because the class of W proposed in Theorem 3.3 contains that of Theorem 3.1. In Section 3.3, we show that, perhaps surprisingly, this more flexible parameterization allows IBPMonDEQ layers to express all explicit networks. Section 4 demonstrates that this parameterization can also lead to empirical improvements.

heading: 3.2 PROOF OF THEOREM 3.1
text: We sketch the proof of Theorem 3.1. To prove I2hˆ2h ´xW ą 0, we require a simple way to reason about the spectrum of xW . The following lemma formalizes a connection between eigenvalues of xW`xWJ
2 and |W |`|W |J 2 .
Lemma 3.4. All eigenvalues of xW`xW J 2 are either eigenvalues of W`WJ 2 or |W |`|W |J
2 . As a direct consequence, the following equivalence holds:
I2hˆ2h ´xW ą 0 ðñ Ihˆh ´ |W | ą 0 (3.8)
Note that the condition that Ihˆh ´ |W | is PD is a stricter requirement than requiring positivedefiniteness of Ihˆh ´W , as it always holds that λmaxp |W |`|W | J 2 q ě λmaxp W`WJ
2 q, where λmax denotes the largest eigenvalue. Thus, in order for both (2.4) and (3.3) to have unique fixed points, it suffices to have Ihˆh ´ |W | ą 0. The proof of Lemma 3.4 is completed in Section A and relies on the following basic fact about structured block matrices.
Claim 3.5. Let M P R2hˆ2h be any matrix of the form M “ „
A B B A

, where A,B P Rhˆh. Then
all eigenvalues of M are either eigenvalues of A`B or A´B.
Following Lemma 3.4, we now complete the proof of Theorem 3.1 by analyzing Ihˆh ´ |W |.
Proof of Theorem 3.1. By Lemma 3.4, it is equivalent to characterize when Ihˆh ´ |W | ą 0. We first show that (3.4) implies positive-definiteness. We write
I ´ |W | ` |W | J
2 “ D´1{2
ˆ D ´ |M | ` |M | J
2
˙
D´1{2 (3.9)
By the lower bound on entries of D, the matrix D ´ |M |`|M | J
2 is symmetric and strictly diagonally
dominant (SDD), and thus PD. Thus, we obtain I ´ |W |`|W | J
2 ą 0, so I ´ |W | ą 0. For the reverse direction, we appeal to the theory of M-matrices (Plemmons, 1977). We note that I ´ |W |`|W | J
2 is a nonsingular M-matrix, i.e., a matrix with negative off-diagonal entries whose eigenvalues have positive real parts. By an equivalent characterization of M-matrices, there exists a diagonal matrix E P D` such that EpI ´ |W |`|W | J
2 qE is SDD. Rearranging gives |W | “ I ´ E´1AE´1 ` S, where A is symmetric and SDD, and S is skew-symmetric (SJ “ ´S). Now we choose M satisfying |M | “ E2 ´ A ` ESE and D “ E2, so that W has the parameterization W “ D´1{2MD´1{2. To check that Di,i ą p|M |1qi`p|M | J1qi 2 , we note that p|M |1qi`p|M |J1qi 2 “ ppE 2 ´ Aq1qi “ E2i,i ´ Ai,i ´ ř
j‰iAi,j ă E2i,i, where we use the fact that Ai,i ą ř j‰i |Ai,j | because A is SDD. Plugging in Di,i “ E2i,i gives the desired inequality.

heading: 3.3 EXPRESSIVITY OF THE IBP-MONDEQ
text: Guaranteeing that (3.3) has a fixed point requires placing further restrictions on W on top of those already proposed for MonDEQs (Winston & Kolter, 2020). This section examines the expressivity
of the resulting IBP-MonDEQ parameterization. To sanity check that our parameterization is not too restrictive, we first contrast against normalization techniques for controlling Lipschitz constants in neural networks. Next, we demonstrate that with the relaxed parameterization of Theorem 3.3, the IBP-MonDEQ is able to express traditional explicit feedforward networks.
Operator norm of W . We first investigate the operator norm of W . A number of papers constrain the weight matrices so that their operator norms are bounded by 1, which prevents blowup of the naive upper bound ś
i }Wi}op on the Lipschitz constant of the whole network (Cisse et al., 2017; Miyato et al., 2018; Farnia et al., 2018; Trockman & Kolter, 2021). This approach has applications in robustness, but there are also concerns that constraining the operator norms to 1 severely harms expressivity (Huster et al., 2018; Anil et al., 2019). We verify that the parameterization of Theorem 3.1 does not imply the stringent constraint }W }op ď 1. Example 3.6. The following choice of W satisfies the parameterization (3.4) with }W }op “ 1.9: W “ „
0 1.9 0.05 0

. We set M “W and D “ I2ˆ2, so W “ D´1{2MD´1{2 as in (3.4).
Example 3.6 may be surprising given superficial similarities between (3.4) and the following parameterization, which does imply }W }op ď 1: W “ D´1M , where D satisfies Di,i ě p|M |1qi. The parameterization in Theorem 3.1 avoids this constraint because the requirement is instead Di,i ě p|M |1`|M | J1qi 2 , so mass in M can be asymmetrically distributed between the upper and lower triangular halves, as in Example 3.6.
Expressing explicit feedforward networks. The following result states that using the parameterization in Theorem 3.3, a single IBP-MonDEQ layer can express all explicit feedforward networks. Proposition 3.7. Consider explicit neural net embedding functions of the following form:
zLpxq “ σpALσpAL´1 ¨ ¨ ¨σpA1xq ¨ ¨ ¨ qq (3.10)
where zL : Rd Ñ Rh andAi P Rhˆh @1 ď i ď L. There is a DEQ layer z‹ : Rd Ñ RLh outputting z‹pxq “ σpWz‹pxq ` Bxq, where W,B P RLhˆLh, such that W obeys the parameterization of Theorem 3.3, and the last h coordinates of z‹ satisfy
pz‹pxqqpL´1qh:Lh “ zLpxq @x P Rd
Proposition 3.7 states that the IBP-MonDEQ parameterized in Theorem 3.3 is at least as powerful as standard explicit networks, and is somewhat surprising given that the parameterizations (3.4) and (3.7) may appear restrictive. The proof, provided in Section A, leverages the fact that Γ provides flexibility in scaling the weights, essentially allowing us to cancel out the normalization matrix D.

heading: 4 EXPERIMENTS
text: In this section, we empirically compare models with IBP-MonDEQ layers against fully explicit models. Our results show that IBP-MonDEQ models can achieve comparable or improved performance on common certified robustness benchmarks compared to IBP with standard explicit models.
Explicit models. Table 1 illustrates the explicit architectures: a smaller 3LAYER model with 2 convolutional layers and 128 output channels, and a larger 7LAYER model. The 7LAYER model is a wide and shallow network with 17 million parameters proposed by Gowal et al. (2018) for IBP.
IBP-MonDEQ models. As shown in Table 1, we consider replacing a convolutional layer in a fullyexplicit model with an IBP-MonDEQ layer where W computes an equivalently-sized convolutional transformation. This leads to DEQ-3 and DEQ-7 models with equivalent parameter counts as their fully-explicit counterparts. We use `LBEN to indicate that the IBP-MonDEQ layer uses the LBEN parameterization in Theorem 3.3. To solve for the fixed points, we use the forward-backward algorithm with Anderson acceleration (Walker & Ni, 2011; imp, 2020).
To guarantee that (3.6) has a unique fixed point, we enforce either (3.4) or (3.7) (depending on whether we use the LBEN parameterization) for the IBP-MonDEQ weight W . To enforce (3.4), we set W “ D´1{2MD´1{2 where M is the only trainable parameter and D “ diag ´
p|M |`|M |Jq1 2p1´mq
¯
is a fixed function of M , where diagp¨q maps a vector to a diagonal matrix. Here m P p0, 1q is a
tunable hyperparameter governing a tradeoff between expressivity and convergence rate: a smaller m leads to more expressivity but also slower convergence of the equilbrium solvers. For the LBEN parameterization (3.7), we parameterize the additional diagonal scaling matrix Γ P Dhˆh` by Γ “ diag ´
γ´1 γ sigmoidpβq ` 1 γ
¯
, where γ ą 1 is a scalar hyperparameter, and β P Rh is a trainable parameter β P Rh. This parameterization enforces that the condition number of Γ is bounded by γ.

heading: 4.1 CERTIFIED ROBUSTNESS RESULTS
text: Tables 2 shows certified and standard classification errors of 3 and 7 layer models trained with IBP on the MNIST and CIFAR10 datasets for various values of . For all settings, IBP-MonDEQ models are able to achieve lower mean certified errors than their fully explicit counterparts.
The improvement is particularly striking in the case of 3 layer models on MNIST, where IBPMonDEQ models perform much better, e.g. 9.87% better on MNIST for “ 0.4. We also find that using the more relaxed LBEN parameterization (Theorem 3.3) generally leads to better performance for 3 layer models, but the reverse trend may hold for larger 7 layer models. We hypothesize that the LBEN parameterization may lead to optimization difficulties in the IBP-MonDEQ layer when
there are other additional layers in the network. Investigating and improving the optimization of IBP-MonDEQ layers is an interesting direction for future work.
Implementation details. We train all models using IBP for 300 epochs using the Adam optimizer (Kingma & Ba, 2014) with a learning rate of 5e-4, and report errors at the 300th epoch of training averaged over 3 runs. We use a smooth warmup schedule for (Xu et al., 2020; Shi et al., 2021), interpolating between “ 0 and “ train, a target training lower bounded by test. Following Shi et al. (2021), we use batch normalization (BN) after every linear layer besides the last FC-10 layer. There is no BN within an IBP-MonDEQ layer, but BN is applied to outputs of the IBP-MonDEQ layers. For 3 layer models, we insert a 4x4 pooling layer before the FC-10 layer. We also use the IBP initialization proposed by (Shi et al., 2021) for all explicit layer weights, which prevents IBP bounds from exploding at initialization. Additional details are in Section B.

heading: 5 ADDITIONAL RELATED WORKS
text: Implicit layers. Various fundamental properties of DEQs have been investigated in the literature, most notably convergence to and existence of a fixed point (Winston & Kolter, 2020; Revay et al., 2020; Bai et al., 2021). Bai et al. (2021) propose empirical Jacobian regularization techniques for speeding up equilibrium solving in DEQs. Another studied property of DEQs is their Lipschitzness: Revay et al. (2020) and Pabbaraju et al. (2020) derive bounds on the Lipschitz constants of MonDEQs which are applicable in certified robustness settings. However, because the Lipschitz constants are tailored to the `2 norm, these works only consider `2 bounded adversaries. Chen et al. (2021) propose polynomial optimization programs for certifying robustness of MonDEQs, but their methods only succeed for `2 perturbations and do not work empirically against `8 adversaries. Kawaguchi (2021) theoretically analyze optimization of equilibrium models.
Other prominent classes of implicit models include neural ODEs (Chen et al., 2018; Dupont et al., 2019; Liu et al., 2019; Finlay et al., 2020), and convex optimization layers (Amos et al., 2017; Amos & Kolter, 2017; Agrawal et al., 2019). Neural ODE outputs are implicitly defined as the solution to some differential equation. Adversarial robustness is also an interesting topic of study for neural ODEs, which may be more robust than explicit models (Yan et al., 2019), though the cause of this might be gradient obfuscation (Huang et al., 2020).
Certified robustness. A common technique in certified robustness is to express a convex program which lower bounds the worst-case perturbed output of the network, either via semidefinite relaxations (Raghunathan et al., 2018a;b), or linear relaxations (Wong & Kolter, 2018; Wong et al., 2018; Dvijotham et al.; Zhang et al., 2018; Wang et al., 2018). One advantage of IBP compared to these approaches is its simplicity and efficiency, making it viable for training larger models (Gowal et al., 2018). Zhang et al. (2019) propose CROWN-IBP, which combines IBP with linear relaxation methods during warmup training. Xu et al. (2020) extend this approach to general computation graphs. Shi et al. (2021) propose methods for speeding up optimization of IBP-trained networks.
Another well-studied certified robustness approach is randomized smoothing (Li et al., 2018; Cohen et al., 2019; Lecuyer et al., 2019; Salman et al., 2019a; Yang et al., 2020), which can in theory produce probabilistic certificates of robustness for generic models (including, in theory, DEQs). However, these certificates are random, not deterministic, and have some error probability. In addition, randomized smoothing has theoretical limitations for certifying `8 robustness for high-dimensional data (Blum et al., 2020; Kumar et al., 2020; Yang et al., 2020).

heading: 6 CONCLUSION
text: This work aims to certify robustness of DEQ models. We propose the IBP-MonDEQ layer, a DEQ layer which solves two equilibrium equations: one for the unperturbed fixed-point output, and one for upper and lower interval bounds on adversarially perturbed values of the fixed point. Our mathematical analysis reveals how to parameterize the IBP-MonDEQ so that existence and uniqueness of a fixed point is guaranteed. One interesting interpretation of these results is that they characterize a class of infinitely deep, weight-tied neural nets for which IBP is stable. An interesting direction for future work is to explore whether other methods besides IBP for certifying robustness of explicit networks can also be adapted to work for DEQs.

heading: 7 ETHICS AND REPRODUCIBILITY STATEMENTS
text: We do not expect ethical concerns to arise from this research because DEQ methods are still exploratory in nature, and so the main impacts of this work are still mainly theoretical and algorithmic.
All proofs omitted from the main body of the paper are in Section A. Additional implementation details are provided in Section B, and code is submitted with the supplementary material.

heading: A MISSING PROOFS IN SECTION 3
text: We first fill in the proofs of Claim 3.5 and Lemma 3.4.
Proof of Claim 3.5. Let u “ „
s t

be any eigenvector of M , with eigenvalue λ. There are two cases:
Case 1: s ‰ ´t. As λ „
s t
 “Mu “ „ As`Bt Bs`At  , it follows that λs “ As`Bt and λt “ Bs`At.
Thus, it follows that pA ` Bqps ` tq “ As ` Bt ` Bs ` At “ λps ` tq. As the condition of this case assumed ps` tq ‰ 0, λ is an eigenvalue of A`B.
Case 2: s “ ´t. Then λ „
s ´s
 “Mu “ „ pA´Bqs ´pA´Bqs  . It follows that λs “ pA´Bqs, so λ is an
eigenvalue of A´B.
Using Claim 3.5, we can complete the proof of Lemma 3.4.
Proof of Lemma 3.4. Define A fi pW q``pW q J ` 2 and B fi pW q´`pW qJ´ 2 , so xW “ „ A B B A  . We note that A ` B “ ppW q``pW q´q`ppW q``pW q´q J
2 “ W`WJ 2 and likewise A ´ B “ |W |`|W |J
2 . We now directly apply Claim 3.5 to conclude that eigenvalues of xW are either eigenvalues of A`B or A´B, as desired.
To see the left-to-right implication of (3.8), we use the fact that the set of eigenvalues of xW `xWJ contains those of |W | ` |W |J as a subset. For the right-to-left implication, we note that I ´ |W | ą 0 implies that λmaxpp|W | ` |W |Jq{2q ă 1. Next, we can observe that λmaxp|W | ` |W |Jq “ λmaxpxW `xWJq because eigenvalues of xW `xWJ are either eigenvalues ofW `WJ or eigenvalues of |W |` |W |J. Now we can use the fact that λmaxpW `WJq ď λmaxp|W |` |W |Jq, which would give us λmaxppxW `xWJq{2q ă 1, or I ´xW ą 0. Finally, to see that λmaxpW `WJq ď λmaxp|W | ` |W |Jq, let v be the eigenvector corresponding to the maximum eigenvalue ofW `WJ. The key observation is that vJpW `WJqv ď |v|Jp|W |` |W |Jq|v| because terms in the expansion of the first quantity will be replaced by positive versions with the same magnitude in the r.h.s.
Next, we complete the proof of Proposition 3.2.
Proof of Proposition 3.2. By results of Winston & Kolter (2020), there exists 0 ă α ď 1 such that the damped iteration
„
suk uk
 “ p1´ αq „
szk´1 zk´1
 ` α ˆ xW „
szk´1 zk´1
 ` „
sv v
˙
„
szk zk
 “ σ ˆ„
suk uk
˙ (A.1)
is guaranteed to converge for any initial sz0, z0: limkÑ8 szk, zk “ sz‹, z‹. For any v satisfying v ď v ď sv, we consider iterating (A.1) with sz0 “ z0 “ z‹pvq. We claim that the following invariant holds: szk ě z‹pvq ě zk @k ě 0. To see this, we also consider the damped iteration for z‹pvq, noting that the following equality holds by (Winston & Kolter, 2020):
u‹ “ p1´ αqz‹pvq ` αpWz‹pvq ` vq z‹pvq “ σpu‹q (A.2)
Now we apply induction on k. The base case k “ 0 given by our choice of sz0, z0. We compare corresponding terms in (A.1) and (A.2) for computing su, u, and u‹. We note that szk´1 ě z‹pvq by the inductive hypothesis, ˆ xW „
szk´1 zk´1
˙
0:h
ě z‹pvq by the inductive hypothesis and properties of
the IBP iteration, and sv ě v by assumption. Thus, it follows that suk ě u‹, and likewise, uk ď u‹. Since σ is nondecreasing, we obtain szk ě z‹pvq ě zk, completing the induction. Taking limits as k Ñ8, we obtain sz‹ ě z‹pvq ě z‹, as desired.
Next, we complete the proof of Theorem 3.3. The following lemma will be useful. Lemma A.1. In the setting of Theorem 3.3, suppose that W satisfies Λ ´ ΛW ą 0 for some Λ P Dhˆh` . Then there exists 0 ă α ď 1 such that the following iteration converges:
zk “ σppI ´ αΛqzk´1 ` αΛpWzk´1 ` vqq (A.3)
with limkÑ8 zk “ z‹, where z‹ is the solution to the fixed point equation z‹ “ σpWz‹ ` vq.
Proof of Lemma A.1. We first observe that the linear operator I ´ αpΛ ´ ΛW q is contractive for sufficiently small α, as Λ ´ ΛW ą 0. Thus, since ReLU is 1-Lipschitz, the iteration in (A.3) contracts and therefore converges to a fixed point. To check that this gives the same fixed point as (3.3), we will check that the following holds:
z‹ “ σppI ´ αΛqz‹ ` αΛpWz‹ ` vqq (A.4)
Note that for coordinates i where pWz‹ ` vqi ą 0, the definition of z‹ implies z‹i “ pWz‹ ` vqi, so (A.4) is verified for such coordinates. Otherwise, for coordinates i where pWz‹ ` vqi ď 0, since σ is the ReLU activation, z‹i “ 0, so we can again verify (A.4) for these coordinates.
We now complete the proof of Theorem 3.3.
Proof of Theorem 3.3. First, we consider any W of the form (3.7). Taking Λ “ Γ´2, we have Λ ´ ΛW “ Γ´1pI ´ D´1{2MD´1{2qΓ´1. Now by invoking Theorem 3.1, we conclude that the middle term in this product is PD, so Λ´ ΛW ą 0.
To prove the reverse implication, we note that Λ ´ Λ|W | “ Λ1{2pI ´ Λ1{2|W |Λ´1{2qΛ1{2, so Λ ´ Λ|W | ą 0 ðñ I ´ Λ1{2|W |Λ´1{2 ą 0. By invoking Theorem 3.1, it follows that we have the parameterization Λ1{2WΛ´1{2 “ D1{2MD1{2, so setting Γ “ Λ´1{2 and rearranging gives the desired result.
Next, we check that (2.4) and (3.3) have guaranteed unique fixed points whenever W is parameterized as in (3.7). Using the observation derived above, we can check that
Λ´ Λ|W | ą 0 (A.5) ùñ I ´ Λ1{2|W |Λ´1{2 ą 0 (A.6) ùñ I ´ Λ1{2WΛ´1{2 ą 0 (A.7)
ùñ Λ´ ΛW ą 0 (A.8)
Thus, we can apply Theorem 1 of (Revay et al., 2020) to conclude the existence of a unique fixed point for (2.4). For (3.3), we apply Lemma 3.4 to conclude that pΛ´pΛxW ą 0, where pΛ fi „
Λ 0 0 Λ

P
R2hˆ2h. Thus, Theorem 1 of (Revay et al., 2020) can also be used to conclude that (3.3) has a unique fixed point.
Finally, it remains to check that sz‹ and z‹ are indeed valid interval bounds on z‹. The proof of Proposition 3.2 no longer directly applies because the damped iteration (A.1) might not converge, as we no longer have the guarantee I2hˆ2h ´xW ą 0. Instead, we invoke Lemma A.1, which states the existence of 0 ă α ď 1 such that the following iteration converges:
„
szk zk
 “ σ ˆ pI2hˆ2h ´ αpΛq „
szk´1 zk´1
 ` αpΛ ˆ xW „
szk´1 zk´1
 ` „
sv v
˙˙
(A.9)
with limkÑ8 szk “ sz‹, limkÑ8 zk “ z‹. Using this modified iteration but keeping other steps the same, we can follow Proposition 3.2 to complete the proof.
Next, we provide the proof of Proposition 3.7.
Proof of Proposition 3.7. We set B “
»
—
—
– A1 0 ¨ ¨ ¨ 0 0 0 ¨ ¨ ¨ 0 ... ... ...
... 0 0 ¨ ¨ ¨ 0
fi
ffi
ffi
fl
. According to (3.7), the weight matrix
W should take the following form: W “ ΓD´1{2MD´1{2Γ´1. We choose Γ to take the following form:
Γ “
»
—
—
– γ1Ihˆh 0 ¨ ¨ ¨ 0 0 γ2Ihˆh ¨ ¨ ¨ 0 ... ... ...
... 0 ¨ ¨ ¨ 0 γLIhˆh
fi
ffi
ffi
fl
(A.10)
M will take the following lower triangular block form:
M “
»
—
—
—
—
– 0 ¨ ¨ ¨ ¨ ¨ ¨ ¨ ¨ ¨ 0 A2 0 ¨ ¨ ¨ ¨ ¨ ¨ 0 0 A3 0 ¨ ¨ ¨ 0 ... ... ... ... ...
0 ¨ ¨ ¨ 0 AL 0
fi
ffi
ffi
ffi
ffi
fl
(A.11)
where if we split M into a grid of h ˆ h blocks, the block in the i-th row and i ´ 1-th column has value Ai, and all other blocks are 0. Finally, D will take the form:
D “
»
—
—
– β1Ihˆh 0 ¨ ¨ ¨ 0 0 β2Ihˆh ¨ ¨ ¨ 0 ... ... ...
... 0 ¨ ¨ ¨ 0 βLIhˆh
fi
ffi
ffi
fl
(A.12)
In order to satisfy the constraints of (3.7), we require β1 ą maxjPrhs p|A|J2 1qj
2 , βL ą maxjPrhs p|A|L1qj 2 , and βi ą maxjPrhs pp|A|i`|A|Ji`1q1qj 2 for 2 ď i ď L ´ 1. We now observe that W is of the form
W “
»
—
—
—
—
—
—
–
0 ¨ ¨ ¨ ¨ ¨ ¨ ¨ ¨ ¨ 0 γ2β ´1{2 2 A2β ´1{2 1 γ ´1 1 0 ¨ ¨ ¨ ¨ ¨ ¨ 0
0 γ3β ´1{2 3 A3β ´1{2 2 γ ´1 2 0 ¨ ¨ ¨ 0 ... ... ... ...
... 0 ¨ ¨ ¨ 0 γLβ´1{2L ALβ ´1{2 L´1 γ ´1 L´1 0
fi
ffi
ffi
ffi
ffi
ffi
ffi
fl
(A.13)
We observe now that we have L degrees of freedom in choosing γ, so we can choose γ such that γiβ ´1{2 i β ´1{2 i´1 γ ´1 i´1 “ 1 @2 ď i ď L, as this only imposes L ´ 1 constraints. For example, we can set γ1 “ 1, and set γ2, . . . , γL in sequence so that the desired equalities hold. This gives W “ M . Finally, it is straightforward to see that the equilibrium for this constructed W and B concatenates all of the hidden layers of the network, so the desired equivalence between the DEQ and explicit network holds.

heading: B ADDITIONAL IMPLEMENTATION DETAILS
text: Implementation details for Section 4. For all models, we use a batch size of 128 and anneal the learning rate, which is initially 5e-4, by a factor of 0.2 at the 120th and 280th epochs. We use gradient clipping with a max `2 norm of 10. To preprocess the data, all inputs are normalized to the range r0, 1s before we subtract the mean and divide by the standard deviation of the training images across each input channel. Note that the adversarial perturbations are applied to the r0, 1snormalized image before subtracting the mean and dividing by the standard deviation. For MNIST, we do not use data augmentation, and for CIFAR10 we use random crops and horizontal flips. We note that during both training and testing, when computing IBP bounds we elide the last FC-10
transformation with the output margins of the model (which can be expressed as a linear function of the logits), as Gowal et al. (2018) show that this leads to performance benefits.
For CIFAR10, we choose train “ test, whereas for MNIST we use a larger value of train, following Gowal et al. (2018) and Shi et al. (2021). The values are displayed in Table 3. To schedule , we set “ 0 for the first epoch of training, and afterwards we smoothly increase following Xu et al. (2020). The schedule interpolates between “ 0 and “ train in a smooth manner: for the first 1 4 of the ramp-up iterations, increases according to a degree 4 monomial. After this, increases linearly until it reaches a final value of train. The linear slope and coefficient of the monomial are chosen so that the derivative of is continuous. For all experiments, we use 79 ramp-up epochs.
All models besides the DEQ-3 can be trained within a day on a single NVIDIA TitanXp GPU. The DEQ-3 can take up to two days because the hidden layer size is larger (128 output channels), so each iteration of the equilibrium solver is more costly. In all, the training times of the IBP-MonDEQ models vary based on the current model weights but generally are 3-10 times longer than the fullyexplicit models. As it is already known that DEQ models tend to compare unfavorably to fully explicit models in terms of runtime (Bai et al., 2019; 2021), improving the runtime discrepancy is deferred to future work.
Finally, we provide additional IBP-MonDEQ-specific implementation details. For IBP-MonDEQ layers, we set m “ 0.1 in DEQ-3 models and m “ 0.5 in DEQ-7 models. We find that m “ 0.5 outperformsm “ 0.1 for DEQ-7 models despite the reduced expressivity, likely due to optimization difficulties. We set γ “ 3 when training models with the more relaxed LBEN parameterization. For DEQ-7 models, we also find it helpful for optimization to use a warmup schedule on the value of m matching the schedule on , and set mcurrent “ m ` p0.99 ´mqp1 ´ current train q so that the value of mcurrent interpolations between 0.99 and m ă 0.99 throughout training. The stopping criterion for the fixed-point solver is }zk`1´zk}2}zk`1}2 ď t, where t “1e-5 is the tolerance threshold, and zk denotes the k-th iterate of the fixed-point solving method. For models with the LBEN parameterization, we tie the trainable scaling parameter β across channels, so that β has the same shape as the convolutional bias parameter.
Details for Figure 2. The models trained in Figure 2 (left) are obtained by taking the 7LAYER model and adding additional CONV-128-3x3-1 layers to reach the desired depth. All other training details for IBP models are the same as above. For the the red curve (training on the standard clean loss), we also use the same implementation details except “ 0 throughout training and testing. For Figure 2 (right), the bounds are computed for randomly initialized models. We obtain the bounds by attempting to solve (3.3) for DEQ models where W corresponds to a fully-connected layer with output dimension 128. We obtain these bounds on MNIST with “ 0.1 and average the mean of szk ´ zk for each k over the entire MNIST test set. We use the damped forward-backward algorithm as the equilibrium solver with damping factor α “ 0.1 (see (A.1)). We note that the standard equilibrium iteration (2.4) converges for both MonDEQ and IBP-MonDEQ models, whereas (3.3) fails to converge for MonDEQ models only.

Review summaries:
The paper presents a new class of neural networks called IBP-MonDEQs that are an extension of the recently introduced implicit networks MonDEQs. The authors identify a class of weight matrices of the network that ensures that fixed point of the implicit layers exist with respect to the interval analysis and is unique. The construction of IBP_MonDEQ is motivated by the goal of obtaining networks that can be certified to be robust. The authors then train such networks comparing against explicit networks of the same architecture constructed using the certified IBP training. The results show that IBP-MonDEQs can obtain better certified robustness than explicit networks on the MNIST and CIFAR10 dataset.

The authors propose a deep equilibrium (DEQ) layer that provides certifiable robustness via the interval bound propagation technique. This involves augmenting the original fixed point condition considered in DEQs with two additional fixed point conditions, one for each bound. The main contribution is a theoretical result that says that when parameterised in a certain way, this IBP-DEQ admits a unique fixed point (Theorem 3.1, 3.3), and also that the model provides valid IPB (Proposition 3.2). Motivated by a theoretical result (Proposition 3,7), the authors show empirically that such restrictions imposed by the specific DEQ and parameterisation achieve comparable or improved performance compared with explicit models on MNIST and CIFAR10.