The mixed-precision conv at a perturbed input #
FloatModel.conv_close_mixed bounds one bf16-mixed convolution against exact ℝ at
an exactly-represented input. That is not enough to compose: a net feeds each layer the
previous layer's already-perturbed output, so what a fold needs is an error modulus — a map
from inherited input error to output error — plus a magnitude bound to thread forward. That pair
is what flatConvMixed_close states: the bound at an input that is both perturbed (E) and
magnitude-bounded (A). No whole-net bf16 (or f32) float bound is assembled in the repo.
What genuinely had to be proved here, none of which the e = 0 bound gives:
convFanS_le— the data-dependentΣ|kernel·window|replaced by the closed formn·w·A, so the budget is a formula in dims and norms rather than in the input.conv2d_sub_abs_le— the REAL conv isn·w-Lipschitz in its input. This is the term that carries a predecessor's error through the layer, and it has no analogue ate = 0.convMixedBudget/convMixed_close_prop— the two combined, at an input that is both perturbed (E) and magnitude-bounded (A).
Note: the budget is evaluated at A + E, not A. The float conv runs on the perturbed input, so
its own rounding scales with the perturbed magnitude; only the real conv sees A. Writing A
there would understate the bound.
n = ic·kH·kW throughout. The fan-in amplification rides uacc (fp32) while uleaf (bf16)
enters flat, so the per-layer relative factor is 1 + O(u); composed depth-first, the bound is
still vacuous in absolute terms (see convMixedGain_factor).
The window inherits the input's magnitude bound — the padded branch is 0, which needs
0 ≤ A rather than the hypothesis.
The window inherits the input's PERTURBATION. The padding branch is the same branch for
both tensors (it depends only on the indices), so it contributes |0 - 0| = 0 ≤ E.
The data-dependent fan-in sum, bounded by dims and norms. conv_close_mixed scales
everything by convFanS W x o hi wi = Σ|kernel·window|; this replaces it by n·w·A, which
is what turns that theorem into a budget a fold can carry.
conv2d is n·w-Lipschitz. THE term with no analogue at e = 0: it is how a
predecessor layer's error reaches this layer's output. The bias cancels (it is the same in
both), so the difference is one dot product against the window difference.
The mixed-precision conv budget — the layerBudget peer, and the object this whole
file exists to produce. Four terms:
uacc * (… + β)— the f32 bias add,uleaf * (1+br) * …— the bf16 store of the accumulator (the bf16-TYPED conv result, forced by the only emit shape that reaches tensor cores),br * …— the dot itself, fan-innamplified at the ACCUMULATE precision,n·w·E— the inherited error, carried through by the real conv's Lipschitz constant.
Note: The first three are evaluated at A + E, not A: the float conv runs on the PERTURBED
input, so its own rounding scales with the perturbed magnitude. Only the fourth term is
linear in E alone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Mixed-precision convolution against exact ℝ at a PERTURBED input. The composable
peer of conv_close_mixed, which is this at E = 0 and with the data-dependent convFanS
left in place.
Two steps: the float conv is conv_close_mixed at its OWN input xt (whose magnitude is
A + E), and the real conv moves from xt to xa by conv2d_sub_abs_le.
Vec-space mixed-precision conv — the bf16 peer of FloatModel.flatConvF, in the flat
space the ResNet composition actually lives in.
Equations
- M.flatConvMixed L W b v = (M.convMixed L W b (Proofs.Tensor3.unflatten v)).flatten
Instances For
The Vec-space propagating bound — convMixed_close_prop transported through
flatten/unflatten, exactly as flatConvF_close transports convF_close.
The per-layer error GAIN — the coefficient of the inherited error E in
convMixedBudget. This is the number that compounds: a d-layer stack multiplies its
input error by gain^d, so the gain, not the additive constant, is what decides whether a
composed bound says anything.
Equations
- Proofs.convMixedGain uacc uleaf n w = ↑n * w * (1 + Proofs.convBrR uacc uleaf n + uleaf * (1 + Proofs.convBrR uacc uleaf n) + uacc * ((1 + uleaf) * (1 + Proofs.convBrR uacc uleaf n)))
Instances For
The per-layer gain factors as n·w·(1+ε), with
ε = br + u_leaf(1+br) + u_acc(1+u_leaf)(1+br) (br = convBrR u_acc u_leaf n).
Relative to f32 (layerBudget, whose slope in E is n·w·(1+u)^(n+2), so ε = (1+u)^(n+2) − 1), bf16-mixed changes only the
1+ε factor, not the n·w growth rate. Composed over depth, both bounds grow as
(n·w)^d and are vacuous in absolute terms at real layer sizes.