Efficient Neural Network Robustness Certification with General Activation Functions

1 Introduction

• Robustness certification seeks the largest neighborhood around an input with an unchanged prediction, but finding minimum adversarial distortion for ReLU networks is NP-complete.Formal verification methods such as Reluplex are computationally demanding even for small networks and face scalability issues.Source: §1 · p. 2
• Prior methods exploit ReLU's piecewise linearity to compute non-trivial certified lower bounds, while certification for nonlinear activations remained largely unexplored.Adversarial perturbations motivate this problem because they can alter predictions in white-box, black-box, and physical settings [2] [12] [13] [14].Source: §1 · pp. 1–2
• CROWN improves certified lower bounds by up to 26% compared to.For a network with over 10,000 neurons, it gives a certified lower bound in about 1 minute on 1 CPU core.Source: §1 · p. 2
• CROWN certifies networks with general activations using linear or quadratic upper and lower bounds, with adaptive bound selection to reduce approximation errors.The framework targets activations beyond piecewise-linear ReLU, including tanh and sigmoid.Source: §1 · p. 2

2 Background and Related Work

• Exact ReLU certification uses MILP [21] [23], SMT (Reluplex [24]) or SAT (Planet), but NP-completeness limits these methods to very small networks.Reluplex can take several hours to find minimum distortion for a network with 5 inputs, 5 outputs, and 300 neurons.Source: §2 · p. 2
• Operator-norm and Jacobian bounds [3, 17] can be loose; local-Lipschitz work excludes ReLU and is hard to extend beyond two layers, while CLEVER is not certified.[26] requires continuously differentiable activations; soft-plus is demonstrated in.Source: §2 · pp. 2–3
• For ReLU networks, relaxes MILP to LP, uses SDP but is limited to one hidden layer, offers Fast-Lin/Fast-Lip certified bounds, and uses zonotopes.Fast-Lin and Fast-Lip exploit ReLU properties and achieve state-of-the-art performance.Source: §2 · p. 2
• CROWN addresses demand for efficient certified bounds with general activations, including those needed in RNNs and LSTMs; also handles general activations but trades bound quality against scalability.The paper states that CROWN performs efficient robustness certification for networks with general activation functions.Source: §2 · p. 2
• Empirical defenses are outside provable certification, while Wasserstein-based distributional certification differs from this paper’s local ℓp-ball robustness model.Source: §2 · p. 3

3.1 General framework

• Neuron-specific linear upper and lower activation bounds are propagated backward through the network to produce explicit output bounds.Taking global bounds over the perturbed input ball yields certified bounds that can be used to search for minimum adversarial distortion.Source: §3.1 · pp. 3–4
• CROWN adaptively selects linear approximations when computing certified lower bounds on minimum adversarial distortion; for an m-layer ReLU network with n neurons per layer and n outputs, its time complexity is O(m^2n^3).It computes analytic output bounds efficiently without optimization solvers for general ℓp distortion.Source: §3.1 · pp. 4–5

3.2 Case studies: CROWN for ReLU, tanh, sigmoid and arctan activations

• CROWN constructs bounds for ReLU, tanh, sigmoid, and arctan, and can incorporate other activations such as leaky ReLU, ELU, and softplus.For tanh, sigmoid, and arctan, the method uses their convexity on one side and concavity on the other; for ReLU, it adaptively selects a lower-bound slope to tighten certification.Source: §3.2 · p. 6

3.3 Extension to quadratic bounds

• CROWN extends its activation bounds with quadratic terms, choosing bounds that make the global-bound problem convex and solvable with projected gradient descent.Without this choice, the quadratic form can be indefinite and the optimization non-convex.Source: §3.3 · p. 7

Methods

• The experiments compare adaptive linear bounds, quadratic bounds, Fast-Lin, Fast-Lip, Reluplex, and LP-Full for ReLU networks, and CROWN-general for other activations.Reluplex can solve the exact minimum distortion but is feasible only for very small networks; LP-Full solves each neuron’s LP exactly to obtain the best possible bound.Source: §4 · p. 7

Model and Dataset

• The evaluation uses MLPs trained on MNIST and CIFAR-10, including the same 100 random test images and attack targets as prior ReLU evaluations.For non-ReLU activations, the authors tune learning rate and weight decay to obtain accuracy similar to ReLU models.Source: §4 · p. 7

Results on Small Networks

• On small networks, CROWN-Quad for 2-layer models and CROWN-Ada achieve the largest lower bounds, while Reluplex and LP-Full are orders of magnitude slower.Reluplex also reveals the gap between certified lower bounds and the true minimum adversarial distortion; CROWN-Ada's improvements over Fast-Lin become more significant on larger networks.Source: Figure 2 · p. 8, §4 · p. 8

Results on Large ReLU Networks

• CROWN-Ada significantly outperforms Fast-Lin and Fast-Lip on large ReLU networks, with computation time increasing by less than 2X over Fast-Lin.Its computation time is comparable with Fast-Lip.Source: Table 4 · p. 8, §4 · p. 8

Results on Different Activations

• CROWN-general efficiently certifies non-trivial lower bounds for four activation functions, with about 20% additional computation time versus CROWN-Ada on ReLU networks.CIFAR models with sigmoid activations are excluded because their accuracy is much worse than that of the other networks.Source: §4 · p. 8, Table 5 · p. 8

• CROWN outperforms state-of-the-art baselines on ReLU networks and efficiently certifies non-trivial lower bounds for networks with over 10K neurons and different activation functions.Source: §5 · p. 8

Upper bound

• Upper-bound derivation selects the appropriate inequality side for each term according to the sign of its associated weight.The proof identifies the nonnegative-weight and other cases, then uses the corresponding key equations to bound the terms.Source: A Proof of Theorem 3.2 · p. 11
• At each rewrite, constant terms are collected and coefficients are combined into equivalent weights and biases, preserving the form needed for another iteration.The derivation also swaps the summation order before combining coefficients.Source: A Proof of Theorem 3.2 · p. 12
• Repeating the rewrite yields a final upper bound at the first layer, which the proof then uses as the bound for the output.The procedure is repeated until f^U,1_j(x) is obtained.Source: A Proof of Theorem 3.2 · p. 12

Lower bound

• The lower-bound proof follows the same iterative procedure but uses the left-hand sides of the bounding inequalities instead of their right-hand sides.This produces a final lower bound f^L,1_j(x).Source: A Proof of Theorem 3.2 · p. 13

Global upper bound

• Theorem 3.2 provides lower and upper bounds for the network output throughout the input ball.The proof's stated goal is to bound the m-th layer output f_j(x) for every x in B_p(x_0, ε).Source: B Proof of Corollary 3.3 · p. 13
• The proof normalizes the perturbation into B_p(0, 1) and applies ℓ_p–ℓ_q duality when moving from equation (19) to (20).It invokes Definition B.1 and the fact that the ℓ_q norm is dual to the ℓ_p norm for p, q ∈ [1, ∞].Source: B Proof of Corollary 3.3 · pp. 13–14

C Illustration of linear upper and lower bounds on sigmoid activation function.

• Figure 3 illustrates linear upper and lower bounds for the sigmoid activation σ(y).Source: Figure 3 · p. 14
• For quadratic approximations, the upper-bound derivation keeps equations (7) and (8) but replaces h(k) with quadratic functions.Source: C Illustration of linear upper and… · p. 14
• The lower-bound derivation follows the upper-bound derivation by swapping h(k)_L,r and obtaining f^L_j(x).Source: C Illustration of linear upper and… · p. 15

E.1 Results on CROWN-Ada

• CROWN-Ada improves certified lower bounds over Fast-Lin by up to 28%, especially for larger and deeper ReLU networks.Table 6 compares the proposed adaptive lower bounds with Fast-Lin, Fast-Lip, and Op-norm.Source: Table 6 · p. 16
• The comparisons consider runner-up, random, and least-likely target classes for each norm.The runner-up class has the second-largest probability.Source: Table 6 · p. 16
• LP-full and Reluplex could not finish within a reasonable time for all reported networks.Source: Table 6 · p. 16
• Op-norm computes each layer's operator norm and uses the product of those norms as a global Lipschitz constant to derive a robustness lower bound.For p = 2, the operator norm is the spectral norm.Source: Table 6 · p. 16
• CLEVER provides an estimated robustness lower bound, while CW and EAD attacks provide upper bounds on minimum adversarial distortion.The cited attack methods are CW [6] and EAD [32].Source: Table 6 · p. 16
• Table 6 compares CROWN-Ada against Fast-Lin, Fast-Lip, and Op-norm alongside LP-full, Reluplex, CLEVER, and attack-based bounds.Source: Table 6 · p. 16

E.2 Results on CROWN-general

• Table 7 compares certified lower bounds from CROWN-Ada on ReLU networks and CROWN-general on tanh, sigmoid, and arctan networks.The caption does not provide the table’s cell values, so it does not establish which method or activation achieves higher bounds.Source: Table 7 · p. 17
• CIFAR models with sigmoid activations are excluded because their accuracy is much worse than that of the other networks.Source: Table 7 · p. 17
• For each norm, robustness is evaluated against the runner-up, a random, and the least likely targeted attack classes.Source: Table 7 · p. 17