Documentation

LeanMlir.Proofs.Certificates.LipschitzCert.Basic

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

The certificate behind the mnist-{linear,mlp,cnn}-pgd demos: the lower bound of the cert ≤ TRUE ≤ PGD sandwich, stated as 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/Verified/Attack.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_probit 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. It asks monotonicity and oddness of the probit only on (0,1), which is what lets the REAL Gaussian quantile instantiate it (Smoothing.Gaussian discharges its hmono/hanti at the true Φ⁻¹).

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

source
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
Instances For
    source
    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.

    source
    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.

    source
    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) — Mathlib's EuclideanSpace.real_norm_sq_eq at Fin k.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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 + δ)

    Randomized-smoothing certified radius (Cohen–Rosenfeld–Kolter 2019), at an honest probit. The form the *-smooth drivers report: with every class probability p c y in (0,1) at every point y (hp), a probit Φ⁻¹ = Phiinv that is increasing and odd about ½ on (0,1) (hmono, hanti), per-class scores Φ⁻¹∘(p c) each (1/σ)-Lipschitz (hg), and the runner-up bound p_j(x) ≤ 1 − p_A(x), every ‖δ‖₂ < σ·Φ⁻¹(p_A(x)) keeps class i the strict argmax of the noise-probabilities. The true quantile is unbounded on (0,1), so monotonicity is only asked on (0,1): a global Monotone Phiinv agreeing with it cannot exist. Smoothing.Gaussian discharges hmono/hanti at the real Φ⁻¹ and proves hg for Gaussian-smoothed [0,1] scores (smoothing_probit_lipschitz); smoothing_certified_radius_classifier is the resulting form for a measurable classifier, whose hypotheses are 0 < σ, measurability, hp and the radius bound.