The robustness certificate composed with the float bridge #
REDUCED CERTIFICATE MODEL — this file's concrete net is the 4×4-pooled 49-dim
MNIST family (width-8 hidden, /128–/256 rational weights), NOT the canonical
784→512→512→10 mlpVerified; chosen so every margin/norm/SOS check is exact rational
arithmetic in-kernel. Canonical surface: Proofs/MlpCanonical.lean.
The 2026-07-02 audit's gap #1, closed: the scorecard's per-image Lipschitz-
margin certificates (LipschitzCertScorecard.lean, exact-ℝ net) composed with
the FloatBridge forward budgets, certifying the FLOAT-EVALUATED capped net.
For each image below: for every L2 perturbation ‖δ‖ < ε = 1/10 and
every rounded input y within u32·(11/10) of img + δ coordinatewise
(covering input quantization), the rounded two-layer forward M.mlp2F — for
any rounding model M at binary32 accuracy or better (M.u ≤ u32) —
keeps the true class the strict argmax.
The composition is pure margin arithmetic (certified_at_eps_close): the
Tsuzuku gap at img + δ is at least m − √2·L·ε; the 2-layer float budget
B ≤ ((14899 : ℝ)/2500000) (γ-form layerBudget chain at the capped net's exact
magnitude bounds |W1s| ≤ ((475 : ℝ)/256), |W2s| ≤ ((129 : ℝ)/64), inputs ≤ 11/10)
perturbs each logit by at most B, so any margin clearing
(14143/10000)·L·ε + 2·B ≈ 2.8066 (vs the ℝ-only threshold
≈ 2.7947) keeps the float argmax:
33/34 of the ℝ-certified images survive the float widening
(dropped: [41]).
Theorem vs. measurement — read this before quoting a number. Soundness lives
in the ENGINE below (certified_at_eps_close + certifiedFloat_of_margin,
proved once) — kernel-checking the 57th image buys nothing the 56th didn't. The
33/34 above is an exact-rational MEASUREMENT; the first 8 surviving images
(test-set order — an unbiased, reproducible rule) each carry a
certifiedC<i>_float THEOREM.
Each such block re-checks all 49 coordinates by fin_cases, which is what this
file costs on every proof push.
What this does NOT close (unchanged trust boundary, Binary32Instance.lean):
the kernel↔model gap — FMA contraction, reduction reassociation, "the GPU
rounds like rndP" — and rndP's overflow/subnormal idealization.
Generated by scripts/lipschitz_cert_float.py from the committed scorecard
data; weights/images/margins are DATA here.
The rounded 2-layer MLP forward: rounded dense, bare (exact) relu,
rounded dense — the 2-layer face of mlpF.
Equations
- M.mlp2F W₀ b₀ W₁ b₁ x = M.dense W₁ b₁ (Proofs.relu d₁ (M.dense W₀ b₀ x))
Instances For
2-layer MLP forward error, uniform budgets, quantized input. If the
device input y is within ein of the real input x coordinatewise
(input quantization), every rounded logit is within the closed-form
2-layer layerBudget chain of the exact-ℝ logit. The 2-layer face of
mlp_float_close_uniform, with the fresh-input e = 0 generalized to
e = ein.
The certificate composed with a per-logit evaluation budget. If the
ℝ logit map is L-Lipschitz with margin m at x, and the margin
clears the float-widened threshold (14143/10000)·L·ε + 2·B, then ANY
evaluation z' within B of the ℝ logits at x + δ keeps class i
the strict argmax — for every ‖δ‖ < ε. Pure margin arithmetic; z'
is the deployed (rounded) forward.
Capped hidden weights in the Mat (input×output) convention.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Layer-0 budget at the capped-net magnitudes, with the input-quantization
error u32·(11/10) inherited.
The whole 2-layer budget: every rounded logit within ((14899 : ℝ)/2500000).
The composed per-image engine: margin clears the float-widened threshold ⇒ the rounded forward of any quantized perturbed input keeps the class.
Float-certified at ε = 1/10 (image #0): every binary32-accuracy rounded forward of every quantized input within the L2 ball keeps class 7 the strict argmax.
Float-certified at ε = 1/10 (image #3): every binary32-accuracy rounded forward of every quantized input within the L2 ball keeps class 0 the strict argmax.
Float-certified at ε = 1/10 (image #5): every binary32-accuracy rounded forward of every quantized input within the L2 ball keeps class 1 the strict argmax.
Float-certified at ε = 1/10 (image #10): every binary32-accuracy rounded forward of every quantized input within the L2 ball keeps class 0 the strict argmax.
Float-certified at ε = 1/10 (image #13): every binary32-accuracy rounded forward of every quantized input within the L2 ball keeps class 0 the strict argmax.
Float-certified at ε = 1/10 (image #14): every binary32-accuracy rounded forward of every quantized input within the L2 ball keeps class 1 the strict argmax.
Float-certified at ε = 1/10 (image #17): every binary32-accuracy rounded forward of every quantized input within the L2 ball keeps class 7 the strict argmax.
Float-certified at ε = 1/10 (image #25): every binary32-accuracy rounded forward of every quantized input within the L2 ball keeps class 0 the strict argmax.