ℝ→Float32 bridge for BatchNorm: the inverse-stddev keystone #
The no-BN CIFAR bridge (CifarFloatBridge.lean) reuses the existing relative-error
model over sums/products/exact-max. BatchNorm adds the one genuinely new numerical
op: the inverse standard deviation istd = 1/√(σ²+ε). The relative-error model
|rnd x − x| ≤ u·|x| does not cover rsqrt (a GPU rsqrt, like exp, has no IEEE
spec), so — exactly as the softmax bridge models exp by a supplied fexp with an
eexp accuracy hypothesis — we model the float inverse-stddev by a supplied
fistd : ℝ → ℝ with a relative accuracy ers.
The keystone is that t ↦ 1/√t is Lipschitz on [ε, ∞) with constant 1/(2ε√ε)
(rsqrt_lipschitz, proved by the algebraic identity
1/√a − 1/√b = (b−a)/((√a+√b)·√a·√b) and the ε-floor). Composing the rsqrt
accuracy with this Lipschitz bound gives bnIstd_close: the float istd is within
ers/√ε + e_var/(2ε√ε) of the certified bnIstd, where e_var is whatever budget
the (standard, Higham) variance rounding supplies. This is the BN analog of the
exp accuracy handoff — the piece that the full per-example bnForward rounding
budget composes from (mean/var rounding + the normalize-stage products remain the
mechanical tail).
t ↦ 1/√t is Lipschitz on [ε, ∞) with constant 1/(2·ε·√ε) = 1/(2ε^{3/2}).
Proof: the algebraic identity 1/√a − 1/√b = (b−a)/((√b+√a)·√a·√b), then the
ε-floor bounds the denominator below by 2ε√ε. The keystone for pushing a
variance-rounding error through the BN inverse-stddev.
BN inverse-stddev rounding budget (the keystone). Model the GPU
inverse-stddev by a supplied fistd with relative accuracy ers
(|fistd t − 1/√t| ≤ ers·(1/√t)), evaluated at the rounded fvarε ≥ ε
(the float σ²+ε, within evar of the real σ²+ε). Then the float istd is
within ers/√ε + evar/(2ε√ε) of the certified bnIstd. The first term is
the rsqrt accuracy lifted to the ε-floor; the second is the variance
rounding pushed through rsqrt_lipschitz. The BN analog of the softmax
exp-accuracy handoff.
BN inverse-stddev budget at the OPERATING POINT (a-posteriori). Identical
to bnIstd_close, but the 1/√ Lipschitz floor is a variance lower bound
V ≤ σ²+ε (both float and real), not the ε-floor. rsqrt_lipschitz is
floor-agnostic, so the bound becomes ers/√V + evar/(2V√V) — and since the
measured σ² is O(1) (never near 0), V ≈ σ²+ε ≫ ε makes this ~(σ²/ε)^{3/2}
tighter than the ε-floor bnIstd_close (empirically ~10⁷× on the CIFAR-BN
probe, scripts/cifar_bn_margin_probe.py). The non-vacuous BN certificate.
The float BN forward (per-example, supplied mean fμ and inverse-stddev
fistdv): yᵢ = fl(γ ⊙ fl(fl(xᵢ ⊖ fμ) ⊙ fistdv) ⊕ β) — every +/−/·
rounded; γ/β are the stored (exact) parameters.
Instances For
The closed-form budget of the BN normalize chain: a sub rounding, two
muls (mulErr), and the final add rounding, threading the upstream mean
error emean and inverse-stddev error eistd.
Equations
- One or more equations did not get rendered due to their size.
Instances For
BN forward closeness, normalize chain. Given the mean within emean and
the inverse-stddev within eistd of the certified values (the latter from
bnIstd_close), plus magnitude bounds (|xᵢ−μ| ≤ D, |istd| ≤ S, |γ| ≤ G,
|β| ≤ Bbnd), the rounded BN forward output is within bnNormBudget of the
real bnForward per coordinate. The output half of the per-example BN bridge;
compose with bnIstd_close (istd) and the mean/var Higham budgets.
⭐⭐ The mean reduction's budget, parameterised by the REDUCTION'S OWN SPEC.
bnMean_close below is this at fsum := M.sum, the concrete LEFT FOLD — and a GPU does not
reduce left to right, so a number stated through that instance is about a program we do not
ship. This form takes any fsum whose forward error meets a fan-in γn, which is what every
summation order satisfies: sequential summation is the worst of them at
γ = (1+u)^{n+1} − 1, and a tree's is (1+u)^{⌈log₂n⌉+1} − 1, strictly smaller, so the
bound holds a fortiori. The resulting mean accuracy is DERIVED for the kernel actually
shipped rather than supplied by analogy (planning/archive/float_budget_numbers_log.md §3.31 route 3);
it is bnMean_close's proof with one hypothesis substituted.
⚠ Only the SUM is parameterised. The division by the exact width is M.div, one rounding,
and there is nothing to model about it.
BN mean rounding budget. The float mean fl((Σx)/n) (rounded sum, then a
rounded division by the exact n) is within
u·(1+u)^{n+1}·A + ((1+u)^{n+1}−1)·A of the real bnMean, under |xᵢ| ≤ A.
Standard: sum_close's fan-in γ plus one division rounding. ⚠ Stated at the concrete
left fold M.sum; bnMean_close_of above is the form that covers the kernels we ship.
⭐⭐ The derived mean accuracy as a RATIONAL — the form a budget file's profile takes.
bnMean_close_of at the fan-in every summation order meets, with gamma_num's
k·u/(1−k·u) relaxation and one more round-up, so what a record has to carry is a numeral
and not an expression in M.u.
⭐ At n = 12544 (ResNet-34's stem BatchNorm) and u ≤ 2⁻²⁴ it is 7.484·10⁻⁴, where every
committed normalisation number SUPPLIED 10⁻² — by analogy with the device rsqrt, which
genuinely has no IEEE specification, when a rounded reduction plainly does have one. That is
§3.3.0(b)'s rule (before writing a bound, grep the whole cone for it) at the tenth
instance: bnMean_close has been in this file since the MNIST work.
Closed-form budget of the float variance vs bnVar. esq is the per-term
centered-square error (mulErr at the centered bound D and centered error
es1 = u(D+emean)+emean); γₙ is the reduction fan-in.
Equations
- One or more equations did not get rendered due to their size.
Instances For
BN variance rounding budget. The float variance (rounded centered squares,
rounded sum, rounded /n) is within bnVarBudget of the real bnVar, given
the mean within emean and the centered bound |xᵢ−μ| ≤ D. The coupled Higham
reduction: each centered term inherits emean (via mul_close), then a
fan-in γ sum and a division rounding — the variance peer of bnMean_close.
Per-example BN forward closeness (assembled). The float BN forward at the
rounded mean fl((Σx)/n) and the GPU inverse-stddev fistd fvarε is within
bnNormBudget of the certified bnForward, with the mean error discharged by
bnMean_close, the inverse-stddev error by the bnIstd_close keystone (the
rsqrt accuracy + rsqrt_lipschitz), and the normalize chain by
bnForward_close_of. The only supplied input is fvarε's closeness to σ²+ε
(hvar) — the variance Higham reduction, the one remaining mechanical piece.