Lipschitz-margin certified robustness radius (Tsuzuku–Sato–Sugiyama 2018)

The verification payoff behind the mnist-{linear,mlp,cnn}-pgd demos (planning/archive/robustness.md, planning/archive/robustness_ladder.md): the certificate — the lower bound of the cert ≤ TRUE ≤ PGD sandwich — turned from a number into a theorem.

The classifier's logit map f : ℝ^d → ℝ^k is L-Lipschitz in L2. At an input x, the margin is m = f(x)_{top} − f(x)_{runner-up}. The theorem: every perturbation δ with ‖δ‖₂ < m / (√2·L) leaves the argmax class unchanged — a provable safe radius against all attacks (vs PGD, which only finds one). The √2 is the L2 distance ‖eᵢ − eⱼ‖₂ between two one-hot class directions: a pairwise logit gap is (√2·L)-Lipschitz.

The L is supplied numerically by specNormW / specNormConvTapSum (LeanMlir/VerifiedTrain.lean); lipschitzL2_comp + clm_lipschitzL2 show why the naive per-layer product L = ∏ᵢ ‖Wᵢ‖₂ is a sound (if loose) global constant — the looseness the demos make visual (linear tight → MLP/CNN vacuous).

The second half of the file formalizes the other certificate — randomized smoothing (Cohen–Rosenfeld–Kolter 2019, the *-smooth demos): smoothing_certified_radius gives the σ·Φ⁻¹(p_A) radius the driver reports, as the same Lipschitz-margin argument on the per-class probit score fields Φ⁻¹∘P[f(x+η)=·] — depth-independent, non-vacuous where the product collapses. smoothing_certified_radius_probit is the Ioo (0,1) variant that the REAL Gaussian quantile can instantiate (SmoothingGaussian.lean discharges its hmono/hanti at the true Φ⁻¹).

All results are propext / Classical.choice / Quot.sound-clean (tests/AuditAxioms.lean).

def Proofs.LipschitzL2 {α : Type u_1} {β : Type u_2} [NormedAddCommGroup α] [NormedAddCommGroup β] (L : ℝ) (f : α → β) : Prop

f is L-Lipschitz in the (L2) norm: ‖f u − f w‖ ≤ L · ‖u − w‖. The explicit ε–δ form (vs Mathlib's LipschitzWith, which is ℝ≥0∞-valued) — it reads like the math and composes by plain arithmetic.

Equations

• Proofs.LipschitzL2 L f = ∀ (u w : α), ‖f u - f w‖ ≤ L * ‖u - w‖

theorem Proofs.LipschitzL2.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [NormedAddCommGroup α] [NormedAddCommGroup β] [NormedAddCommGroup γ] {Lg Lh : ℝ} {g : β → γ} {h : α → β} (hg : LipschitzL2 Lg g) (hh : LipschitzL2 Lh h) (hLg : 0 ≤ Lg) : LipschitzL2 (Lg * Lh) (g ∘ h)

Composition multiplies Lipschitz constants: g ∘ h is (Lg·Lh)-Lipschitz. This is exactly the per-layer product bound L = ∏ᵢ ‖Wᵢ‖₂ — sound, and (past one layer) loose by construction, the depth-cliff the PGD demos expose.

theorem Proofs.clm_lipschitzL2 {α : Type u_1} {β : Type u_2} [NormedAddCommGroup α] [NormedSpace ℝ α] [NormedAddCommGroup β] [NormedSpace ℝ β] (A : α →L[ℝ] β) : LipschitzL2 ‖A‖ ⇑A

A continuous linear map A (a net's affine layer, bias dropped) is ‖A‖-Lipschitz — and for a weight matrix the operator norm ‖A‖ is the spectral norm ‖W‖₂ that specNormW estimates by power iteration. So each linear layer contributes its spectral norm to the product.

theorem Proofs.euclid_norm_sq {k : ℕ} (v : EuclideanSpace ℝ (Fin k)) : ‖v‖ ^ 2 = ∑ i : Fin k, v.ofLp i ^ 2

‖v‖² = Σᵢ (vᵢ)² on EuclideanSpace ℝ (Fin k) (unfold the L2 norm).

theorem Proofs.coord_pair_bound {k : ℕ} (v : EuclideanSpace ℝ (Fin k)) {i j : Fin k} (hij : i ≠ j) : (v.ofLp i - v.ofLp j) ^ 2 ≤ 2 * ‖v‖ ^ 2

Two distinct coordinates of v carry at most 2‖v‖² of squared mass: (vᵢ − vⱼ)² ≤ 2‖v‖². Equivalently |vᵢ − vⱼ| ≤ √2·‖v‖ — the √2 in the radius.

theorem Proofs.logit_gap_stable {k : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : E → EuclideanSpace ℝ (Fin k)} {L : ℝ} (hf : LipschitzL2 L f) (x δ : E) {i j : Fin k} (hij : i ≠ j) : (f x).ofLp i - (f x).ofLp j - √2 * L * ‖δ‖ ≤ (f (x + δ)).ofLp i - (f (x + δ)).ofLp j

Pairwise logit gaps are (√2·L)-stable. Perturbing the input by δ moves the gap f(·)ᵢ − f(·)ⱼ (any two classes) down by at most √2·L·‖δ‖: f(x)ᵢ − f(x)ⱼ − √2·L·‖δ‖ ≤ f(x+δ)ᵢ − f(x+δ)ⱼ. The engine of the certificate.

theorem Proofs.lipschitz_margin_certified_radius {k : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : E → EuclideanSpace ℝ (Fin k)} {L : ℝ} (hf : LipschitzL2 L f) (hL : 0 < L) {x δ : E} {i : Fin k} {m : ℝ} (hmargin : ∀ (j : Fin k), j ≠ i → m ≤ (f x).ofLp i - (f x).ofLp j) (hδ : ‖δ‖ < m / (√2 * L)) (j : Fin k) : j ≠ i → (f (x + δ)).ofLp j < (f (x + δ)).ofLp i

Lipschitz-margin certified radius (Tsuzuku et al. 2018). If the logit map f is L-Lipschitz in L2 (L > 0), class i leads every other class at x by at least the margin m (hmargin), and ‖δ‖₂ < m / (√2·L), then i still strictly leads every other class at x + δ — the prediction provably cannot flip inside the L2 ball of radius m / (√2·L), against any attack.

The other certificate of the cifar-smooth / mnist-{mlp,cnn}-smooth demos — the one that stays non-vacuous where the Lipschitz product collapses. The smoothed classifier ĝ(x) = argmax_c P[f(x+η)=c], η ~ N(0,σ²I), is certifiably robust in L2 with radius σ·Φ⁻¹(p_A) (the radius the driver reports). The proof factors exactly like the Tsuzuku theorem: a Lipschitz-margin argument over per-class probit score fields

gᶜ(x) = Φ⁻¹(P[f(x+η)=c]),

each of which is (1/σ)-Lipschitz. That (1/σ)-Lipschitzness is the analytic heart of Cohen 2019 (Neyman–Pearson over the Gaussian likelihood ratio; equivalently Gaussian isoperimetry, Salman et al. 2019 Lemma 2) — it is taken here as the hypothesis hg, in exactly the way lipschitz_margin_certified_radius takes the logit-map Lipschitz constant L as a hypothesis rather than re-deriving the spectral norms. Given it, the certified radius is pure margin algebra: no Gaussian measure theory leaks past the hypothesis, and the result is Classical-clean.

theorem Proofs.smoothed_margin_certified_radius {k : ℕ} {E : Type u_1} [NormedAddCommGroup E] {σ : ℝ} (hσ : 0 < σ) {g : Fin k → E → ℝ} (hg : ∀ (c : Fin k), LipschitzL2 (1 / σ) (g c)) {x δ : E} {i : Fin k} {m : ℝ} (hmargin : ∀ (j : Fin k), j ≠ i → m ≤ g i x - g j x) (hδ : ‖δ‖ < σ * m / 2) (j : Fin k) : j ≠ i → g j (x + δ) < g i (x + δ)

Core smoothing margin step. If the smoothed classifier's per-class probit score fields g c are each (1/σ)-Lipschitz in L2 (hg — the Cohen/Salman Gaussian content), and class i leads every other class in probit score at x by margin m, then for every ‖δ‖₂ < σ·m/2 it still leads at x+δ. The radius is σ·m/2; with m = Φ⁻¹(p_A)−Φ⁻¹(p_B) this is Cohen's R = (σ/2)(Φ⁻¹(p_A)−Φ⁻¹(p_B)). Since Φ⁻¹ is increasing the g-argmax IS the smoothed prediction ĝ, so ĝ cannot flip inside the L2 ball of radius σ·m/2.

theorem Proofs.smoothing_certified_radius {k : ℕ} {E : Type u_1} [NormedAddCommGroup E] {σ : ℝ} (hσ : 0 < σ) {Phiinv : ℝ → ℝ} (hmono : Monotone Phiinv) (hanti : ∀ (p : ℝ), Phiinv (1 - p) = -Phiinv p) {p : Fin k → E → ℝ} (hg : ∀ (c : Fin k), LipschitzL2 (1 / σ) fun (x : E) => Phiinv (p c x)) {x δ : E} {i : Fin k} (hrunner : ∀ (j : Fin k), j ≠ i → p j x ≤ 1 - p i x) (hδ : ‖δ‖ < σ * Phiinv (p i x)) (j : Fin k) : j ≠ i → p j (x + δ) < p i (x + δ)

Randomized-smoothing certified radius (Cohen–Rosenfeld–Kolter 2019). The form the *-smooth drivers report: with p c x = P[f(x+η)=c], an (abstract) probit Φ⁻¹ = Phiinv that is increasing (hmono) and odd about ½ (hanti : Φ⁻¹(1−p) = −Φ⁻¹(p) — the real inverse Gaussian CDF is both), per-class scores Φ⁻¹∘(p c) each (1/σ)-Lipschitz (hg), and the runner-up bound p_j(x) ≤ 1 − p_A(x) (the non-top mass; hrunner), every ‖δ‖₂ < σ·Φ⁻¹(p_A(x)) keeps class i the strict argmax of the noise-probabilities — i.e. ĝ(x+δ) = i. This is the σ·Φ⁻¹(p_A) radius, derived from the core step via p_B ≤ 1−p_A ⇒ Φ⁻¹(p_B) ≤ −Φ⁻¹(p_A), so the margin Φ⁻¹(p_A)−Φ⁻¹(p_B) ≥ 2·Φ⁻¹(p_A). Depth-independent: no per-layer norm, no product.

theorem Proofs.smoothing_certified_radius_probit {k : ℕ} {E : Type u_1} [NormedAddCommGroup E] {σ : ℝ} (hσ : 0 < σ) {Phiinv : ℝ → ℝ} (hmono : MonotoneOn Phiinv (Set.Ioo 0 1)) (hanti : ∀ q ∈ Set.Ioo 0 1, Phiinv (1 - q) = -Phiinv q) {p : Fin k → E → ℝ} (hp : ∀ (c : Fin k) (y : E), p c y ∈ Set.Ioo 0 1) (hg : ∀ (c : Fin k), LipschitzL2 (1 / σ) fun (x : E) => Phiinv (p c x)) {x δ : E} {i : Fin k} (hrunner : ∀ (j : Fin k), j ≠ i → p j x ≤ 1 - p i x) (hδ : ‖δ‖ < σ * Phiinv (p i x)) (j : Fin k) : j ≠ i → p j (x + δ) < p i (x + δ)

The radius theorem at an honest probit (Ioo variant). The TRUE quantile Φ⁻¹ is unbounded on (0,1), so no total real-valued Phiinv can satisfy the global hmono of smoothing_certified_radius while agreeing with it — the abstract theorem is fine, but it can never be instantiated at the real inverse Gaussian CDF. This variant fixes that: all class probabilities live in (0,1) (hp — Monte-Carlo/Clopper–Pearson estimates are never exactly 0 or 1), and monotonicity/oddness are only required ON Ioo 0 1, which the real Φ⁻¹ satisfies (SmoothingGaussian.lean discharges both, making the Cohen radius a theorem about the genuine Gaussian quantile with only the Neyman–Pearson Lipschitz core hg left as a hypothesis). Same proof, with the Ioo memberships threaded through.