Documentation

Randomized-smoothing certificate (Cohen–Rosenfeld–Kolter 2019, planning/archive/robustness_ladder.md §3) — the depth-INDEPENDENT cert, and the answer where the Lipschitz product is hopeless. The smoothed classifier ĝ(x) = argmax_c P[f(x+η)=c], η ~ N(0,σ²I), is certified robust at L2 radius σ·Φ⁻¹(p_A) where p_A is a lower bound on the top class's noise probability. It's forward-only: no new kernel, no input-VJP — just sample n noisy copies, run the existing proof-rendered <slug>_fwd, count argmax votes, Clopper–Pearson lower-bound p_A. The base classifier is trained with matched Gaussian augmentation (every batch corrupted with N(0,σ²I) host-side before the proof-rendered SGD step — the forward/backward graph is untouched), the Cohen recipe. Architecture-agnostic + depth-independent, so it certifies a non-vacuous radius on the very nets (CIFAR, deep) where ∏‖Wᵢ‖₂ is astronomically loose. Generic over any VerifiedNet (fwd + train-step only).

n (SMOOTH_N, default 10000 — Cohen's large-n regime) is the estimation budget and the only honest tightening lever: the per-point radius is capped at σ·Φ⁻¹(α^(1/n)) (a unanimous vote still only certifies p_A ≤ α^(1/n)), so larger n lifts the ceiling and tightens the CP bound toward the true noise-probability — bigger certified radii at the same 1−α guarantee.

Randomized-smoothing certificate (Cohen 2019, depth-independent); see VerifiedNet.smoothCertify. Forward-only — works on any spec via its rendered fwd.