15. Verification & Distribution-Free Guarantees
Bound propagation (IBP, CROWN, α,β-CROWN), SDP relaxations, randomized smoothing, conformal prediction and the scenario approach
This module assumes:
- Neural-network layers, activations and backpropagation (Primer E)
- Norms, norm balls and dual-norm bounds (Primer A)
- Convex sets, convex functions and relaxations (Primer B)
- Lagrangian bounds, strong duality and supergradient ascent (Module 2)
- Positive semidefinite matrices, LMIs and SDPs (Module 2)
- Quadratic certificates and the S-procedure (Module 2)
- Gaussian distributions, projections and quantiles (Primer C)
- Binomial confidence intervals and exchangeability (Primer C)
- Confidence statements and union bounds (Primer C)
- MPC, open-loop planning and recursive feasibility (Primer D)
Book contents · Apply this chapter to a real decision · Glossary
On a first pass, follow the links below and solve the Easy set before opening the research exercises. Try each question on paper; open its hint only when stuck, then compare your reasoning with the worked solution. Use Medium questions to connect the algebra and Hard questions to check the assumptions.
§1: objective and counterexamples · §2: intervals and signed lines · §4: the smoothed classifier · §5: coverage and exchangeability · §6: design versus validation
Practice: 4 Easy · 4 Medium · 4 Hard · original research exercises. Check readiness or use the course study guide.
Two inequalities to keep separate
For deterministic verification, $p^\star$ is the true largest violation and $\bar p\ge p^\star$ is a computed upper bound. If $\bar p\le0$, every allowed input is safe for that specification. If $\bar p\gt0$, the answer is undecided until an actual violating input or a tighter proof is found. For example $p^\star=-1$ and $\bar p=2$ can both be correct.
For a probabilistic certificate, write down the random experiment as well as the number. Smoothing uses random draws to certify the ideal smoothed classifier; conformal coverage averages over calibration and a new example; scenario confidence is over the samples used to choose a design. A $95\%$ number has different meanings in these three sentences. Refresh conditional and marginal probability and confidence events and union bounds before comparing them.
Modules 12–14 built certificates into a network: a Lipschitz bound from an SDP, a 1-Lipschitz layer by construction, a closed-loop stability LMI. This module asks the complementary question: given a network somebody else trained, or a learned predictor inside a controller, what can we certify after the fact, and with what kind of guarantee? The first half (Sections 1–3) is deterministic: worst-case bounds over an input set, computed by interval arithmetic, linear relaxations, branch-and-bound or semidefinite programming (see Primer A). The second half (Sections 4–6) is distribution-free and probabilistic: randomized smoothing, conformal prediction and the scenario approach certify statements of the form “with probability at least $1-\delta$” (see Primer C: probability and Primer C: confidence) without assuming anything about the network or the data distribution beyond sampling. Section 7 puts the two families side by side, because in a safety argument it matters enormously which kind of statement one is making.
1. The Verification Problem
Take a feed-forward network with $m$ layers (see Primer E), written as pre-activations and activations,
with $\phi$ applied elementwise (ReLU unless stated otherwise). A specification is a property that must hold for every input in a set $\mathcal X$, typically an $\ell_p$ ball $\mathcal B_p(x_0,\varepsilon)=\{x:\|x-x_0\|_p\le\varepsilon\}$ around a nominal input (Primer A). Almost every property studied in this literature is linear in the output:
This is the formulation of Gowal et al., ICCV 2019 (their eqs. 2–4); the β-CROWN papers write the same problem as a minimisation, $\min_{x\in\mathcal X} f(x) \ge 0$ with a scalar “margin output” $f$. We will switch between the two freely: an upper bound on $\max c^{\top}f$ is a lower bound on $\min(-c^{\top}f)$.
Why it is hard. The maximisation is over a piecewise-affine function with up to $2^{N}$ feasible activation patterns ($N$ = number of ReLUs), and it is not convex (see Primer B). Katz et al., CAV 2017 prove (appendix, Section I) that deciding satisfiability of a conjunction of linear constraints on the inputs and outputs of a ReLU network is NP-complete: membership in NP uses a polynomial-bit rational witness for a feasible activation pattern, checked by a forward pass, and it is NP-hard by a reduction from 3-SAT (Sälzer & Lange, RP 2021, who repair flaws in both the membership and the hardness proof and show hardness already for one-layer networks). That is the counterexample question. The verification question of the definition above, whether the property holds for every $x\in\mathcal X$, is its complement, so for rationally encoded networks and polyhedral specifications it is coNP-complete. Computing the exact Lipschitz constant, the other route to robustness certificates (Module 12), is likewise NP-hard already for two-layer ReLU networks (Virmaux & Scaman, NeurIPS 2018). Thus, unless P = NP, no general polynomial-time exact verifier exists; practical complete methods may explore exponentially many patterns, while incomplete relaxations accept conservatism, and the modern answer is to combine both.
A decision problem asks a yes/no question about an input written with finitely many bits (here: rational weights, biases and constraint coefficients); running times are measured in that bit length. P contains the problems solvable in polynomial time. NP contains those whose yes-instances have a witness of polynomial bit length that can be checked in polynomial time. A polynomial reduction maps every instance of one problem to an equivalent instance of another with polynomial work; a problem is NP-hard if every NP problem reduces to it, and NP-complete if it is moreover in NP. coNP contains the complements of NP problems: "does the property hold for all inputs?" is in coNP because a counterexample is a checkable witness for "no".
For ReLU satisfiability the witness cannot simply be "an input", since a real input may need arbitrarily many digits. Instead guess an activation pattern: the remaining constraints are linear with rational data, a feasible linear system has a solution of polynomial bit length, and a forward pass checks it. Hardness is conditional: unless P = NP, no algorithm solves all instances in polynomial time. NP-hardness is not itself a proof that exponential time is needed.
Complete verifiers: Reluplex, Marabou and branch-and-bound
Vocabulary first. A satisfiability query asks whether all listed constraints can hold at once: SAT comes with a satisfying assignment (here a counterexample input), UNSAT means none exists. SMT (satisfiability modulo theories) combines Boolean case choices with constraints from a theory such as linear arithmetic. The simplex method keeps a system of linear equations with variable bounds; a pivot changes which variables are solved for in terms of the others. Abstract interpretation propagates simple sets that enclose the exact sets.
Reluplex extends the simplex method. Each ReLU becomes a pair of variables $(x^b, x^f)$ with $x^f = \max(0,x^b)$; ordinary simplex pivots repair bound violations, dedicated rules (Update$_b$, Update$_f$, PivotForRelu) repair “broken” ReLU pairs, and only when repairs keep failing does ReluSplit branch on the two cases $\{x^b\le 0, x^f=0\}$ and $\{x^b\ge 0, x^f=x^b\}$. The query is “does there exist $x\in\mathcal X$ with $f(x)\in\mathcal Y_{\rm bad}$?”: SAT returns a counterexample, UNSAT proves the property. It verified the ACAS Xu collision-avoidance networks, an order of magnitude larger than anything verified before (Katz et al., CAV 2017). Its successor Marabou re-implements the Reluplex procedure; the current version, Marabou 2.0 (Wu et al., CAV 2024), adds DeepPoly/CROWN-style abstract interpretation for bound tightening, more activation functions and proof production (checkable certificates for UNSAT answers); full conflict-driven clause learning is described there as ongoing work.
Abstract interpretation is sound. If $S_0\subseteq\widehat S_0$ and each layer map $F_k$ has an abstract transformer $T_k$ with $F_k(S)\subseteq T_k(\widehat S)$ whenever $S\subseteq\widehat S$, induction gives $F_{k-1}\circ\cdots\circ F_0(S_0)\subseteq\widehat S_k$ with $\widehat S_{k+1}:=T_k(\widehat S_k)$. If the final enclosure misses the unsafe set, the property holds on all of $S_0$. Example: for $x\in[-1,1]$ the interval $[-2,2]$ encloses $2x$; enlarging sets costs precision, never soundness.
Checked proofs. A proof-producing UNSAT answer (Marabou 2.0) is trustworthy once an independent checker re-verifies every case split, every derived bound and the contradiction at every leaf, instead of trusting the solver's status.
Branch and bound (BaB) is the organising principle of every current top verifier: split the domain on an unstable neuron (one whose pre-activation can take both signs on $\mathcal X$) into $\{z_j \ge 0\}$ and $\{z_j \le 0\}$, bound each sub-domain with a cheap incomplete verifier, and recurse only where the bound fails. Completeness follows once all unstable neurons are split, because then the network is affine on every sub-domain and the split constraints are linear in $x$, so each leaf is a convex problem solved to optimality: an LP over a polytope when $\mathcal X$ is polyhedral (a box, an $\ell_\infty$ or an $\ell_1$ ball), a second-order-cone program for an $\ell_2$ ball (Wang et al., NeurIPS 2021, Theorem 3.3, proved for an $\ell_\infty$ box). Sections 2 and 8 make this concrete.
A second-order-cone program (SOCP) minimises a linear objective subject to linear constraints and constraints of the form $\|Ax+b\|_2\le e^\top x+e_0$ (an affine right-hand side); it is convex and solved to high accuracy by interior-point methods, which we use as a black box. At a fully split leaf the objective and the phase constraints are affine, and the remaining condition $\|x-x_0\|_2\le\varepsilon$ is exactly such a norm constraint ($A=I$, $b=-x_0$, constant right-hand side $\varepsilon$). Example: minimising $x_1$ over $\|x\|_2\le1$ gives $-1$ at $x=(-1,0)$.
2. Bound Propagation: IBP, CROWN, α,β-CROWN
2.1 Interval bound propagation
The cheapest sound bound is interval arithmetic: keep an axis-aligned box $[\underline z^{(k)},\overline z^{(k)}]$ around every layer. For the input, $\underline z^{(0)}=x_0-\varepsilon\mathbf 1$, $\overline z^{(0)} = x_0+\varepsilon\mathbf 1$ (an $\ell_\infty$ ball is a box). The affine layer is the only step that needs an argument.
Let $a\in[\underline a,\overline a]$ (coordinatewise) and $z = Wa + b$. Write the box in centre–radius form, $\mu = \tfrac12(\overline a+\underline a)$, $r = \tfrac12(\overline a - \underline a)$, so that $a = \mu+\delta$ with $|\delta_j|\le r_j$ for every $j$. Then for row $i$,
where the first inequality is the triangle inequality and the second uses $|\delta_j|\le r_j$; $|W|$ is the elementwise absolute value. Both inequalities are equalities for $\delta_j = r_j\,\mathrm{sign}(W_{ij})$, which is a feasible corner of the box, so the resulting interval is tight per coordinate:
This is eq. (6) of Gowal et al.: two matrix products per layer. For a monotone activation the box simply maps through, $[\phi(\underline z),\phi(\overline z)]$ (their eq. 7). The looseness is joint, not per coordinate: the true image of the box is the zonotope $W\mu+b+\sum_j[-r_j,r_j]\,W_{:,j}$, a sum of line segments along the columns of $W$ (a parallelotope when these generators are linearly independent), and IBP keeps only its bounding box. Example: $(a_1,a_2)\mapsto(a_1+a_2,\ a_1-a_2)$ maps $[-1,1]^2$ to the diamond with vertices $(\pm2,0)$, $(0,\pm2)$, whose bounding box $[-2,2]^2$ also contains the unreachable corner $(2,2)$. The corner that maximises $z_1$ is generally not the corner that maximises $z_2$, but the next layer is allowed to combine them as if it were. Every subsequent layer compounds this, which is why plain IBP bounds explode with depth on ordinary networks.
Two practical refinements from the same paper: (i) elision of the last layer, i.e. fold the specification into the last affine map, $c' = W^{(m)\top}c$, $d' = c^{\top}b^{(m)}+d$, and bound $\max c'^{\top}a^{(m-1)}+d'$ over the penultimate box, which skips one relaxation (their eq. 9): since $c^\top(W^{(m)}a+b^{(m)})+d=(W^{(m)\top}c)^\top a+c^\top b^{(m)}+d$ is a single affine function of $a=a^{(m-1)}$, it can be bounded directly, instead of bounding each output separately and combining extrema that need not occur at the same input; (ii) IBP training: form the worst-case logits $\hat z_{K,y}=\overline z_{K,y}$ for $y\ne y_{\rm true}$ and $\hat z_{K,y_{\rm true}}=\underline z_{K,y_{\rm true}}$ ($K=m$ is the output layer) and minimise $\kappa\,\ell(z_K,y_{\rm true})+(1-\kappa)\,\ell(\hat z_K(\varepsilon),y_{\rm true})$, with $\ell$ a classification loss such as the cross-entropy $\ell(z,y)=\log\sum_je^{z_j}-z_y$ (Primer E), $\kappa$ annealed (changed gradually during training) from $1$ to $\tfrac12$ and $\varepsilon$ ramped from $0$ to a training radius $\varepsilon_{\rm train}$ (the paper finds that $\varepsilon_{\rm train}$ larger than the test radius generalises better). A network trained this way makes its own IBP bounds tight, which is the surprising message of the paper: the loose relaxation becomes a good one when the weights are chosen for it.
2.2 CROWN: linear relaxation of the activation and backward substitution
CROWN (Zhang et al., NeurIPS 2018) replaces the box at each neuron by a pair of linear functions and keeps the linear dependence on $x$ all the way back to the input. The construction needs, for every neuron $r$ of layer $k$, pre-activation bounds $l_r\le z_r\le u_r$ (obtained from IBP, or recursively from CROWN itself).
- stable active, $0\le l_r$: $h_L=h_U=z$ (no relaxation);
- stable inactive, $u_r\le 0$: $h_L=h_U=0$;
- unstable, $l_r \lt 0 \lt u_r$: the upper bound is the chord $h_U(z)=\dfrac{u_r}{u_r-l_r}(z-l_r)$ and the lower bound is any line through the origin, $h_L(z)=\alpha z$ with $\alpha\in[0,1]$.
Caveat. tanh, sigmoid and arctan are convex on one side of $0$ and concave on the other, so for $l\lt0\lt u$ neither rule covers the whole interval. A candidate line $h$ is then checked directly: the extrema of $\phi-h$ on $[l,u]$ occur at $l$, at $u$, or where $\phi'(z)=h'(z)$, and $h$ is a valid lower (upper) bound exactly when the minimum (maximum) of $\phi-h$ is $\ge0$ ($\le0$).
Suppose $0\le a\le2$. For the output $f=1-3a$, the upper bound is $1-3(0)=1$ and the lower bound is $1-3(2)=-5$. A negative output weight therefore needs the lower activation bound to form an upper output bound, and vice versa. CROWN repeats this familiar inequality rule using affine lines instead of constants.
Keep the desired side written down during each substitution. After obtaining one affine expression in the original input, maximize or minimize that expression over the specified input set using the appropriate dual norm. The Medium signed-line problem and Hard norm-ball problem practice those two steps.
With the relaxations in hand, CROWN back-substitutes. The rule that makes it work is the one every student has seen in inequality manipulation: multiplying an inequality by a negative number flips it. We derive the one-hidden-layer case in full (the walkthrough in Section 8 evaluates it numerically); Theorem 3.2 of Zhang et al. is the same argument iterated over layers.
Let $f_j(x)=\sum_{i} W^{(2)}_{ji}\,\phi(z_i) + b^{(2)}_j$ with $z_i = W^{(1)}_{i,:}x + b^{(1)}_i$, and suppose valid linear bounds $h_{L,i}\le\phi\le h_{U,i}$ are known on $[l_i,u_i]$ (obtained from IBP on the first layer). We want a lower bound on $f_j$.
Step 1 (choose the side by the sign of the weight). For each $i$: if $W^{(2)}_{ji}\ge 0$ then $W^{(2)}_{ji}\phi(z_i)\ge W^{(2)}_{ji}h_{L,i}(z_i)$; if $W^{(2)}_{ji}\lt 0$ then $W^{(2)}_{ji}\phi(z_i)\ge W^{(2)}_{ji}h_{U,i}(z_i)$ (the inequality flips, so the upper line is needed for a lower bound). Summing,
This is exactly the matrix $\omega^{(1)}$ / $\Theta^{(1)}$ selection in Zhang et al.’s Theorem 3.2, specialised to $m=2$.
Step 2 (substitute the affine pre-activation). Since $z_i$ is affine in $x$, the right-hand side is affine in $x$:
For deeper networks one now treats $\Omega_{j,:}$ as the “equivalent weight” of the next layer down, chooses the side of each relaxation by the sign of its entries, and repeats: that is the backward pass.
Step 3 (concretise over the ball with Hölder). Write $x = x_0+\delta$, $\|\delta\|_p\le\varepsilon$. Then $\Omega_{j,:}x = \Omega_{j,:}x_0 + \Omega_{j,:}\delta \ge \Omega_{j,:}x_0 - \|\Omega_{j,:}\|_q\|\delta\|_p \ge \Omega_{j,:}x_0-\varepsilon\|\Omega_{j,:}\|_q$ with $1/p+1/q=1$ (Hölder's inequality, Primer A), and the bound is attained. With $v=\Omega_{j,:}\ne0$: for $p=\infty$ take $\delta=-\varepsilon\,\mathrm{sign}(v)$; for $p=2$, $\delta=-\varepsilon v/\|v\|_2$; for $p=1$, put the whole radius, with the opposite sign, on a coordinate of largest $|v_i|$; for $1\lt p\lt\infty$, $\delta_i=-\varepsilon\,\mathrm{sign}(v_i)|v_i|^{q-1}/\|v\|_q^{q-1}$, which has $\|\delta\|_p=\varepsilon$ because $(q-1)p=q$, and gives $v^\top\delta=-\varepsilon\|v\|_q$. (If $v=0$ every $\delta$ is optimal.) Hence (Corollary 3.3 of Zhang et al.)
and symmetrically $\gamma_j^U = \Lambda_{j,:}x_0+\varepsilon\|\Lambda_{j,:}\|_q + \dots$ with the sides swapped. The minimum of the linear lower bound over the ball is a closed-form expression; no LP is solved. A certified radius is obtained by bisection on $\varepsilon$ (Primer B): keep a certified radius and a larger uncertified one, test the midpoint, and keep the half that still separates the two. Every accepted radius is valid, but a failed test only means that this verifier did not certify it, and with approximately optimised relaxations success need not even be monotone in $\varepsilon$, so bisection finds a certified radius, not necessarily the largest one the method could certify. (Zhang et al. bound the logits separately and require $\gamma^L_c-\gamma^U_t\gt 0$; bounding the margin $c^{\top}f$ directly, as in Section 1, is tighter.)
Why intermediate bounds matter. The relaxation at layer $k$ depends on $[l^{(k)},u^{(k)}]$. CROWN computes them by running the same backward procedure with the intermediate neuron as the “output”, so a full pass costs $O(m^2n^3)$ operations for $m$ layers of width $n$ (their complexity paragraph; $O(\cdot)$ notation: Primer 0), and tighter intermediate bounds give tighter final bounds. Everything downstream (α-CROWN, β-CROWN, SDP-CROWN) inherits this structure.
2.3 α-CROWN and β-CROWN: optimise the relaxation, then branch
α-CROWN (Xu et al., ICLR 2021) observes that every choice $\alpha_j\in[0,1]$ for the unstable neurons yields a valid lower bound $g(\alpha)=-\varepsilon\|a(\alpha)\|_q + a(\alpha)^{\top}x_0 + c(\alpha)$, so one may maximise $g$ over $\alpha$ by projected gradient ascent through the backward pass (see Primer B), on a GPU, for thousands of sub-domains in parallel. For step size $\eta>0$, take $\alpha_j\leftarrow\min\{1,\max\{0,\alpha_j+\eta\,\partial g/\partial\alpha_j\}\}$: ascend, then clip each coordinate to its allowed interval. Autodifferentiation applies the chain rule to the backward bound calculation. Soundness never depends on convergence. In the walkthrough network $g$ is a concave piecewise-linear function of a single $\alpha$ whose maximum sits at $\alpha=\tfrac12$, strictly better than both endpoint rules. (With one hidden layer and fixed pre-activation bounds, $a(\alpha)$ and $c(\alpha)$ are affine in $\alpha$, so $g$ is concave; with more layers the slopes of different layers multiply, and α-CROWN also optimises separate slopes for every intermediate bound, so the joint problem is non-convex (Wang et al., eq. 12). Since every feasible $\alpha$ is sound, gradient ascent to a good, not optimal, $\alpha$ is enough.)
β-CROWN (Wang et al., NeurIPS 2021) makes bound propagation usable inside branch and bound. After splitting neuron $j$, the sub-domain carries a constraint $z_j\ge 0$ (or $z_j\le 0$). Plain CROWN can use the split to fix the neuron’s phase (identity on one sub-domain, zero on the other), but it cannot enforce the constraint itself: it still minimises over all of $\mathcal C$, including inputs on the wrong side of the split, so the split’s restriction on the inputs and on the other neurons is lost, the bound tightens little and many infeasible sub-domains go unnoticed (Wang et al., Sections 2.3 and 3.1; the walkthrough in Section 8 shows exactly this with $\beta=0$). β-CROWN encodes the split as a Lagrange multiplier.
Consider one split, $z_j(x)\ge 0$, on top of $x\in\mathcal C$. For any $\beta\ge 0$ and any feasible $x$ we have $-\beta z_j(x)\le 0$, hence $f(x)-\beta z_j(x)\le f(x)$ on the feasible set. Therefore
where the second inequality drops a constraint (a minimum over a larger set is smaller). The right-hand side is a CROWN-type problem for the modified objective $f-\beta z_j$: the term $-\beta z_j$ is linear in the pre-activation, so it simply adds $\beta$ times the sign matrix $S$ to the equivalent weight of layer $j$ during back-substitution ($S_{jj}=-1$ for a split $z_j\ge0$, $+1$ for $z_j\le 0$, $0$ if unsplit). Because the bound holds for every $\beta\ge 0$, we may maximise over $\beta$. Collecting all splits into a vector $\beta$ gives Theorem 3.1 of Wang et al.:
with $a,P,q,c$ computed by the backward pass from the weights, biases and intermediate bounds. (For an input of dimension $n$ and $r$ splits, $a\in\mathbb R^n$, $P\in\mathbb R^{n\times r}$, $q\in\mathbb R^r$, $c\in\mathbb R$; column $j$ of $P$ and entry $j$ of $q$ carry split $j$, e.g. $P_{:,j}=-w_j$ and $q_j=-b_j$ for a first-layer split $z_j=w_j^\top x+b_j\ge0$, since $-\beta_jz_j=\beta_j(-w_j)^\top x+\beta_j(-b_j)$. This vector $q$ is unrelated to the dual-norm exponent $q$ below.) For $\mathcal C=\mathcal B_p(x_0,\varepsilon)$ the inner minimum is again Hölder (their eq. 8):
which is concave in $\beta$ as long as $a,P,q,c$ stay fixed (a norm with a minus sign plus linear terms), so projected super-gradient ascent in $\beta$ is well-behaved. The coefficients are not constants, though: they depend on $\alpha$, on the intermediate bounds (which α,β-CROWN also optimises, each with its own multipliers, their eq. 12) and, through the choice of relaxation line at each unstable neuron, on the signs of the back-substituted weights. The joint problem is therefore non-convex (their Section 3.3), but any feasible $(\alpha,\beta)$ still gives a sound bound. Once every unstable neuron is split, no relaxation and no intermediate bound is left, the coefficients really are fixed and $g$ is concave in $\beta$ (their Appendix A.3); completeness rests on this. Theorem 3.2 of the paper shows that, for the $\ell_\infty$ input box of their LP (eq. 10, so $\|\cdot\|_q=\|\cdot\|_1$), $g$ is precisely the dual objective of the LP relaxation with split constraints, and its Corollary 3.2.1 that with optimal $(\alpha,\beta)$ and fixed intermediate bounds $\max g$ equals the LP optimum $p^\star_{LP}$: β-CROWN matches the LP-based BaB verifiers at bound-propagation cost. (For an $\ell_2$ ball the same relaxation carries a second-order-cone constraint on $x$ and is no longer an LP.) With BaB on all unstable neurons the procedure is sound and complete (Theorem 3.3), provided every fully split leaf is solved to optimality: a finite number of gradient steps may leave a leaf undecided, so exact leaf resolution requires certified optimization of the concave $g$ (their Appendices A.3 and B.3); plain CROWN inside BaB is not complete, because it cannot detect infeasible sub-domains, while an infeasible affine leaf admits an unbounded dual ray, which can certify infeasibility when explicitly verified (next box).
Why. A feasible $x$ would make the weighted residual $\lambda^\top(Ax-b)$ nonpositive, contradicting $\eta\gt0$; the box keeps $\min_B(v^\top x+v_0)$ finite. Example: $B=[0,1]$ and the constraint $x\ge2$ (i.e. $-x\le-2$, $\lambda=1$) give residual $2-x\ge1$ on $B$. A finite run of gradient ascent never "reaches $+\infty$": infeasibility is proved by exhibiting and checking such a $\lambda$, or by a checked LP infeasibility certificate.
Two extensions bring the cutting planes of mixed-integer programming into bound propagation: GCP-CROWN (Zhang et al., NeurIPS 2022) admits arbitrary linear cutting planes $\sum_i\big(H^{(i)}z^{(i)}+G^{(i)}a^{(i)}+Q^{(i)}\zeta^{(i)}\big)\le d$ over pre-activations, post-activations and the relaxed ReLU indicators $\zeta^{(i)}\in[0,1]$ of the mixed-integer encoding (their eq. 15, written in the notation of Section 1), each cut with its own multiplier in the same back-substitution (in the paper the cuts come from an off-the-shelf MIP solver running in parallel on the CPU); β-CROWN’s per-neuron splits are the special case of single-variable cuts. BICCOS (Zhou, Brix, Hanasusanto & Zhang, NeurIPS 2024) infers cuts from the BaB tree itself. The resulting verifier α,β-CROWN won every VNN-COMP from 2021 to 2025; in the 2025 edition it scored 1566.9 against 1430.2 for NeuralSAT, 1228.4 for PyRAT and 987.2 for CORA (Kaulen et al., VNN-COMP 2025 report, Table 6; the first three years are summarised in Brix et al., STTT 2023).
For a neuron with $l\lt0\lt u$ introduce an indicator $\zeta\in\{0,1\}$ and impose $a\ge0$, $a\ge z$, $a\le u\zeta$, $a\le z-l(1-\zeta)$. With $\zeta=0$ these force $a=0$ and $z\le0$; with $\zeta=1$ they force $a=z\ge0$: exactly the ReLU. Relaxing to $0\le\zeta\le1$ gives a convex relaxation that admits extra points: for $l=-1$, $u=2$ and $z=0$ the exact value is $a=0$, but $\zeta=\tfrac13$ allows every $a\in[0,\tfrac23]$. A valid cut is an extra linear inequality satisfied by every exact assignment ($\zeta$ binary); it can remove such relaxed points but never a genuine input–output pair of the network. In the GCP-CROWN formula each row of $H^{(i)},G^{(i)},Q^{(i)}$ holds the coefficients of one cut and $d$ collects the right-hand sides; a cut may involve several neurons, which is how it couples neurons beyond the single-neuron triangles.
- Input: network $f$, domain $\mathcal C_0$, incomplete lower-bound routine $\underline f(\cdot)$ (β-CROWN with optimised $\alpha,\beta$). Queue $\leftarrow\{\mathcal C_0\}$.
- While the queue is non-empty and time remains:
- pop a batch of sub-domains; compute $\underline f(\mathcal C_i)$ for all of them in parallel on the GPU;
- if $\underline f(\mathcal C_i)\ge 0$: $\mathcal C_i$ is verified, discard it; // discard infeasible sub-domains only with a verified infeasibility certificate
- else if an attack finds $x\in\mathcal C_i$ with $f(x)\lt 0$: return the counterexample (falsified);
- else if $\mathcal C_i$ still has an unstable neuron: choose one, $z_j$ (branching heuristic), and push $\mathcal C_i\cap\{z_j\ge 0\}$, $\mathcal C_i\cap\{z_j\le 0\}$; // closed branches: they overlap only where $z_j=0$ and both phases give $a_j=0$, and their leaves are closed polytopes, so minima are attained
- else ($\mathcal C_i$ is a leaf: every unstable neuron is split, so $f$ is affine on it) solve $\min_{x\in\mathcal C_i}f(x)$ to optimality, by an LP or its dual solved to a certified optimum (a second-order-cone program for an $\ell_2$ ball): discard the leaf if it is infeasible or the minimum is $\ge 0$, otherwise return the minimiser as a counterexample. // the finite optimisation and the attack above may both have missed it
- Return “verified” if the queue emptied, otherwise “unknown” (timeout). // on timeout the sub-domains still cover $\mathcal C_0$, so $\min\{0,\ \min_{\text{open }\mathcal C_i}\underline f(\mathcal C_i)\}$ is a sound global lower bound (0 for the discarded, verified ones)
2.4 Certified training and the tightness of ℓ2 relaxations
Verification and training interact: the numbers reported as “certified accuracy” depend on the training method at least as much as on the verifier. IBP training (above), CROWN-IBP (a CROWN backward pass on IBP intermediate bounds during training), SABR and MTL-IBP (mixed adversarial/box objectives) were re-evaluated under equal tuning in CTBench (Mao, Balauca & Vechev, ICML 2025). On CIFAR-10 at $\varepsilon=2/255$ the CTBench certified accuracies (their Table 1) are MTL-IBP 64.41%, STAPS 64.21%, SABR 63.61%, TAPS 61.27%, CROWN-IBP 57.11%, IBP 55.99%; at $\varepsilon=8/255$ they are MTL-IBP 35.41%, SABR 35.34%, IBP 35.28%, TAPS 35.25%, STAPS 35.11%, CROWN-IBP 32.59%. (The same table’s last column, e.g. 67.69% and 36.11%, is PGD adversarial accuracy, an upper bound on certified accuracy; do not quote it as a certificate: PGD (projected gradient descent, run here as ascent on the loss) searches for an adversarial input by gradient steps projected back into the threat set, and failing to find one proves nothing (Primer E). For the same model, test set and perturbation set, certified accuracy $\le$ true robust accuracy $\le$ attack-based accuracy.) Tuned IBP is within 0.13 percentage points of the best method at the larger radius: $\ell_\infty$ certified training on CIFAR-10 has saturated near 35% at $8/255$, and most published gains shrink once baselines are tuned. (Kaulen, Shavit & Hoos, 2026 go one step further and compare whole natural-vs-certified Pareto fronts: the models for which no other model is at least as good in both clean and certified accuracy and strictly better in one; Primer E.)
For $\ell_2$ balls, bound propagation has a structural weakness: the tightest box containing $\mathcal B_2(\hat x,\rho)$ is $\mathcal B_\infty(\hat x,\rho\mathbf 1)$, whose corners have $\ell_2$ distance $\sqrt n\,\rho$ from the centre, so per-neuron relaxations effectively enlarge the attack by $\sqrt n$. SDP-CROWN (Chiu, Chen, Zhang & Zhang, ICML 2025) derives, from the SDP relaxation of Section 3, a linear lower bound that couples neurons through the $\ell_2$ norm with a single extra scalar per layer:
Reason for the $\lambda$-optimised form: for $a,b\ge0$, $\inf_{\lambda\gt 0}\ \tfrac12(\lambda a + b/\lambda) = \sqrt{ab}$ (AM–GM; for $a,b\gt0$ the infimum is attained at $\lambda=\sqrt{b/a}$, while if exactly one of $a,b$ is zero it is only approached, as $\lambda\to0$ or $\lambda\to\infty$); in the centred case $\hat x=0$, with $a=\rho^2$, $b=\|\varphi\|^2$ this yields $\sup_{\lambda\gt0}h=-\rho\|\varphi\|_2$, still a valid offset because the bound holds for every $\lambda\gt0$. This step needs $\hat x=0$: only then is $\varphi=\min\{c-g,g,0\}$ independent of $\lambda$; for $\hat x\ne0$, $\varphi$ depends on $\lambda$ and $\lambda$ is optimised numerically. (All minima and maxima of vectors here are coordinatewise, $\odot$ is the entrywise product, and $\alpha\in[0,1]^n$.) Inside α-CROWN the offset $h(\alpha)$ of the ordinary relaxation is replaced by $h(g(\alpha),\lambda)$ and $(\alpha,\lambda)$ are optimised jointly; the method approaches SDP tightness on networks with 65k neurons and 2.47M parameters, far beyond what an interior-point SDP solver handles.
3. SDP Relaxations of Verification
Linear relaxations treat each neuron separately. Semidefinite relaxations keep products of variables and therefore capture correlations between neurons, at cubic cost in the number of variables. Two constructions matter for these notes: the lifting of a quadratically constrained program (Raghunathan, Steinhardt & Liang) and the quadratic-constraint / S-procedure framework of DeepSDP (Fazlyab, Morari & Pappas), which is the same machinery as LipSDP and Module 14 applied to a single point instead of a pair of points.
3.1 From a gradient bound to an SDP (ICLR 2018)
For a two-class, one-hidden-layer network $f(x)=v^{\top}\sigma(Wx)$ with $\sigma'\in[0,1]$ and an $\ell_\infty$ attack of size $\varepsilon$, Raghunathan, Steinhardt & Liang, ICLR 2018 bound the worst-case change of the margin by integrating the gradient along the segment from $x$ to $x+\delta$ and applying the dual norm (their eq. 4; the segment stays in the ball): $f(x+\delta)\le f(x)+\varepsilon\max_{\tilde x\in\mathcal B_\varepsilon(x)}\|\nabla f(\tilde x)\|_1$. By the chain rule $\nabla f(\tilde x)=W^{\top}\mathrm{diag}(v)\,\sigma'(W\tilde x)$, and the only unknown is the vector of activation derivatives $s=\sigma'(W\tilde x)\in[0,1]^m$; dropping the requirement that $s$ be realised by some $\tilde x$ (this is where conservatism enters) and writing $\|z\|_1=\max_{t\in[-1,1]^d}t^{\top}z$ gives their eq. (6):
Set $r(t):=f(x+t\delta)$ for $t\in[0,1]$. By the chain rule $r'(t)=\nabla f(x+t\delta)^\top\delta$ (Primer B), so
by Hölder's inequality with $p=\infty$, $q=1$, and because $x+t\delta$ stays in the ball. For a ReLU network $r$ is continuous and piecewise affine in $t$: apply the calculation on each affine piece and add the changes; the finitely many kinks do not change the integral, and at a kink the relaxed derivative $s_i$ may take any value in $[0,1]$.
The maximisation is a non-convex bilinear program over a box, which the authors liken to the NP-hard MAXCUT problem, and it is relaxed the way Goemans–Williamson relax MAXCUT: substitute $s\to\tfrac12(\mathbf 1+s)$ so that all variables live in $[-1,1]$, stack $y=[1;\,t;\,s]$, write the objective as $\tfrac14 y^{\top}M(v,W)y=\tfrac14\langle M(v,W),\,yy^{\top}\rangle$, and observe that $P=yy^{\top}$ is positive semidefinite with $\mathrm{diag}(P)\le 1$. Dropping the rank-one requirement (eq. 10),
and the certificate is $\max_{i\ne y}f^{iy}_{\rm SDP}(x)\lt 0$ with $v=V_i-V_y$ per class pair: for a multiclass logit map $F(x)=V\sigma(Wx)$ the margin against class $i$, $f^{iy}(x)=F_i(x)-F_y(x)$, is a one-hidden-layer network whose output vector is the difference of rows $V_i-V_y$. The SDP depends only on the weights, and every dual-feasible point gives a valid bound, so the dual variables can be trained jointly with the weights: the network is trained against its own certificate (SDP-NN: no attack at $\varepsilon=0.1$ on MNIST exceeds 35% error). The optimal value itself may have kinks where the dual optimiser changes, so it is not differentiated directly.
MAXCUT splits the vertices of a weighted graph into two groups so that the total weight of the edges between the groups is maximal. With signs $s_i\in\{-1,1\}$ marking the groups, the cut weight is $\sum_{i\lt j}w_{ij}(1-s_is_j)/2$, a quadratic function of the signs (a triangle with unit weights has maximum cut $2$). Goemans and Williamson replace the rank-one matrix $ss^\top$ by any PSD matrix with unit diagonal, which enlarges the feasible set and turns the problem into an SDP. The same lifting is used here; their approximation guarantee is not needed.
Write $A=W^\top\mathrm{diag}(v)\in\mathbb R^{d\times m}$ and let $s_{\rm old}=\tfrac12(\mathbf 1+s)$ with the new $s\in[-1,1]^m$ (the page reuses the letter $s$). With $y=[1;\,t;\,s]$ take
so the objective is $t^\top As_{\rm old}=\tfrac14y^\top My=\tfrac14\langle M,yy^\top\rangle$, with $\langle M,P\rangle=\mathrm{tr}(M^\top P)=\sum_{ij}M_{ij}P_{ij}$ (Primer A). $P=yy^\top$ satisfies $P\succeq0$ and $\mathrm{diag}(P)=(1,t_i^2,s_j^2)\le1$; the SDP keeps these two properties and drops $\mathrm{rank}\,P=1$.
3.2 Lifting the ReLU constraints (NeurIPS 2018)
The gradient bound is specific to one hidden layer. The general recipe, from the sequel Raghunathan, Steinhardt & Liang, NeurIPS 2018, lifts the verification problem itself.
Step 1 (exact reformulation). $a=\mathrm{ReLU}(z)$ holds if and only if $a\ge 0$, $a\ge z$ and $a_i(a_i-z_i)=0$ for every $i$: the first two say $a\ge\max(0,z)$, and the complementarity equality forces $a_i$ to equal one of the two. With $z=Wx+b$ the equality is quadratic in $(x,a)$: $a_i^2 = a_i\,(W_{i,:}x+b_i)$. An input box $l\le x\le u$ is likewise quadratic: $(x_i-l_i)(x_i-u_i)\le 0$, i.e. $x_i^2\le(l_i+u_i)x_i-l_iu_i$. The verification problem $\max c^{\top}a$ subject to these constraints is a non-convex QCQP that is exact.
Step 2 (lift). Stack $v=[1;\,x;\,a]$ and define $P=vv^{\top}$. Every monomial of degree $\le 2$ in $(x,a)$ is an entry of $P$: $x_i = P_{1,x_i}$, $a_i^2=P_{a_i,a_i}$, $a_i x_j = P_{a_i,x_j}$. Hence all constraints of Step 1 become linear in $P$:
and the objective $c^{\top}a=c^{\top}P_{1,a}$ is linear too. What is not convex is the requirement $P=vv^{\top}$, i.e. $P\succeq 0$, $P_{11}=1$ and $\mathrm{rank}\,P=1$.
Step 3 (relax). Drop the rank constraint. The result is an SDP whose optimal value upper-bounds the true maximum: every feasible point of the original problem gives a feasible rank-one $P$, so the feasible set only grew. Multi-layer networks add one block of variables per layer. The relaxation is not uniformly tighter than the LP/triangle relaxation (for a single ReLU in isolation the LP is tighter), but with many neurons it typically is, because the $P_{a_i,a_j}$ terms remember how neurons co-vary. Their Proposition 1 (box below) makes this quantitative in one random setting. This coupling is precisely the inter-neuron coupling that SDP-CROWN (Section 2.4) later extracts in closed form for $\ell_2$ balls.
Statement. For a universal constant $\gamma$: $p_{\rm LP}\ge\tfrac12md$ almost surely, and $p_{\rm SDP}\le\gamma\,(m\sqrt d+d\sqrt m)$ with probability at least $1-e^{-(d+m)}$ over the draw of $W$.
Consequence. On that event $\dfrac{p_{\rm LP}}{p_{\rm SDP}}\ge\dfrac{md}{2\gamma(m\sqrt d+d\sqrt m)}=\dfrac{1}{2\gamma\big(1/\sqrt d+1/\sqrt m\big)}\ge\dfrac{\sqrt{\min(m,d)}}{4\gamma}$, since $1/\sqrt d+1/\sqrt m\le2/\sqrt{\min(m,d)}$: the LP bound is looser by a factor of order at least $\sqrt{\min(m,d)}$. Each LP neuron may use its own worst input, while the SDP keeps the shared products. These are one-sided bounds for this random model (zero biases, box, all-ones objective), not a scaling law for arbitrary networks or specifications.
3.3 DeepSDP: quadratic constraints and the S-procedure
Fazlyab, Morari & Pappas, TAC 2022 organise the same idea in control-theoretic language. Every piece of the problem is abstracted by a quadratic constraint (QC) at a single point (compare Module 2):
- Input set. $x\in\mathcal X$ is over-approximated by $\begin{bmatrix}x\\1\end{bmatrix}^{\top}P\begin{bmatrix}x\\1\end{bmatrix}\ge 0$ for all $P\in\mathcal P_{\mathcal X}$; a box $[\underline x,\overline x]$ gives $(x-\underline x)^{\top}\Gamma(\overline x-x)\ge 0$ for any diagonal $\Gamma\succeq 0$ (each term is a product of two non-negative numbers).
- Activation. $\phi$ satisfies $\begin{bmatrix}z\\ \phi(z)\\ 1\end{bmatrix}^{\top}Q\begin{bmatrix}z\\ \phi(z)\\ 1\end{bmatrix}\ge 0$ for all $Q\in\mathcal Q_\phi$. For ReLU (their eq. 21 and Lemma 3): the complementarity $\phi_i(\phi_i-z_i)=0$ (an equality, so its multiplier $\lambda_i$ may have either sign), the facts $\phi_i\ge z_i$ (multiplier $\nu_i\ge0$) and $\phi_i\ge 0$ (multiplier $\eta_i\ge 0$), and cross-neuron terms $\lambda_{ij}\big[(\phi_j-\phi_i)(z_j-z_i)-(\phi_j-\phi_i)^2\big]\ge 0$, $\lambda_{ij}\ge0$, which hold because ReLU is monotone and 1-Lipschitz. Pre-activation bounds from a cheap pre-solve (e.g. IBP) tell which neurons are always active or inactive, and their Lemma 4 then frees the corresponding multipliers.
- Specification. The unsafe half-space $c^{\top}f(x)\gt d$ is encoded by $S=\begin{bmatrix}0&0&0\\0&0&c\\0&c^{\top}&-2d\end{bmatrix}$, so that $\begin{bmatrix}x\\ f(x)\\1\end{bmatrix}^{\top}S\begin{bmatrix}x\\ f(x)\\1\end{bmatrix}=2\,(c^{\top}f(x)-d)$. (DeepSDP’s safe set is $c^{\top}f(x)\le d$, so its $d$ is minus the $d$ of Section 1.)
Fix $x\in\mathcal X$ and let $\xi=[x;\,\phi(W^0x+b^0);\,1]$. Multiply the LMI from both sides by $\xi$: $\xi^{\top}M_{\rm in}(P)\xi + \xi^{\top}M_{\rm mid}(Q)\xi+\xi^{\top}M_{\rm out}(S)\xi\le 0$. By construction of the padding, the first term equals $[x;1]^{\top}P[x;1]$, which is $\ge0$ because $x\in\mathcal X$; the second equals $[z;\phi(z);1]^{\top}Q[z;\phi(z);1]$ with $z=W^0x+b^0$, which is $\ge 0$ because $\phi$ satisfies the QC on $\mathcal Z$. Two non-negative terms plus the third are $\le 0$, so the third is $\le 0$: $2(c^{\top}f(x)-d)\le0$. This is the S-procedure of Module 2 (Boyd et al., 1994): a sufficient condition (the multipliers inside $P$ and $Q$ are the $\tau_i$), lossless only in special cases, hence a relaxation whose conservatism shrinks as more valid QCs are added.
Cost. An interior-point solver for an SDP with an $n\times n$ matrix variable and $m$ constraints needs $O(\sqrt n\log(1/\epsilon))$ Newton iterations, each costing $O(mn^3+m^2n^2+m^3)$ (Module 2), and here $n$ is the number of neurons plus inputs. Plain interior-point DeepSDP and LipSDP therefore stop at networks with a few thousand neurons; the remedies are sparsity exploitation, layer-wise recursions and closed-form relaxations (Module 12), or, for verification, extracting only the $\ell_2$ coupling into bound propagation (SDP-CROWN). Which relaxation wins is a question of the input set: for $\ell_\infty$ boxes and well-trained networks, α,β-CROWN with BaB; for $\ell_2$ balls and small networks, the SDP.
4. Randomized Smoothing
Sections 2–3 certify a network by looking inside it. Randomized smoothing certifies a different classifier, built from any base classifier by averaging over Gaussian noise, and never looks inside at all. That is what lets it reach ImageNet scale. In this section $\sigma$ is the noise level, $\delta$ is an adversarial perturbation and $\alpha$ is the failure probability of the Monte-Carlo certificate.
In words. Beyond measurability and a fixed randomisation law, nothing is assumed about $f$; only the two numbers $\underline{p_A}$, $\overline{p_B}$ matter. The radius grows with $\sigma$ (more smoothing), with $\underline{p_A}$ and with the gap to $\overline{p_B}$; it is $\ell_2$ specifically, because the Gaussian is rotation-invariant. Tightness means that the theorem cannot be improved without assuming more about $f$. The proof is a hypothesis-testing argument: the worst-case base classifier is a half-space perpendicular to $\delta$.
Lemma (Neyman–Pearson, Cohen et al. Lemma 3). Let $X,Y$ have densities $\mu_X,\mu_Y$ on $\mathbb R^d$ and let $h:\mathbb R^d\to\{0,1\}$ be any (possibly random) test. If $S=\{z:\mu_Y(z)\le t\mu_X(z)\}$ for some $t\gt 0$ and $\mathbb P(h(X)=1)\ge\mathbb P(X\in S)$, then $\mathbb P(h(Y)=1)\ge\mathbb P(Y\in S)$. (Part 2: with $\ge t$ and $\le$, the conclusion is $\le$.)
Proof of the lemma. Write $h(1|z)$ for the probability that $h(z)=1$ and $S^c$ for the complement. Then
The first equality splits $\int h(1|z)\mu_Y$ over $S$ and $S^c$ and uses $h(1|z)=1-h(0|z)$ on $S$; the inequality uses $\mu_Y\ge t\mu_X$ on $S^c$ and $\mu_Y\le t\mu_X$ on $S$ (both with the right sign because of the minus in front of the second integral); the last equality reverses the first step for $X$. $\square$
Specialisation to Gaussians (Lemma 4). For $X\sim\mathcal N(x,\sigma^2I)$ and $Y\sim\mathcal N(x+\delta,\sigma^2I)$,
a strictly increasing function of $\delta^{\top}z$. Hence every half-space $\{\delta^{\top}z\le\kappa\}$ is a likelihood-ratio set $\{\mu_Y/\mu_X\le t\}$ (and $\{\delta^{\top}z\ge\kappa\}$ one of the form $\{\mu_Y/\mu_X\ge t\}$), so the lemma applies to half-spaces normal to $\delta$.
Main argument. Fix $\delta\ne0$ (for $\delta=0$, $R\gt0$ means $\underline{p_A}\gt\overline{p_B}$, which already makes $c_A$ the unique top class) and a competitor class $c_B\ne c_A$; put $X=x+\varepsilon$, $Y=x+\delta+\varepsilon$. Take $0\lt\overline{p_B}\le\underline{p_A}\lt1$, so that all quantiles below are finite; a bound equal to $0$ or $1$ can be replaced by a valid bound arbitrarily close to it, which gives the theorem with $\Phi^{-1}(0)=-\infty$, $\Phi^{-1}(1)=+\infty$ (only $\underline{p_A}=\overline{p_B}\in\{0,1\}$ is indeterminate). We must show $\mathbb P(f(Y)=c_A)\gt\mathbb P(f(Y)=c_B)$. Define the half-spaces
Step 1: $A$ and $B$ match the known probabilities under $X$. Since $\delta^{\top}(X-x)=\delta^{\top}\varepsilon\sim\mathcal N(0,\sigma^2\|\delta\|^2)$, the variable $\delta^{\top}(X-x)/(\sigma\|\delta\|)$ is standard normal, so $\mathbb P(X\in A)=\Phi(\Phi^{-1}(\underline{p_A}))=\underline{p_A}$ and $\mathbb P(X\in B)=1-\Phi(\Phi^{-1}(1-\overline{p_B}))=\overline{p_B}$.
Step 2: apply the lemma twice. With $h=\mathbf 1[f(\cdot)=c_A]$ we have $\mathbb P(h(X)=1)\ge\underline{p_A}=\mathbb P(X\in A)$, so $\mathbb P(f(Y)=c_A)\ge\mathbb P(Y\in A)$. With $h=\mathbf 1[f(\cdot)=c_B]$ and part 2 of the lemma, $\mathbb P(h(X)=1)\le\overline{p_B}=\mathbb P(X\in B)$ gives $\mathbb P(f(Y)=c_B)\le\mathbb P(Y\in B)$.
Step 3: compute the two probabilities under $Y$. Now $\delta^{\top}(Y-x)=\|\delta\|^2+\delta^{\top}\varepsilon$, so
using $-\Phi^{-1}(1-p)=\Phi^{-1}(p)$ for the second. Step 4. Because $\Phi$ is increasing, $\mathbb P(Y\in A)\gt\mathbb P(Y\in B)$ if and only if $\Phi^{-1}(\underline{p_A})-\|\delta\|/\sigma\gt\Phi^{-1}(\overline{p_B})+\|\delta\|/\sigma$, i.e. $\|\delta\|\lt\tfrac\sigma2(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B}))=R$. Chaining Steps 2–4 gives $\mathbb P(f(Y)=c_A)\ge\mathbb P(Y\in A)\gt\mathbb P(Y\in B)\ge\mathbb P(f(Y)=c_B)$ for every $c_B$, hence $g(x+\delta)=c_A$. $\square$
Tightness (Theorem 2). The base classifier $f^\star$ that returns $c_A$ on $A$, $c_B$ on $B$ and other classes elsewhere is well defined when $\underline{p_A}+\overline{p_B}\le1$ (the hypothesis of Theorem 2): then $\Phi^{-1}(\underline{p_A})\le\Phi^{-1}(1-\overline{p_B})$, so $A$ and $B$ are disjoint except, at equality, for their common boundary hyperplane, which has probability zero under every Gaussian and can be given to either class. It is consistent with the class probabilities (Step 1) provided the leftover mass $1-\underline{p_A}-\overline{p_B}$ can be shared among the other $K-2$ classes with at most $\overline{p_B}$ each, i.e. $\underline{p_A}+(K-1)\overline{p_B}\ge1$. The paper leaves this implicit; it holds automatically for CERTIFY’s choice $\overline{p_B}=1-\underline{p_A}$. It can fail: with two classes, $\underline{p_A}=0.6$ and $\overline{p_B}=0.3$ give $R\approx0.389\sigma$, yet normalisation forces $p_A\ge0.7$, which certifies $0.524\sigma$. When the condition holds, Step 3 shows that $f^\star$ has $\mathbb P(f^\star(Y)=c_A)\lt\mathbb P(f^\star(Y)=c_B)$ for every $\|\delta\|\gt R$: the half-space is the worst case, and the bound cannot be improved.
Monte-Carlo certification and its price
$p_A$ cannot be computed exactly for a neural base classifier, so it is estimated, and the certificate becomes a statistical statement.
- Draw $n_0$ noisy copies $x+\varepsilon_i$, evaluate $f$, and let $\hat c_A$ be the most frequent class. // selection sample, $n_0=100$ in the paper
- Draw $n$ fresh noisy copies and count $k=\#\{i: f(x+\varepsilon_i)=\hat c_A\}$. // estimation sample, $n=100{,}000$
- $\underline{p_A}\leftarrow$ one-sided Clopper–Pearson lower confidence bound (see Primer C) at level $1-\alpha$ for a Binomial$(n,p)$ parameter given $k$ successes. // $\alpha=0.001$
- If $\underline{p_A}\gt\tfrac12$: return $\hat c_A$ with radius $R=\sigma\,\Phi^{-1}(\underline{p_A})$; else ABSTAIN. // uses $\overline{p_B}:=1-\underline{p_A}$ in Theorem 1
The two samples are kept separate for a statistical reason. Conditional on the selection sample, $\hat c_A$ is a fixed label, and each of the $n$ fresh draws votes for it independently with the same probability $p=\mathbb P(f(x+\varepsilon)=\hat c_A)$, so $k\sim\mathrm{Binomial}(n,p)$ and the Clopper–Pearson bound applies. Choosing the label and estimating its probability on the same draws would favour whichever label happened to do well on them, and the fixed-label interval would no longer be valid without a correction for that selection. With probability at least $1-\alpha$ over the sampling, a returned certificate is correct (Proposition 2 of the paper). Two costs follow. First, $10^5$ forward passes per certified input: 15 s per CIFAR-10 image (110-layer ResNet) and 110 s per ImageNet image (ResNet-50) on an RTX 2080 Ti. Second, the radius is capped by $n$: even if $f$ returns $c_A$ on all $n$ samples, the best lower bound is $\underline{p_A}=\alpha^{1/n}$, so $R\le\sigma\Phi^{-1}(\alpha^{1/n})$, which is $1.50\sigma$ for $n=100$, $3.20\sigma$ for $n=10^4$ and $3.81\sigma$ for $n=10^5$ at $\alpha=0.001$; certifying $4\sigma$ at 99.9% confidence has the sufficient sample count $n\ge\ln(10^3)/(1-\Phi(4))\approx2.2\times10^5$. Prediction alone is cheap (PREDICT: $n=100$ samples and a two-sided binomial test, 0.15 s).
If all $n$ draws vote for $\hat c_A$, the one-sided Clopper–Pearson bound solves $\mathbb P(\mathrm{Bin}(n,p)\ge n)=p^n=\alpha$, so $\underline{p_A}=\alpha^{1/n}$ and $R=\sigma\Phi^{-1}(\alpha^{1/n})$. Hence $R\ge r\sigma$ iff $\alpha^{1/n}\ge\Phi(r)$ iff $\ln\alpha\ge n\ln\Phi(r)$ iff $n\ge\ln(1/\alpha)/\big(-\ln\Phi(r)\big)$ (dividing by the negative number $\ln\Phi(r)$ flips the inequality). With $u=1-\Phi(r)$ we have $-\ln\Phi(r)=-\ln(1-u)=u+\tfrac{u^2}2+\dots\ge u$, so $n\ge\ln(1/\alpha)/u$ is sufficient, and almost exact for small $u$. For $r=4$, $\alpha=10^{-3}$: $u=3.17\times10^{-5}$, and both expressions give $n\approx2.18\times10^5$.
Denoised smoothing. Theorem 1 holds for any base classifier, so the base classifier may include a denoiser. Carlini et al., ICLR 2023 use an off-the-shelf diffusion model as a one-shot denoiser in front of an off-the-shelf classifier: the forward process $x_t=\sqrt{\alpha_t}\,x+\sqrt{1-\alpha_t}\,\mathcal N(0,I)$ is matched to the smoothing noise by choosing $t^\star$ with $\sigma^2=(1-\alpha_{t^\star})/\alpha_{t^\star}$ (their eq. 4; here $\alpha_t$ is the diffusion noise schedule, not a failure probability), and the rescaled noisy input $\sqrt{\alpha_{t^\star}}(x+\varepsilon)$, $\varepsilon\sim\mathcal N(0,\sigma^2I)$, is denoised in one step and classified. The matching is one line: with $\varepsilon=\sigma Z$, $Z\sim\mathcal N(0,I)$, the input is $\sqrt{\alpha_{t^\star}}\,x+\sqrt{\alpha_{t^\star}}\,\sigma Z$, and $\alpha_{t^\star}\sigma^2=1-\alpha_{t^\star}$ is exactly the choice of $t^\star$, so it has the law $\sqrt{\alpha_{t^\star}}\,x+\sqrt{1-\alpha_{t^\star}}\,Z$ of the diffusion inputs the denoiser was trained on. For the certificate the denoiser is simply part of the base classifier: the composition of the rescaling, the one-step denoiser at time $t^\star$ and the classifier is fixed during certification (any internal randomness has the same law on every call), so Theorem 1 applies to it unchanged; the quality of the denoising affects $p_A$ and hence the radius, never soundness. No training is needed, and the certified ImageNet top-1 accuracies are 71.1 / 54.3 / 38.1 / 29.5% at $\ell_2$ radii 0.5 / 1.0 / 1.5 / 2.0 (BEiT-L classifier, 552M-parameter diffusion model, $n=10^4$ samples). The best deterministic certificates are far behind at large radii: the 2B-parameter LipNeXt reaches 41.2% certified accuracy at radius $36/255\approx 0.14$ and 22.4% at radius 1 (Hu, Hu & Fredrikson, ICLR 2026; see Module 13).
5. Conformal Prediction for Safe Planning and Control
Randomized smoothing certifies a classifier’s decision. Conformal prediction (CP) certifies a prediction set: with a small calibration sample it turns any heuristic uncertainty score into a set that contains the truth with prescribed probability, for any data distribution. In this section $\alpha\in(0,1)$ is the miscoverage level and $\delta$ is the failure probability in the control application.
- Choose a nonconformity score $s(x,y)\in\mathbb R$: large when the model’s prediction at $x$ disagrees with $y$ (e.g. $|y-\hat f(x)|$ for regression; $1-\hat f_y(x)$ for classification, with $\hat f_y(x)=e^{z_y}/\sum_j e^{z_j}$ the softmax probability of class $y$ computed from the model’s logits $z_j$ at $x$, Primer E).
- On a calibration set $(X_i,Y_i)_{i=1}^n$ not used for training, compute $s_i=s(X_i,Y_i)$.
- Let $\hat q$ be the $\lceil(n+1)(1-\alpha)\rceil/n$ empirical quantile of $s_1,\dots,s_n$: sort the scores and take the $k$-th smallest with $k=\lceil(n+1)(1-\alpha)\rceil$ ($\hat q=+\infty$ if $k\gt n$; $\lceil r\rceil$ is the smallest integer $\ge r$).
- For a new input, output $\mathcal C(X_{\rm test})=\{y:\ s(X_{\rm test},y)\le\hat q\}$.
Let $s_i=s(X_i,Y_i)$ for the calibration points and $s_{\rm test}=s(X_{\rm test},Y_{\rm test})$. Assume the $n+1$ scores are almost surely distinct (the general case needs a tie-breaking convention). Sort the calibration scores, $s_{(1)}\lt\dots\lt s_{(n)}$, and let $k=\lceil(n+1)(1-\alpha)\rceil$.
Step 1 (rewrite the event). By definition of $\mathcal C$, $\{Y_{\rm test}\in\mathcal C(X_{\rm test})\}=\{s_{\rm test}\le\hat q\}$. If $k\gt n$ then $\hat q=\infty$ and coverage is trivially $1$, so assume $k\le n$, i.e. $\alpha\ge\tfrac1{n+1}$; then $\hat q=s_{(k)}$ and the event is $\{s_{\rm test}\le s_{(k)}\}$.
Step 2 (exchangeability fixes the rank distribution). Among the $n+1$ exchangeable, a.s. distinct scores $s_1,\dots,s_n,s_{\rm test}$, the rank of $s_{\rm test}$ is uniform on $\{1,\dots,n+1\}$: any permutation of the scores has the same joint law, so no position is more likely than another. Now $s_{\rm test}\le s_{(k)}$ (the $k$-th smallest of the calibration scores) holds exactly when the rank of $s_{\rm test}$ among all $n+1$ is at most $k$ (if $s_{\rm test}$ is among the $k$ smallest of all $n+1$ points, at most $k-1$ calibration points are below it, so it lies below the $k$-th calibration order statistic, and conversely). Hence
Step 3 (both bounds). With $k=\lceil(n+1)(1-\alpha)\rceil$: $k\ge(n+1)(1-\alpha)$ gives $\mathbb P\ge 1-\alpha$; $k\lt(n+1)(1-\alpha)+1$ gives $\mathbb P\lt 1-\alpha+\tfrac1{n+1}$. Continuity is only needed for the upper bound (ties would push mass onto the boundary). $\square$
Where the assumptions enter. Exchangeability is used once, in Step 2, and nothing else is used: no assumption on the model, the score or the distribution. The price is that the guarantee is marginal: averaged over calibration sets and test points. Conditioning on the calibration set (Primer C), the coverage is a random variable, and its law needs more than exchangeability. If the calibration and test points are i.i.d. and the model (hence the score) was fitted on independent training data, then, conditionally on that training data, the $n+1$ scores are i.i.d. with a common CDF $F$. For continuous $F$ and $k\le n$ the conditional coverage is then $F(s_{(k)})$, the CDF evaluated at the $k$-th order statistic of $n$ i.i.d. draws, which is $\mathrm{Beta}(k,\,n+1-k)$-distributed (derivation below; for $k=n+1$ it is identically 1); writing $l=\lfloor(n+1)\alpha\rfloor$ (the largest integer $\le(n+1)\alpha$) so that $k=n+1-l$, this is the $\mathrm{Beta}(n+1-l,\ l)$ law quoted by Angelopoulos & Bates, with mean $k/(n+1)$ and standard deviation $\sqrt{kl/((n+1)^2(n+2))}\approx\sqrt{\alpha(1-\alpha)/n}$. Panel B of the explorer shows both: the mean sits inside $[1-\alpha,\,1-\alpha+\tfrac1{n+1}]$, the individual runs scatter around it.
For $a,b\gt0$ the $\mathrm{Beta}(a,b)$ distribution on $(0,1)$ has density proportional to $u^{a-1}(1-u)^{b-1}$, mean $a/(a+b)$ and variance $ab/[(a+b)^2(a+b+1)]$. It appears here as follows, for a fixed score function with continuous CDF $F$ and $1\le k\le n$. (i) Probability integral transform: $\mathbb P(F(s)\le u)=u$ for $u\in[0,1]$ (for strictly increasing $F$, $F(s)\le u$ iff $s\le F^{-1}(u)$, which has probability $F(F^{-1}(u))=u$; flat pieces of $F$ carry no probability), so the $U_i=F(s_i)$ are i.i.d. uniform on $[0,1]$, and because $F$ is non-decreasing, $F(s_{(k)})=U_{(k)}$, the $k$-th smallest of them. (ii) $U_{(k)}\le u$ exactly when at least $k$ of the $n$ uniforms are $\le u$, a binomial event: $\mathbb P(U_{(k)}\le u)=\sum_{j=k}^n\binom nj u^j(1-u)^{n-j}$. (iii) Differentiating, the sum telescopes to the density $\frac{n!}{(k-1)!\,(n-k)!}\,u^{k-1}(1-u)^{n-k}$, i.e. $\mathrm{Beta}(k,n+1-k)$, with mean $k/(n+1)$ and variance $k(n+1-k)/[(n+1)^2(n+2)]$. Example: $n=9$, $\alpha=0.1$ gives $k=9$, density $9u^8$, mean $0.9$ and standard deviation $0.09$, so single calibration sets scatter visibly around the marginal guarantee.
Safe planning among dynamic agents (Lindemann et al., RA-L 2023)
A robot with known dynamics $x_{t+1}=f(x_t,u_t)$ shares the space with $N$ agents whose joint trajectory $(Y_0,Y_1,\dots)\sim\mathcal D$ is unknown; a learned predictor (an LSTM in the paper; Primer E) produces forecasts $\hat Y_{\tau|t}$ of $Y_\tau$ from the observations up to time $t$. The requirement is chance-constrained (Primer C): for a constraint function $c$ that is $L$-Lipschitz in the agents’ state uniformly in the robot state, $|c(x,y)-c(x,y')|\le L\|y-y'\|$ for all $x$ (e.g. $c(x,y)=\|x-y\|-0.5$ for collision avoidance with one agent, $L=1$; with agents at positions $y^{(i)}$, $c(x,y)=\min_i\|x-y^{(i)}\|-0.5$, still with $L=1$),
Lindemann, Cleaveland, Shim & Pappas, RA-L 2023 obtain this from split CP applied to prediction errors. Nothing in the method acts on the start: their footnote 2 assumes it is safe, $c(x_0,Y_0)\ge0$ (almost surely), and the planner below only constrains the times $1,\dots,T$. On top of that they make two assumptions: Assumption 1, the robot’s actions do not change the distribution of the agents (no interaction), and Assumption 2, a calibration set $D_{\rm cal}$ of trajectories drawn independently from $\mathcal D$.
Theorem 1. With $\bar\delta:=\delta/T$, simultaneously over the horizon, $$ \begin{aligned} &\mathbb P\big(\|Y_\tau-\hat Y_{\tau|0}\|\le C_{\tau|0}\ \ \forall\tau\in\{1,\dots,T\}\big)\ge 1-\delta,\\ &\mathbb P\big(\|Y_{t+1}-\hat Y_{t+1|t}\|\le C_{t+1|t}\ \ \forall t\in\{0,\dots,T-1\}\big)\ge 1-\delta . \end{aligned} $$
Proof of Theorem 1 (one line). Each individual event fails with probability at most $\bar\delta$; Boole’s inequality bounds the probability that any of the $T$ events fails by $T\bar\delta=\delta$. This union bound is the source of the method’s conservatism: the regions are calibrated at level $1-\delta/T$, so for $T=20$ and $\delta=0.05$ each region must cover 99.75% of the calibration errors, and with $|D_{\rm cal}|$ trajectories one needs $\lceil(|D_{\rm cal}|+1)\cdot 0.9975\rceil\le|D_{\rm cal}|$, i.e. at least 399 calibration trajectories before the region is even finite. The regions then enter the planner as tightened constraints (see Primer D):
Here $J$ is the trajectory cost, $\mathcal U$ and $\mathcal X$ are the admissible input and state sets, and the conformal constraint is imposed at the next $H\le T-t$ steps. Theorem 2 (open loop). If this problem is feasible almost surely at $t=0$ with $H=T$ (the paper says “feasible”; see below), the resulting input sequence gives $\mathbb P\big(c(x_\tau,Y_\tau)\ge 0\ \forall\tau\in\{1,\dots,T\}\big)\ge1-\delta$, which together with the assumed safe start is the chance constraint. Proof: by Lipschitz continuity, $0\le c(x_\tau,\hat Y_{\tau|0})-LC_{\tau|0}\le c(x_\tau,Y_\tau)+L\|Y_\tau-\hat Y_{\tau|0}\|-LC_{\tau|0}$; on the event of Theorem 1 the last two terms are $\le0$ together, so $c(x_\tau,Y_\tau)\ge 0$ for all $\tau\in\{1,\dots,T\}$ with probability $\ge1-\delta$. Feasibility is itself random, since it depends on the calibration data and the forecasts, so the proof is really an event inclusion, $\{\text{all regions cover}\}\cap\{\text{feasible}\}\subseteq\{\text{safe}\}$. Hence $\mathbb P(\text{feasible and unsafe})\le\delta$ always; the unconditional $\mathbb P(\text{safe})\ge1-\delta$ needs feasibility almost surely (or a certified fallback), and conditionally on feasibility only $\mathbb P(\text{unsafe}\mid\text{feasible})\le\delta/\mathbb P(\text{feasible})$ follows. Theorem 3 (closed loop). If the problem is feasible almost surely at every $t$ (recursive feasibility is assumed, not proved), applying only $u_t$ and re-planning with updated forecasts gives the same guarantee for $t\in\{1,\dots,T\}$ via the second statement of Theorem 1 (and, with the safe start, the chance constraint). The closed loop is much less conservative because the regions are recomputed from fresh observations and short-horizon ones are small (average cost 367 versus 414 for the open loop in their synthetic ORCA study, $|D_{\rm cal}|=2000$, $T=20$). In the CARLA intersection study ($\delta=0.05$) one of 100 runs violated the constraint. That is consistent with the theorem, but the paper’s reading, “at most 5 of the 100 MPC runs”, overstates it: a 5% failure probability bounds the expected number of violations by five, not the realised count (independent runs that each fail with probability exactly 0.05 produce more than five violations with probability 0.384). Note also what the experiment changed to make the MPC work: $T=30$ instead of the true mission length 60 because calibration data were scarce, the smallest region over $t$ reused for each look-ahead, and slack variables on the conformal constraint for recursive feasibility (replace $c\ge LC$ by $c\ge LC-s$ with $s\ge0$ and penalise $s$ in the cost; Primer B). Each change steps outside the hypotheses of Theorem 3 (a union bound over 30 steps does not cover 60; a region smaller than $C_{t+\kappa|t}$ is not a calibrated region; a softened constraint is not the constraint), a small instance of “benchmark safety is not a guarantee” (Section 7).
6. The Scenario Approach
Conformal prediction certifies a prediction set; the scenario approach certifies a decision. Robust control asks for a design that satisfies a constraint for every value of an uncertain parameter $\delta\in\Delta$, a semi-infinite program (finitely many decision variables, potentially infinitely many constraints) that is intractable in general. The scenario approach samples $N$ parameters and imposes only those. In this section $\varepsilon$ is a violation probability, $\beta$ a confidence parameter (the confidence is $1-\beta$) and $d$ the number of decision variables.
In words. $\mathbb P^N$ is the joint law of the $N$ i.i.d. samples: the design $x^\star_N$ is random because it is computed from them, and $V(x^\star_N)$ is the probability that a fresh draw $\delta\sim\mathbb P$ violates it. So with confidence $1-\beta$ over the samples, where $\beta$ is the binomial tail, the scenario design violates at most an $\varepsilon$-fraction of the unseen uncertainty. To read the binomial: equality (fully supported case) says that $V(x^\star_N)$ has the law of the $d$-th smallest of $N$ independent uniforms on $[0,1]$, i.e. $\mathrm{Beta}(d,N-d+1)$, and the $d$-th smallest uniform exceeds $\varepsilon$ exactly when fewer than $d$ of the $N$ uniforms fall in $[0,\varepsilon]$, a $\mathrm{Bin}(N,\varepsilon)$ count. The $d$ support constraints play the role of the $d$ order statistics that pin the solution down. The bound sharpened the earlier $\binom Nd(1-\varepsilon)^{N-d}$ of Calafiore & Campi, TAC 2006 substantially: for $\varepsilon=0.05$, $\beta=10^{-5}$, $d=10$ the required sample size drops from $N=1344$ to $N=581$ (Campi & Garatti, SIAM J. Optim. 2008, Table 2.2). Finding the smallest integer $N$ whose tail is at most $\beta$ needs a discrete search (the tail is non-increasing in $N$, so bisection over the integers works; equality is not needed); an explicit sufficient condition is more convenient in a design loop.
Why each assumption matters. Convexity of the sets $\mathcal X_\delta$ and of the cost is what caps the number of support constraints at $d$ (Proposition 2.2); for non-convex designs no such cap exists in general and the bound need not hold. Feasibility and a unique solution make $x^\star_N$ a well-defined function of the samples (with ties, the minimum-norm tie-break of Section 2.1 of the paper restores this); the non-empty-interior condition is a regularity condition of the proof. Independence of the $N$ samples, drawn from the same $\mathbb P$ that governs deployment, is what turns “fewer than $d$ samples violate” into a binomial tail; samples from a different distribution (a mismatched model posterior, for instance) certify the violation probability under that distribution only.
Let $X\sim\mathrm{Bin}(N,\varepsilon)$ with mean $\mu=N\varepsilon$. The multiplicative Chernoff bound for the lower tail states that $\mathbb P\big(X\le(1-t)\mu\big)\le\exp(-t^2\mu/2)$ for $t\in[0,1]$.
Step 1. The Campi–Garatti tail is $\mathbb P(X\le d-1)\le\mathbb P(X\le d)$. Provided $d\le\mu$ (checked below), write $d=(1-t)\mu$ with $t=1-d/\mu\in[0,1]$; Chernoff gives
Step 2. The right-hand side is $\le\beta$ iff $(N\varepsilon-d)^2\ge 2N\varepsilon\ln\frac1\beta$. Abbreviate $\ell_\beta:=\ln\frac1\beta$ (a local symbol, not a Lipschitz constant) and try $N\varepsilon=2\ell_\beta+2d$ (that is $N=\frac2\varepsilon(\ell_\beta+d)$): the left side is $(2\ell_\beta+d)^2=4\ell_\beta^2+4\ell_\beta d+d^2$ and the right side is $2(2\ell_\beta+2d)\ell_\beta=4\ell_\beta^2+4\ell_\beta d$, so the inequality holds, with $d^2$ to spare. Also $\mu=2\ell_\beta+2d\ge d$, as required in Step 1.
Step 3. The tail $\mathbb P(\mathrm{Bin}(N,\varepsilon)\le d-1)$ is non-increasing in $N$ (more trials, more successes), so every $N\ge\frac2\varepsilon(\ln\frac1\beta+d)$ satisfies $\mathbb P^N\{V(x^\star_N)\gt\varepsilon\}\le\beta$. This is the explicit condition of Campi, Garatti & Prandini (Annual Reviews in Control 2009) used as Theorem 1 by von Rohr et al. below. For $\varepsilon=0.05$, $\beta=10^{-5}$, $d=10$ it gives $N\ge 40\,(11.51+10)=860.5$, i.e. $N=861$: between the exact 581 and the 2006 value 1344, and available without solving anything. $\square$
Scenario design and Hoeffding validation in learning-based control (Trimpe group)
The scenario approach and a second elementary tool, Hoeffding’s inequality, are how the statistical bounds of Module 3 become controller certificates.
von Rohr, Neumann-Brosig & Trimpe, L4DC 2021 synthesise an LQR for a system whose linearised dynamics $[\bar A\ \bar B]$ carry a GP posterior. The initial gain solves a common-Lyapunov LMI over $M$ sampled models, a convex scenario program with $n_k=2d_x^2+d_xd_u$ decision variables, so Theorem 2.4 applies: with $M\ge\lceil\frac2\varepsilon(\ln\frac1\beta+n_k)\rceil$ samples from the (truncated) posterior, the gain stabilises all but an $\varepsilon$-fraction of the plausible models with confidence $1-\beta$ (their Theorem 1). Because the subsequent cost-improvement steps are no longer scenario programs, the final gain $K^\star$ is validated a posteriori: draw $M_{\rm val}$ fresh models, let $\phi_K=\mathbf 1[\rho(\bar A+\bar BK)\lt1]$, and accept if the empirical stability rate $\hat\phi$ is at least $1-\varepsilon$; Hoeffding then certifies a true rate of at least $1-\varepsilon-t$, where $t$ is the validation tolerance. This is a one-shot guarantee for a gain fixed before its validation models are drawn: if gains are re-proposed and re-validated until one passes, attempt $j$ needs its own failure budget $\alpha_j$ with $\sum_j\alpha_j\le\alpha$ (a union bound over attempts), because fresh data for each attempt do not remove the multiple-testing effect. Hertneck, Köhler, Trimpe & Allgöwer, L-CSS 2018 use the identical device to validate a neural approximation of a robust MPC: the indicator is “approximation error below the tolerance $\eta$ along the closed loop”, and $\mu\ge\tilde\mu-\sqrt{-\ln(\delta_h/2)/(2p)}$ with probability $1-\delta_h$ (Module 11).
The third pattern is to pass a statistical bound into a deterministic robust-synthesis tool: Fiedler, Scherer & Trimpe, CDC 2021 learn the unknown static nonlinearities of a plant by GP regression, convert the RKHS error tube $|\varphi(x)-\mu_D(x)|\le\beta_D\sigma_D(x)$ into sector bounds $[\hat\kappa_1,\hat\kappa_2]$ that contain the true sector with probability $1-\delta$, and feed those sectors as IQC multipliers into robust controller synthesis; with $n_p$ learned channels each receives $\delta/n_p$ (a union bound again), and the synthesised controller stabilises the true plant with robust performance with probability at least $1-\delta$ (their Theorem 1; Module 11), provided the loop signals stay in the interval on which the sectors were computed; otherwise the certificate is only local (Module 11 discusses this gap). Note that their Proposition 1, stated as a variant of the AAAI-2021 bound, prints $\beta_D=B+2R\sqrt{\log\det(K_D+\bar\lambda I)-2\log\delta}$, with $B$ a bound on the RKHS norm of the unknown function, $R$ the sub-Gaussian noise constant, $K_D$ the kernel matrix of the data, $\lambda\gt0$ the regularisation (the GP noise variance) and $\bar\lambda=\max\{1,\lambda\}$, whereas the corrected AAAI bound (arXiv v2) is $\beta_D=B+\frac{R}{\sqrt\lambda}\sqrt{\log\det(\frac{\bar\lambda}{\lambda}K_D+\bar\lambda I)-2\log\delta}$ (Module 3). For $\lambda\ge1$ the printed constant is the larger of the two, so it remains valid (only conservative); for $\lambda\lt\tfrac14$ it is smaller than the corrected one and no longer covered by the theorem. Use the corrected form when reproducing the pipeline.
7. Deterministic vs Probabilistic Guarantees: A Comparison
| Certificate | Type | Assumptions | What is certified | Cost | Representative papers |
|---|---|---|---|---|---|
| Complete verification (SMT / MILP / BaB) | Deterministic, exact | Piecewise-linear network, polyhedral input set | The property holds for all $x\in\mathcal X$, or a counterexample | Exponential worst case (counterexample search NP-complete, proving the property coNP-complete); practical with GPU BaB | Reluplex; Marabou 2.0; α,β-CROWN |
| Bound propagation (IBP, CROWN, α/β-CROWN) | Deterministic, sound, incomplete | Known weights; interval or linear relaxations of activations | A lower bound on the margin over $\mathcal X$ (verified if positive) | A few forward/backward passes; scales to millions of parameters | Gowal 2019; Zhang 2018; Xu 2021; Wang 2021 |
| SDP relaxation (DeepSDP, SDP-CROWN) | Deterministic, sound, incomplete | Quadratic constraints for input set, activations, specification | Reachable-set over-approximation; margins on $\ell_2$ balls | Interior point: $O(mn^3+m^2n^2+m^3)$ per iteration, practical up to a few thousand neurons; SDP-CROWN at bound-propagation cost (one extra scalar per layer) | Raghunathan 2018; Fazlyab 2022; Chiu 2025 |
| Lipschitz certificate (LipSDP, Lipschitz-by-design) | Deterministic, global | Slope-restricted activations; margin | Correct classification within radius margin$/(\sqrt2L)$ for every input | One SDP or zero at inference (by design) | Module 12, Module 13 |
| Randomized smoothing | Probabilistic (over Monte-Carlo sampling), $1-\alpha$ | None on $f$; Gaussian noise; $\ell_2$ threat model | The smoothed classifier is constant on an $\ell_2$ ball of radius $R$ | $10^4$–$10^5$ forward passes per input | Cohen 2019; Carlini 2023 |
| Conformal prediction | Probabilistic (marginal), $1-\alpha$ | Exchangeable calibration and test data; no feedback on the environment | Prediction set contains the truth; chance-constrained planning with union bound over time | One calibration pass; trivial online | Angelopoulos & Bates 2023; Lindemann 2023 |
| Scenario approach | Probabilistic, violation $\le\varepsilon$ w.p. $1-\beta$ | Convex program in the design; i.i.d. samples of the uncertainty | The design satisfies the constraint for all but an $\varepsilon$-mass of uncertainties | One convex program with $N\approx\frac2\varepsilon(\ln\frac1\beta+d)$ constraints | Calafiore & Campi 2006; Campi & Garatti 2008; von Rohr 2021 |
| Hoeffding validation | Probabilistic, $1-\alpha$ on a success rate | i.i.d. test scenarios; a checkable indicator | The true success rate is at least the empirical one minus $t$: $\mathbb E[\phi]\ge\hat\phi-t$ (one-sided; $|\hat\phi-\mathbb E[\phi]|\le t$ would need $M\ge\ln(2/\alpha)/(2t^2)$) | $M\ge\ln(1/\alpha)/(2t^2)$ closed-loop simulations | Hertneck 2018; von Rohr 2021 |
Open problems. (i) Verification of closed loops over long horizons still explodes: reachable sets must be over-approximated step by step, and the wrapping effect compounds exactly like IBP’s box (Module 14). (ii) Certified training has saturated for $\ell_\infty$ (about 35% on CIFAR-10 at $8/255$); the honest question is whether the threat model, not the method, is the bottleneck. (iii) Conformal guarantees under feedback and non-stationarity need either adaptive levels or explicit shift bounds, and neither gives finite-horizon safety of the kind the viability tools of Module 7 provide. (iv) Combining the two families, e.g. a deterministic reachability or robust-control certificate whose model error comes from a conformal, scenario or GP bound, is an active direction (the conformal planner of Lindemann et al. and the learning-enhanced synthesis of Fiedler, Scherer & Trimpe in Sections 5–6 are two instances), and it inherits the union bounds of both.
8. Walkthrough: IBP vs CROWN on a Two-Neuron Network
Every idea of Section 2 can be computed by hand on a 2-2-1 ReLU network. Take
with the $\ell_\infty$ box of radius $\varepsilon=1$ around $x_0=(1,1)$, i.e. $x\in[0,2]^2$. We want the range of $f$ over the box: a lower bound certifies $f\ge$ threshold, exactly the margin problem of Section 1. Step through the six tabs; the explorer below lets you change every weight and $\varepsilon$ and recomputes all bounds.
Neuron 2 is the only unstable one, so BaB splits the box once. On the sub-domain $\{z_2\ge 0\}$ the network is linear, $f=-2z_1+2z_2=-4x_1+2x_2$, and the split constraint $z_2(x)=-x_1+2x_2+1\ge 0$ enters as a multiplier $\beta\ge 0$ with sign $S=-1$:
For $0\le\beta\le1$ this is $-8+\beta$, for $1\le\beta\le4$ it is $-4-3\beta$ and for $\beta\ge4$ it is $4-5\beta$: concave and piecewise linear, increasing up to $\beta=1$ and decreasing after it, so maximised at $\beta=1$ with $g(1)=-7$. On the other sub-domain $\{z_2\le 0\}$, $f=-2z_1=-2x_1-2x_2-2$ and the constraint enters with $S=+1$: $g(\beta)=-8+\beta-|2\beta-2|$, i.e. $-10+3\beta$ for $\beta\le1$ and $-6-\beta$ for $\beta\ge1$, again maximised at $\beta=1$ with value $-7$. The minimum over the two sub-domains is $-7$, the exact minimum of $f$ on the box. With $\beta=0$ the two sub-domains return $-8$ and $-10$: plain CROWN uses the split only to fix the phase of neuron 2 (identity on one sub-domain, zero on the other) but still minimises over the whole box, so the branch does not improve on the unsplit bound $-8$ (taken naively, the minimum over the two sub-domains, $-10$, is even worse; BaB implementations keep the parent bound). With the optimal $\beta$ the LP-with-splits bound is recovered, as Theorem 3.2 of Wang et al. promises; and since every unstable neuron is now split, that LP is exact (Theorem 3.3).
Interactive: Output Bounds and Conformal Coverage
Panel A recomputes, for the 2-2-1 network and any weights you set, the IBP interval, adaptive CROWN, α-CROWN (the lower slopes optimised exactly: the bound is piecewise linear in $\alpha$, so an optimum occurs at an endpoint or a vertex of the partition into affine pieces), β-CROWN with complete branch and bound (every unstable neuron split, multipliers optimised exactly) and the exact range (enumeration of activation patterns, cross-checked on a $201\times201$ grid). Panel B simulates split conformal prediction with a seeded random generator. Try $W_{21}=W_{22}=0$ with $b_2=1$ (neuron 2 constant and stable), or large $\varepsilon$ (both neurons unstable, four sub-domains).
Left: the input box (blue) in $x$-space, the activation boundaries $z_1=0$ (purple) and $z_2=0$ (teal), the slice (orange, dashed), the exact minimiser (green dot) and the box corner where the CROWN lower bound is attained (orange square). Right: $f$ along the slice (blue) with the CROWN lower and upper linear bounds (orange) and the α-CROWN lower bound (purple, dashed), which stay on the correct side of $f$ everywhere in the box (a bound that is exact along the slice lies under the blue curve: with the default weights the CROWN lower line equals $f$ on the slice $x_2=1$, where neuron 2 is active); red dashed lines mark the IBP interval; the bars compare the five global intervals on the same vertical axis. β-CROWN BaB maximises the dual over the split multipliers exactly (the dual is piecewise linear, so vertex enumeration suffices) and is checked against the primal LP on every sub-domain.
Fact (derived here). Let a compact polytope $D$ be split into finitely many convex polytopes, and let $g$ be affine on each piece. Then the maximum and the minimum of $g$ over $D$ are attained at vertices of the pieces: every point of a piece is a convex combination of the piece’s vertices, an affine function takes the same combination of their values, and so its value lies between the smallest and the largest vertex value. A whole edge or piece may tie, but some vertex is always optimal. For $g(a)=-|2a-1|$ on $[0,1]$ the endpoints alone would miss the maximum at the kink $a=\tfrac12$.
Panel A uses this three times, with the intermediate bounds held fixed. (i) α-CROWN: the bound is affine in the free slopes as long as the coefficients inside the absolute values keep their signs. With one free slope the candidates are the endpoints of $[0,1]$ and the points where a coefficient vanishes; with two, the zero sets are lines that cut $[0,1]^2$ into polygons, and the candidates are the corners of the square and all pairwise intersections of these lines inside it. (ii) β-CROWN: the same enumeration for the multipliers on the orthant $\beta\ge0$; on a feasible sub-domain the dual is concave and bounded above by the primal minimum, so a vertex is again optimal, and the value is compared with the primal LP. (iii) Exact range: on each activation pattern the network is affine and the pattern’s region is the box clipped by the half-planes $z_j\ge0$ or $z_j\le0$, so evaluating $f$ at the vertices of these polygons suffices. The $201\times201$ grid is only a diagnostic (its minimum can exceed the true minimum and its maximum can fall below the true maximum), the plotted curve is a one-dimensional slice while the bars refer to the whole box, and everything runs in floating-point arithmetic, so the agreement shown is a numerical check, not a formally verified proof.
Left: the $n$ calibration scores, the quantile $\hat q$ (index $k=\lceil(n+1)(1-\alpha)\rceil$) and the coverage measured on 2000 fresh test scores. Right: for each $n$, 30 independent calibration sets (grey dots), their mean coverage (blue), the theoretical mean $k/(n+1)$ (dotted) and the band $[1-\alpha,\,1-\alpha+\tfrac{1}{n+1}]$ (green). The score distribution changes $\hat q$, i.e. the size of the prediction set (left), but for continuous scores neither the band nor the spread of the coverage (right). The simulation draws i.i.d. scores, so for $k\le n$ the coverage of a fixed calibration set is $F(s_{(k)})\sim\mathrm{Beta}(k,\,n+1-k)$ whatever the continuous score CDF $F$ is, and switching the distribution only reshuffles the grey dots. For $k=n+1$, i.e. $(n+1)\alpha\lt 1$, $\hat q=\infty$ and the coverage is identically 1, with no spread. The “three standard errors” use the exact beta-binomial variance $p(1-p)(n+1+2000)/(2000\,(n+2))$ of one run, $p=k/(n+1)$, divided by the 30 runs.
The three score distributions are generated from independent standard normals $Z,Z_0,Z_1,Z_2,Z_3$. Gaussian: $|Z|$. Student-t with 3 degrees of freedom: $|Z_0|/\sqrt{(Z_1^2+Z_2^2+Z_3^2)/3}$; the three squared normals in the denominator are the three degrees of freedom, and because the denominator is itself random and occasionally small (a numerator of 1 over a denominator of 0.1 gives a score of 10), very large scores are far more frequent than under Gaussian noise: the distribution has heavy tails. Mixture (Primer C): with probability $0.8$ draw $|0.5Z|$, otherwise $|3Z|$. All three are continuous, so the rank argument and the Beta law of Section 5 hold for each; only the scale and the tail change, and with them the size of the prediction sets.
Let $C$ be the coverage of one calibration set, a random variable, and $\hat C$ its measured coverage on $m=2000$ fresh test scores. For continuous i.i.d. scores and $k\le n$, $C\sim\mathrm{Beta}(k,n+1-k)$ (Section 5) and, given $C$, $m\hat C\sim\mathrm{Bin}(m,C)$: a binomial count whose success probability is itself Beta-distributed, called a beta-binomial count. With $p=k/(n+1)$, $\operatorname{Var}(C)=p(1-p)/(n+2)$ and $\mathbb E[C(1-C)]=\mathbb E[C]-\mathbb E[C]^2-\operatorname{Var}(C)=p(1-p)(n+1)/(n+2)$. The law of total variance (Primer C),
shows that the calibration and test-sampling variances add; standard deviations do not, which is why the readout adds the two variances before taking a square root. Averaging 30 independent runs divides the variance by 30, and the plotted check uses three times the resulting standard error: a simulation diagnostic, not a deterministic band or an exact confidence statement. Example: $n=99$, $\alpha=0.1$, so $k=90$, $p=0.9$, $m=2000$: $\operatorname{Var}(\hat C)\approx0.000936$, and the standard error of a 30-run mean is about $0.0056$.
From the mathematics to a real decision
Learning objectives
- Verify a concrete neural output specification by enumerating its linear regions.
- Interpret a loose interval bound as unresolved rather than as a physical counterexample.
- Combine deterministic network bounds with marginal statistical coverage without changing either guarantee.
A commissioning decision
A controller predicts a next temperature by adding a neural correction to a nominal thermal model. Let the dimensionless sensor feature lie in $z\in[-0.3,0.4]$ and let the correction, measured in degrees Celsius, be
The numerical coefficients include the conversion from normalized features to degrees. The proposed nominal prediction is 59.65 degrees, and the desired specification is $59.65+n(z)\le60$ for every allowed feature. Assume this network is implemented exactly, the input interval is justified independently, and the nominal-plus-network expression initially describes the entire prediction. This is a verification question about a fixed function over a fixed set.
A later residual-calibration step will add model discrepancy. Keeping that step separate lets us see exactly what deterministic verification proves before a statistical assumption enters. An output enclosure is useful only when its direction matches the requested specification: here we need a sound upper bound, because larger temperature is worse.
Worked decision, with its limits
Try interval propagation. The first hidden output lies in $[0,0.6]$ and the second in $[0,0.3]$. Combining these intervals independently yields $n(z)\in[-0.6,0.6]$. The corresponding temperature upper bound is 60.25 degrees, so this inexpensive calculation cannot approve the proposal. It does not provide an input that produces overheating.
Preserve the shared input. Split at the ReLU breakpoints $z=-0.2$ and $z=0.1$. On $[-0.3,-0.2]$, both hidden units are zero, so $n=0$. On $[-0.2,0.1]$, only the first is active, so $n=z+0.2$. On $[0.1,0.4]$, both are active, giving $n=0.4-z$. The exact range is $[0,0.3]$, with the maximum attained at $z=0.1$.
Make the deterministic decision. The actual upper temperature in this model is $59.65+0.3=59.95$ degrees. Every allowed input passes, with 0.05 degrees of margin. The interval calculation lost correlation between two hidden outputs driven by the same scalar. Splitting restores the relevant relationship and converts “unresolved” into a certificate.
Now include a different uncertainty source. Suppose an additional physical prediction residual $r$ remains. A score $|r|$ was fixed before calibration, and 19 calibration examples together with the next test example are exchangeable. At miscoverage level 0.1, split conformal uses order $k=\lceil20(0.9)\rceil=18$. Suppose the sorted scores are 0.01 through 0.16 in increments of 0.01, followed by 0.22, 0.24, and 0.30 degrees. Then the calibration radius is 0.24 degrees.
The original proposal now has upper temperature $59.65+0.3+0.24=60.19$ on the residual-coverage event and must be revised. A nominal prediction at most $60-0.3-0.24=59.46$ passes that robust inequality. The residual interval has at least 90% marginal coverage over calibration and test examples under exchangeability; it is not a deterministic bound on every future residual or a conditional guarantee for every selected input.
A tempting wrong approach
The neural correction is zero at both input endpoints $-0.3$ and 0.4, but reaches 0.3 inside the interval. Endpoint evaluation is exact for an affine function on an interval, not for an arbitrary piecewise-affine network. A grid can also miss a narrow interior peak. Here the breakpoint enumeration supplies an exhaustive argument; its completeness is what makes the maximum useful for approval.
Transfer the argument
Exercise 15.B1 — Medium: Reverify after the input envelope changes
A new sensor calibration gives $z\in[-0.1,0.5]$. Find the exact correction range and decide whether a nominal temperature of 59.7 degrees satisfies the deterministic specification. Exclude the additional residual for this exercise.
Review: ReLU relaxation and branching.
Show hint
The first ReLU is active everywhere on the new interval. Split only at 0.1.
Show worked solution
On $[-0.1,0.1]$, $n=z+0.2$ ranges from 0.1 to 0.3. On $[0.1,0.5]$, $n=0.4-z$ ranges from 0.3 down to $-0.1$. Thus the exact range is $[-0.1,0.3]$. The upper predicted temperature is 60.0 degrees, which satisfies the stated non-strict limit. It has zero certified margin and would fail a requirement of strict separation or any unbudgeted positive implementation error. The old minimum zero cannot be reused after changing the input domain.
Exercise 15.B2 — Hard: Calibrate a whole ten-step forecast
For a ten-minute forecast, use the single trajectory score $s=\max_{1\le t\le10}|r_t|$. Require marginal coverage at least 0.99 for the whole residual trajectory. Find the smallest calibration size permitting a finite split-conformal quantile. At that size suppose the chosen quantile is 0.32 degrees. Does nominal temperature 59.35 degrees at every step pass with the same neural upper bound 0.3?
Review: Trajectory-level conformal scores.
Show hint
The order is $\lceil(n+1)0.99\rceil$; it must not exceed $n$. Calibration examples must be entire exchangeable trajectories.
Show worked solution
A finite quantile requires $0.99(n+1)\le n$, equivalently $n\ge99$. At $n=99$, the order is 99, the largest calibration trajectory score. On the event $s\le0.32$, every step has residual magnitude at most 0.32, so each upper temperature is $59.35+0.3+0.32=59.97$ degrees. Under exchangeability of the 99 calibration trajectories and the next trajectory, the event has marginal probability at least 0.99. Calibrating individual time points at 99% separately would not yield the same joint statement; a ten-step union bound would only ensure 90% without an adjusted budget.
Synthesis and bridge
The complete argument contains two different pieces of evidence: a universal neural output bound on a specified input set and a marginal residual-coverage statement under exchangeability. Combining them requires an explicit implication from the coverage event to the physical constraint. Neither piece acquires stronger quantifiers merely because they appear in one controller.
Across the book, the recurring task is to connect a precise mathematical object to a decision the model actually supports. Before approving a learned robot or thermal controller, trace that connection from sensors and units through model uncertainty, admissible actions, and future trajectories. The open problems are opportunities to strengthen specific links in that chain.
Exercises
Turn a two-logit label claim into one scalar inequality. For a probabilistic statement, name the certified object, the sampling experiment and the failure event. Explain why a positive relaxed upper bound is inconclusive.
If this is difficult, revisit the earlier prerequisite, work the Easy questions, and return to the linked section. You can postpone the advanced extensions while building confidence with the core certificate.
Graded practice: build the calculation, then audit the claim
These twelve new questions each include an independent hint and a fully worked solution. The difficulty measures the amount of reasoning, not the amount of notation. The original research exercises follow below.
Easy: read definitions and compute
Easy 1 — Turn a label claim into a scalar specification
On $x\in[0,1]$, logits are $f_1(x)=2x+1$ and $f_2(x)=-x+2$. Write the specification for class 1 to beat class 2, find its worst case, and give a counterexample. If an incomplete verifier returns upper bound $1.4$, does that number alone prove failure?
Review if needed: Primer 0: maxima and bounds; this module's relevant section.
Hint
The scalar violation objective is $f_2-f_1$, not $f_1-f_2$.
Worked solution
Step 1. The violation is $p(x)=f_2(x)-f_1(x)=1-3x$, which is largest at $x=0$, with $p^\star=1$. Thus the desired property fails.
Step 2. The input $x=0$ is an explicit counterexample: the logits are $(1,2)$ and class 2 wins.
Step 3. An upper bound $\bar p=1.4\gt0$ by itself says only that the relaxation did not verify the property. Here failure is established by the actual input and its forward evaluation, not by the positive upper bound.
Easy 2 — One affine interval and one ReLU
For $x_1\in[1,2]$, $x_2\in[-1,1]$, find the exact interval for $z=2x_1-3x_2+1$ and its ReLU output. Give input corners attaining the two endpoints.
Review if needed: Primer 0: maxima and bounds; this module's relevant section.
Hint
Positive coefficients maximize at the upper input endpoint; negative coefficients maximize at the lower endpoint.
Worked solution
Step 1. The minimum is $2(1)-3(1)+1=0$, attained at $(1,1)$. The maximum is $2(2)-3(-1)+1=8$, attained at $(2,-1)$. Hence $z\in[0,8]$.
Step 2. ReLU is monotone, so its output interval is $[\operatorname{ReLU}(0),\operatorname{ReLU}(8)]=[0,8]$. This neuron is stable active, including its zero boundary.
Step 3. In centre-radius form the input centre is $(1.5,0)$ and radius $(0.5,1)$; the pre-activation centre is $4$ and radius $2(0.5)+3(1)=4$, giving the same result.
Easy 3 — An unstable ReLU triangle
On $z\in[-2,3]$ write the chord upper bound and choose lower line $h_L(z)=0.4z$. Check both inequalities at $z=-1$ and $z=1$. Why is a negative lower-line value allowed?
Review if needed: Primer B: convex relaxations; this module's relevant section.
Hint
The chord joins $(-2,0)$ to $(3,3)$. A lower bound need not be an attainable activation value.
Worked solution
Step 1. The chord is $h_U(z)=\frac35(z+2)$. At $z=-1$, $h_L=-0.4\le0=\operatorname{ReLU}(-1)\le0.6=h_U$.
Step 2. At $z=1$, $h_L=0.4\le1\le1.8=h_U$. More generally, $0\le0.4\le1$ makes $0.4z$ a valid ReLU lower line across the entire interval.
Step 3. A relaxation encloses the true graph and may include artificial points. A negative lower value is conservative, while a lower value above the actual ReLU would be unsound.
Easy 4 — Choose the conformal order statistic
Nine calibration scores sorted increasingly are $0.1,0.2,\ldots,0.9$. At miscoverage level $\alpha=0.2$, compute the split-conformal index and threshold. For absolute-error scores and prediction $\hat y=2$, write the prediction interval.
Review if needed: Primer C: binomial tails and exchangeability; this module's relevant section.
Hint
Use $k=\lceil(n+1)(1-\alpha)\rceil$, with $n+1$, not $n$.
Worked solution
Step 1. $k=\lceil10(0.8)\rceil=8$, so the threshold is the eighth calibration score, $\hat q=0.8$.
Step 2. The set $|y-2|\le0.8$ is the interval $[1.2,2.8]$. The endpoints are included because the conformal set uses $\le$.
Step 3. With a score fixed before calibration and exchangeable calibration/test examples, the marginal coverage is at least $0.8$. The theorem averages over calibration and test randomness; it is not a guarantee at each individual input.
Medium: connect two or three steps
Medium 1 — Interval independence can invent an impossible output
For $x\in[-1,1]$, let $a_1=\operatorname{ReLU}(x)$, $a_2=\operatorname{ReLU}(x)$, $f=a_1-a_2$. Compute the IBP output interval and the exact output set. What information did IBP discard?
Review if needed: Primer A: matrix arithmetic; this module's relevant section.
Hint
The two activation intervals are identical, but their values cannot be chosen independently.
Worked solution
Step 1. Each hidden interval is $[0,1]$. Treating them as independent gives $f\in[0-1,1-0]=[-1,1]$.
Step 2. The exact network always has $a_1=a_2$, so $f(x)=0$ and the exact output set is $\{0\}$.
Step 3. IBP kept coordinate ranges and forgot equality between the coordinates. It remains sound because $\{0\}\subset[-1,1]$. A relaxation preserving this equality, or algebraic cancellation before bounding, recovers the tighter result.
Medium 2 — Select a CROWN line by the output sign
Let $f(z)=1-2\operatorname{ReLU}(z)$ on $[-1,2]$, with upper chord $h_U(z)=\frac23(z+1)$ and lower line $h_L=0$. Which line gives an upper bound on $f$, and which a lower bound? Show at $z=-1/2$ why using $1-2h_U$ as an upper bound fails.
Review if needed: Primer 0: signed arithmetic and inequalities; this module's relevant section.
Hint
Multiplying an activation inequality by $-2$ reverses its direction.
Worked solution
Step 1. From $h_L\le\operatorname{ReLU}(z)\le h_U$ we get $1-2h_U\le f(z)\le1-2h_L=1$. Thus the lower activation line supplies the upper output bound.
Step 2. The lower output line is $1-\frac43(z+1)$, whose minimum on the interval is $-3$ at $z=2$. The exact function ranges from $-3$ to $1$, so both final scalar bounds are tight here.
Step 3. At $z=-1/2$, the actual output is $1$, while $1-2h_U=1-2(1/3)=1/3$. It cannot be an upper bound on a value equal to $1$; it is a valid lower bound.
Medium 3 — A smoothing radius and its confidence statement
An independent Monte-Carlo confidence procedure returns $\underline p_A=\Phi(2)\approx0.977249868$ at confidence $99.9\%$, with Gaussian noise scale $\sigma=0.5$. Compute the certified Euclidean radius and a sufficient infinity-norm radius in dimension $100$. What happens if the lower bound is instead $0.5$?
Review if needed: Primer C: Gaussian quantiles; this module's relevant section.
Hint
The single-probability rule is $R=\sigma\Phi^{-1}(\underline p_A)$.
Worked solution
Step 1. Because $\Phi^{-1}(\Phi(2))=2$, the Euclidean radius is $R=0.5(2)=1$. On the confidence event, the ideal smoothed classifier keeps label $A$ for all perturbations with Euclidean norm strictly below $1$.
Step 2. $\|\delta\|_2\le\sqrt{100}\|\delta\|_\infty=10\|\delta\|_\infty$, so a sufficient strict infinity-norm radius is $0.1$.
Step 3. The confidence is over the probability-estimation samples, and the certified object is the smoothed classifier. If $\underline p_A=0.5$, the rule produces zero radius and CERTIFY abstains; it does not supply a positive-radius certificate.
Medium 4 — Validation needs a sampling margin
A fixed controller is evaluated on fresh i.i.d. trials with a success indicator in $[0,1]$. At one-sided confidence $99\%$ and tolerance $t=0.1$, compute the sufficient Hoeffding sample size. If the observed success fraction is $0.98$, what population success lower bound follows? Can this tolerance certify target success $0.95$?
Review if needed: Primer C: confidence events and union bounds; this module's relevant section.
Hint
Use $M\ge\ln(1/\alpha)/(2t^2)$ and subtract $t$ from the observed fraction.
Worked solution
Step 1. Here $\alpha=0.01$, so $M\ge\ln100/0.02\approx230.25851$. The integer sample count is at least $231$.
Step 2. With probability at least $0.99$, the population success probability is at least $\hat\phi-t=0.98-0.1=0.88$. The observed fraction itself is not the population guarantee.
Step 3. To certify population success $0.95$ with this tolerance would require $\hat\phi\ge1.05$, which is impossible. Reduce $t$ and increase the sample size; keep validation independent of controller selection or account for selection explicitly.
Hard: combine calculations with assumptions
Hard 1 — The same affine bound over different input balls
A backward relaxation yields the exact affine expression $g(x)=3x_1-4x_2+2$. Around $x_0=(1,2)$ with radius $\varepsilon=0.2$, compute its ranges for Euclidean and infinity-norm input balls, and give perturbations attaining the lower endpoints. Explain why the radii cannot be exchanged unchanged.
Review if needed: Primer A: norm comparisons and dual norms; this module's relevant section.
Hint
The dual norms of the coefficient row $(3,-4)$ are $5$ for an $\ell_2$ ball and $7$ for an $\ell_\infty$ ball.
Worked solution
Step 1. The centre value is $3-8+2=-3$. On the Euclidean ball, the deviation is bounded by $0.2\sqrt{3^2+(-4)^2}=1$, so the exact range is $[-4,-2]$. The lower endpoint is attained by $\delta=-0.2(3,-4)/5=(-0.12,0.16)$.
Step 2. On the infinity-norm ball, the deviation is $0.2(|3|+|-4|)=1.4$, giving $[-4.4,-1.6]$. The minimizing perturbation is $\delta=(-0.2,0.2)$, choosing the sign against each coefficient.
Step 3. The infinity-norm ball with the same numerical radius contains vectors with larger Euclidean norm. The correct dual norm is part of the specification; reusing the Euclidean bound unchanged on that larger set would miss attainable values.
Hard 2 — A trajectory budget and finite calibration resolution
For four future times you want total miscoverage at most $0.1$. Allocate equal per-time budgets and compute the conformal order index for $n=39$ and for $n=19$ calibration trajectories. Would using $90\%$ marginal coverage at every time alone imply $90\%$ joint coverage?
Review if needed: Primer C: confidence events and union bounds; this module's relevant section.
Hint
Use a union bound, then compare $k=\lceil(n+1)(1-\alpha)\rceil$ with $n$.
Worked solution
Step 1. Choose per-time miscoverage $\alpha=0.1/4=0.025$. Then the union bound gives joint coverage at least $1-4(0.025)=0.9$ without requiring independence between times.
Step 2. For $n=39$, $k=\lceil40(0.975)\rceil=39$, so the threshold is the largest observed score. For $n=19$, $k=\lceil20(0.975)\rceil=20\gt19$, so the valid threshold is $+\infty$; the data cannot supply a finite threshold at this nominal resolution.
Step 3. Four marginal $90\%$ statements give only the union-bound lower bound $1-4(0.1)=0.6$. Even independent $90\%$ coverage events would have joint probability $0.9^4=0.6561$, not $0.9$. A horizon guarantee needs its own budget and the exchangeability assumptions.
Hard 3 — Compare an exact scenario tail with an explicit bound
A scenario program meets the theorem assumptions with $d=3$, target violation $\varepsilon=0.1$ and design failure probability $\beta=0.05$. Compute the explicit sufficient integer count from $N\ge\frac2\varepsilon(\ln(1/\beta)+d)$. Check the exact binomial tail at $N=60$ and $61$. State what probability is bounded.
Review if needed: Primer C: binomial tails and exchangeability; this module's relevant section.
Hint
For $d=3$, sum the binomial probabilities for $i=0,1,2$. The outer randomness is the design sample.
Worked solution
Step 1. The explicit rule gives $N\ge20(\ln20+3)\approx119.91465$, so $N=120$ suffices.
Step 2. The exact tail is $S_N=0.9^N+N(0.1)0.9^{N-1}+\binom N2(0.1)^2 0.9^{N-2}$. It gives $S_{60}\approx0.05304508\gt0.05$ and $S_{61}\approx0.04911828\le0.05$. The tail decreases with $N$, so $61$ is the smallest admissible count.
Step 3. The theorem states that, with probability at least $0.95$ over the sampled design constraints, the returned solution has population violation probability at most $0.1$. It does not prove zero violation for every uncertainty realization; convexity, feasibility/solution assumptions and matching i.i.d. deployment sampling remain necessary.
Hard 4 — Conditioning on planner feasibility changes the bound
A conformal planning argument proves $\mathbb P(\text{feasible and unsafe})\le0.04$, while $\mathbb P(\text{feasible})=0.5$. What upper bound follows on failure conditional on feasibility? Does the argument prove unconditional safety at least $0.96$ if behavior on infeasible runs is unspecified?
Review if needed: Primer C: conditional probability; this module's relevant section.
Hint
Use the definition of conditional probability; the event inclusion controls only one part of all runs.
Worked solution
Step 1. $\mathbb P(\text{unsafe}\mid\text{feasible})=\mathbb P(\text{unsafe and feasible})/0.5\le0.04/0.5=0.08$. Thus the conditional safety lower bound from these facts is $0.92$.
Step 2. Infeasible runs have probability $0.5$ and may all be unsafe. The given facts alone therefore permit unconditional unsafe probability as high as $0.5+0.04=0.54$, yielding only the lower bound $0.46$ on safety.
Step 3. To obtain the intended unconditional safety statement, prove almost-sure feasibility or add a certified safe fallback for infeasible cases. Simply discarding infeasible runs changes the probability space and does not preserve the original $0.96$ claim.
Original research exercises
Continue here when the core calculations and the certificate assumptions are clear. Use the graded questions above as a warm-up; the original derivations below remain available in full.
Key Papers
| Paper | Venue | Contribution | Why read it |
|---|---|---|---|
| Zhang, Weng, Chen, Hsieh & Daniel — Efficient Neural Network Robustness Certification with General Activation Functions (CROWN) | NeurIPS 2018 | Linear upper/lower relaxations of any activation on its pre-activation interval, back-substituted layer by layer into closed-form output bounds (Theorem 3.2, Corollary 3.3). | The backward pass that auto_LiRPA and α,β-CROWN run; the walkthrough is Theorem 3.2 for $m=2$. |
| Gowal et al. — On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models | ICCV 2019 (as “Scalable Verified Training for Provably Robust Image Classification”) | IBP with the $|W|$ rule, elision of the last layer, and the mixed loss with $\kappa$/$\varepsilon$ curricula that makes IBP bounds tight after training. | The simplest sound bound, and the reason tuned IBP is still within 0.13 pp of the best certified training at $8/255$ in 2025. |
| Wang, Zhang, Xu, Lin, Jana, Hsieh & Kolter — Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification | NeurIPS 2021 | Split constraints of branch and bound as optimisable Lagrange multipliers inside bound propagation; equals the LP-with-splits bound on an $\ell_\infty$ box (Theorem 3.2) and is sound and complete with BaB (Theorem 3.3). | The engine of α,β-CROWN; the derivation in Section 2.3 and the “going deeper” box reproduce it on two neurons. |
| Kaulen et al. — The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results | arXiv 2512.19007 (2025) | Standardised benchmarks (ONNX/VNN-LIB, equal hardware); overall ranking α,β-CROWN 1566.9, NeuralSAT 1430.2, PyRAT 1228.4, CORA 987.2. | What state of the art means for verifiers; the benchmark suite is the de-facto test bed for control-relevant networks too. |
| Mao, Balauca & Vechev — CTBench: A Library and Benchmark for Certified Training | ICML 2025 (PMLR 267); arXiv 2406.04848 | Equal-tuning re-evaluation of IBP, CROWN-IBP, SABR, TAPS, STAPS, MTL-IBP; certified accuracy saturates near 35% on CIFAR-10 at $8/255$ (MTL-IBP 35.41%, tuned IBP 35.28%). | The honest baseline for any claim about certified training progress. |
| Katz, Barrett, Dill, Julian & Kochenderfer — Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks | CAV 2017 | Simplex extended with lazy ReLU case splitting; NP-completeness of finding a counterexample (so proving a property is coNP-complete); ACAS Xu verified. | The complete-verification landmark and the hardness result that frames every relaxation. |
| Fazlyab, Morari & Pappas — Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming (DeepSDP) | IEEE TAC 2022 | QC abstraction of input set, activations and specification; S-procedure LMI certifies output bounds and reachable-set over-approximations. | The control-theoretic verification template; contrast its single-point coupled multipliers with LipSDP’s incremental ones. |
| Raghunathan, Steinhardt & Liang — Certified Defenses against Adversarial Examples | ICLR 2018 | Gradient-norm bound relaxed to a MAXCUT-style SDP for one-hidden-layer networks, trained against its own dual certificate. | The first SDP certificate; the lifting $P=yy^{\top}$ is the prototype of every later SDP relaxation. |
| Chiu, Chen, Zhang & Zhang — SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming | ICML 2025 | An SDP-derived linear relaxation for $\ell_2$ input sets with one scalar per layer, up to $\sqrt n$ tighter than box-based bounds, inside α-CROWN at 65k neurons. | Where the SDP line and the bound-propagation line meet. |
| Cohen, Rosenfeld & Kolter — Certified Adversarial Robustness via Randomized Smoothing | ICML 2019 | Tight $\ell_2$ radius $\tfrac\sigma2(\Phi^{-1}(\underline{p_A})-\Phi^{-1}(\overline{p_B}))$ via Neyman–Pearson; PREDICT/CERTIFY with statistical guarantees; first ImageNet-scale certificate. | The cleanest proof in the certified-robustness literature; every smoothing result builds on Theorem 1. |
| Carlini, Tramèr, Dvijotham, Rice, Sun & Kolter — (Certified!!) Adversarial Robustness for Free! | ICLR 2023 | Off-the-shelf diffusion denoiser plus off-the-shelf classifier inside randomized smoothing: 71.1% certified ImageNet top-1 at radius 0.5 without training. | Shows how far the “any base classifier” clause of Theorem 1 can be pushed. |
| Angelopoulos & Bates — Conformal Prediction: A Gentle Introduction (journal title; the arXiv preprint is titled “A Gentle Introduction to Conformal Prediction and Distribution-Free Uncertainty Quantification”, and the appendix numbers on this page follow it) | Found. Trends ML 16(4):494–591, 2023 | Split conformal prediction with the coverage theorem, its proof, conditional-coverage caveats and extensions (risk control, shift). | The standard entry point; Appendix D is the proof reproduced in Section 5. |
| Lindemann, Cleaveland, Shim & Pappas — Safe Planning in Dynamic Environments Using Conformal Prediction | IEEE RA-L 8(8), 2023 | Conformal regions on trajectory-prediction errors, union bound over the horizon, Lipschitz-tightened MPC constraints with open- and closed-loop guarantees. | The template for conformal guarantees in control and the source of its conservatism (Assumption 1, $\delta/T$). |
| Campi & Garatti — The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs | SIAM J. Optim. 19(3), 2008 | Distribution-free binomial-tail bound on the violation probability of scenario solutions, exact for fully supported problems; $N=581$ instead of $1344$ in the reference example. | The sharp result behind scenario-based robust design and the explicit $\tfrac2\varepsilon(\ln\tfrac1\beta+d)$ rule. |
| von Rohr, Neumann-Brosig & Trimpe — Probabilistic Robust Linear Quadratic Regulators with Gaussian Processes | L4DC 2021, PMLR 144 | Scenario common-Lyapunov LMI on GP-sampled models with an a-priori guarantee, iterative improvement and Hoeffding validation. | A compact worked example of scenario plus Hoeffding in learning-based control; read it with the two corrections of Section 6. |