ℝ → Float32 bridge, Tier 1: standard-model rounding bounds #
Every theorem in LeanMlir/Proofs/ is over exact reals; the executed kernels
are binary32. This file is the first bite at that gap, for the toy nets only
(linear, MLP — the Tier-1 ladder): a standard-model formalization of
rounded arithmetic and forward error bounds for the same dense/relu
compositions the train-step proofs certify.
The model is hypothesis-style, like the suite's 0 < ε / off-the-kink
hypotheses: a FloatModel is any rounding operator rnd with relative error
u (|rnd x − x| ≤ u·|x|). No project axioms — IEEE-754 binary32
round-to-nearest satisfies the interface with u = 2⁻²⁴ in the normal
range (Higham, Accuracy and Stability, §2.2; the standard model without
underflow — the subnormal absolute-error term is future work, as is the
gradient half). exactModel (rnd = id, u = 0) shows the interface is
inhabited and collapses every bound to 0.
Design notes, in suite style:
- Order-robustness.
FloatModel.dotfixes one association (left fold), but the bound((1+u)^(n+1) − 1)·Σ|xᵢyᵢ|is the classical one valid for every summation order — so the statement survives a backend that reassociates (IREE tiles reductions), at the cost of not benefiting from pairwise summation's tighterlog ncompounding. - ReLU is exact in floating point — comparison/selection rounds nothing,
which is why
mlpFinterleaves barereluwith norndand the bridge only needsrelu's 1-Lipschitz error propagation (relu_close). The op that forced the kink hypotheses on theℝside is the free op here. - Error shapes are
denseErr, one def reused at every layer: the rounded layer at a perturbed input vs the real layer at the real input. The MLP capstone (mlp_float_close) threads it three times; itse₀/e₁hypotheses are uniformizations of the per-coordinate layer bounds, dischargeable at any concrete instance by finite max.
The unit roundoff of IEEE-754 binary32 (round-to-nearest-even).
Equations
- Proofs.u32 = (2 ^ 24)⁻¹
Instances For
The normal-range unit roundoff of fp8 E4M3 (1-4-3, 3 mantissa bits):
2⁻⁴ = 1/16 (6.25%) — the leaf precision of the §3c E4M3 MNIST demo
(scripts/mnist_e4m3_demo.py). Outside the normal range (subnormals,
near the 448 max) the relative model degrades; see §2/§5 of the plan.
Equations
- Proofs.u_e4m3 = (2 ^ 4)⁻¹
Instances For
Rounded addition: fl(x + y).
Instances For
Rounded multiplication: fl(x · y).
Instances For
Rounded dot product, left-fold association (((x₀y₀ + x₁y₁) + …)).
The bound below is association-independent, so the choice is immaterial.
Equations
Instances For
Rounded dense layer — the float peer of Proofs.dense
(fl(Σᵢ xᵢ·Wᵢⱼ) ⊕ bⱼ, every +/· rounded).
Instances For
Rounded MLP forward — the float peer of the Tier-1
dense W₂ b₂ ∘ relu ∘ dense W₁ b₁ ∘ relu ∘ dense W₀ b₀ composition
(MlpTrainStep.lean). relu appears bare: max-with-0 is exact in
floating point.
Equations
- M.mlpF W₀ b₀ W₁ b₁ W₂ b₂ x = M.dense W₂ b₂ (Proofs.relu d₂ (M.dense W₁ b₁ (Proofs.relu d₁ (M.dense W₀ b₀ x))))
Instances For
Rounded dot product forward error —
|fl(x·y) − x·y| ≤ ((1+u)^(n+1) − 1)·Σᵢ|xᵢyᵢ|.
The classical bound (Higham §3.1), in the exact compounded form (no
n·u < 1 side condition); valid for every association of the sum, not
just the left fold dot fixes. The exponent is n+1 rather than the
optimal n because dot rounds the seed addition with 0 too.
Mixed-precision dot product. The matmul inputs are first rounded by a
leaf model L (low precision, u_leaf — e.g. bf16 2⁻⁸ or fp8-E4M3
2⁻⁴); the accumulation M.dot then rounds every +/· at the
accumulate precision M.u (u_acc, typically fp32 2⁻²⁴). This is the
deployed bf16-mixed kernel shape: bf16 leaf compute, fp32 accumulate.
Instances For
Mixed-precision dot forward error, decomposed. The leaf precision
contributes only a flat per-leaf term (2·u_leaf + u_leaf²)·Σ|xᵢyᵢ|
(NOT fan-in amplified); the fan-in amplification rides entirely on the
accumulate precision as the Higham γ-factor ((1+u_acc)^(n+1) − 1). That
separation is exactly why bf16-mixed is non-vacuous where pure bf16 is not:
the 1/u fan-in wall sits at u_acc = 2⁻²⁴, not at the leaf precision.
dot_close_mixed folded to a single Σ|xᵢyᵢ| factor — the directly
instantiable form. Bounds the leaf-rounded magnitudes by (1+u_leaf)²,
so the whole error is [γ_acc·(1+u_leaf)² + (2u_leaf + u_leaf²)]·Σ|xᵢyᵢ|.
At bf16 leaf / fp32 accumulate (u_leaf = 2⁻⁸, u_acc = 2⁻²⁴, fan-in a
few hundred) the bracket is ≈ the flat 2·2⁻⁸ ≈ 0.8% leaf term plus a
negligible accumulate γ — the shipped-artifact budget.
Mixed-precision dense layer — leaf precision L on the matmul (the
dotMixed), accumulate precision M on the bias add. The deployed
bf16-mixed dense layer (fp32 master/accumulate, bf16 leaf compute).
Equations
- M.denseMixed L W b x j = M.add (M.dotMixed L x fun (i : Fin m) => W i j) (b j)
Instances For
Mixed-precision dense forward error. The leaf precision enters only
through the flat dotMixed term; the accumulate precision rides the bias
add and the fan-in γ. The bf16-mixed / fp8 dense layer falls out by setting
L.u.
The per-coordinate error budget of one rounded dense layer evaluated at an
input within e of the real activation xa: the layer's own rounding
(compounded (1+u)^(m+2) − 1, on magnitudes inflated by e) plus the
Lipschitz pass-through (Σᵢ|Wᵢⱼ|)·e of the inherited error. e = 0
specializes to the fresh-input bound.
Equations
Instances For
Rounded dense layer forward error, with inherited input error.
If xt is within e of the real activation xa coordinatewise, then
|M.dense W b xt j − dense W b xa j| ≤ denseErr W b xa e j.
dense_close at a fresh (unperturbed) input — the e = 0 face.
ReLU propagates error without amplification. No rounding term: max
with 0 is exact in floating point, so the float net applies relu bare
and the bridge only needs 1-Lipschitz-ness.
Linear-net forward extraction (Chapter 1). The rounded mnistLinear
is within the explicit denseErr budget of the real one, per logit. With
u = 2⁻²⁴ this is the binary32 forward-error bound for the certified
linear classifier.
MLP forward extraction (Chapter 2). The rounded 3-layer MLP is within
the layer-2 denseErr budget (at inherited error e₁) of the real MLP —
the same dense/relu composition whose train step is certified in
MlpTrainStep.lean. The hypotheses h₀/h₁ uniformize the per-coordinate
layer-0/1 budgets into e₀/e₁; at any concrete net they are discharged
by finite max over the d₁ (resp. d₂) coordinates.
Worst-case output magnitude of one real layer under uniform magnitude
bounds: |denseⱼ| ≤ m·w·A + β (and relu only shrinks).
Equations
- Proofs.FloatModel.layerAct m w β A = ↑m * w * A + β
Instances For
The uniform-magnitude form of denseErr: every |Wᵢⱼ| ≤ w, |bⱼ| ≤ β,
real activation magnitude ≤ A, inherited error ≤ E.
Equations
Instances For
denseErr under uniform magnitude bounds is at most the closed-form
layerBudget.
MLP forward extraction, uniform-magnitude budgets. mlp_float_close
with the e₀/e₁ uniformization discharged once and for all from
coordinatewise magnitude bounds |Wᵢ| ≤ wᵢ, |bᵢ| ≤ βᵢ, |x| ≤ a.
The budget is a closed form in the dims and magnitudes — evaluable by
norm_num at a concrete net.
Numeric capstone at the committed MNIST-MLP dims and TRAINED
magnitudes (the MainMnistMlpVerified.lean net: 784→512→512→10;
|W| ≤ 3/5 covers the measured max|W| = 0.52 of a real 12-epoch
97.8% run — He init already exceeds the prettier 1/32 in its tails).
For any rounding model at binary32 accuracy (u ≤ 2⁻²⁴), every rounded
logit is within 5100 of the exact-real logit — the worst-case logit
magnitude at these bounds is ≈4.5·10⁷, so ≈10⁻⁴ relative, the same
relative scale as at small weights. All three layer budgets discharge by
norm_num through the γ-form; no big-power evaluation.
Measured on the live run (scripts/margin_probe.py): actual logit
drift ≤ 1.6·10⁻⁵ — the ≈3·10⁸ gap between the worst-case bound and
reality is the worst-case-composition blow-up (307·e Lipschitz
amplification per layer at these magnitudes), the quantitative case for
a-posteriori certificates past toy depth.
Rounded subtraction: fl(x − y).
Instances For
Budget of one rounded product of two inherited-error operands:
|fl(xt·yt) − x·y| with |xt−x| ≤ ea, |yt−y| ≤ ec, |x| ≤ A, |y| ≤ C.
Equations
Instances For
ReLU backward mask — if z > 0 then v else 0. Compare + select: exact
in floating point, so the float chain applies it bare (the rendered
trainer's relu-back compare reads the rendered pre-activation, exactly
the zt here).
Instances For
The float-side kink condition. If the pre-activation error ez
cannot flip any sign — ez < |zᵢ|, a quantitative margin, the float
analogue of the suite's x k ≠ 0 off-the-kink hypotheses — then the
float and real masks agree and the mask is 1-Lipschitz in the value.
Cotangent through one layer — mask(z, Wᵀ·c), float vs real. The
transposed matvec is dense with zero bias, so the dot machinery is
reused wholesale; under the quantitative margin the mask passes the
layerBudget through unchanged.
Rounded output-layer weight update (W₂). The float update
fl(W₂ᵢⱼ − fl(lr·fl(ã₂ᵢ·gtⱼ))) — outer-product gradient from the stored
float forward activation, as the rendered trainer computes it — is
within an explicit budget of the real step W₂ᵢⱼ − lr·(a₂ᵢ·gⱼ). The real
target is Mat.outer a₂ g i j = emitWeightGrad's entry, the quantity
mlp_render_W2_certified proves equal to the pdiv-Jacobian contraction —
so this chains the float step to the certified gradient. Takes the output
cotangent gt ≈ g as a hypothesis (the softmax−onehot head needs an exp
accuracy axiom — future rung).
Rounded output-layer bias update (b₂) — the bias gradient is the
cotangent (emitBiasGrad), so this is sgd_step_close directly.
Rounded hidden-layer weight update (W₁), through the backward chain.
The float cotangent ct₁ = mask(pt₁, W₂ᵀ·gt) — computed from the rendered
pre-activation and the rounded transposed matvec, exactly the structure
of the rendered backward — is within layerBudget of the real
c₁ = mask(p₁, W₂ᵀ·g) (the mlpCotOut1 closed form), given the
quantitative margin E₁ < |p₁ᵢ| at every layer-1 pre-activation: the
forward rounding error must not flip a ReLU. Then the update is within
sgdErr of the real W₁ᵢⱼ − lr·(a₁ᵢ·c₁ⱼ), the quantity
mlp_render_W1_certified certifies. W₀/b₁/b₀ are the same
instantiation one mask deeper.
Rounded hidden bias update (b₁) — the gradient is the layer-1
cotangent itself (emitBiasGrad), so this is the cotangent chain
followed by sgd_step_close.
Rounded input-layer weight update (W₀) — the cotangent crosses BOTH
masks, so both quantitative margins are required; the activation operand
is the raw input x, identical in both nets (zero inherited error). The
real target W₀ᵢⱼ − lr·(xᵢ·c₀ⱼ) is the mlp_render_W0_certified
quantity.
Rounded input bias update (b₀) — the layer-0 cotangent directly.
Numeric gradient capstone at the committed dims and TRAINED
magnitudes (784→512→512→10, |W| ≤ 3/5 covering the measured
max|W| = 0.52): binary32 accuracy (u ≤ 2⁻²⁴), lr = 1/10,
|b|, |x| ≤ 1, |g| ≤ 1 (a softmax−onehot cotangent is always in
[−1,1]), cotangent taken exact — then every rounded W₂ SGD entry is
within 5/4 of the certified real step.
The budget decomposes honestly: ~1.2 of it is lr·E₁·|g| — the
forward budget riding through the gradient at learning-rate scale —
while fresh backward rounding contributes only ~2·10⁻³. The gradient
step is as accurate as the forward pass, no worse. Measured on the
live run (scripts/margin_probe.py): actual W₂ step deviation
≤ 7.5·10⁻⁹ — the worst-case-vs-measured gap is the a-posteriori case
in numbers.
Rounded division: fl(x / y).
Instances For
SGD step whose gradient is a rounded dot product. When the gradient is
a correlation g = Σ pᵢqᵢ computed in float as M.dot p q — the shape of
a conv weight gradient (Σ_{hi,wi} convPad · cot) and of any dense weight
gradient — the rounded update fl(θ − fl(lr·fl(p·q))) is within sgdErr of
the real step θ − lr·g, with the dot's Higham γ as the gradient-error
slot eg. This is dot_close feeding sgd_step_close.
SGD step whose gradient is a rounded sum. When the gradient is a plain
reduction g = Σ xᵢ computed in float as M.sum x — the shape of a conv
bias gradient (Σ_{hi,wi} cot) — the rounded update is within sgdErr of
the real step, with the sum's Higham γ as the eg slot.
The float softmax: rounded exp, rounded sum, rounded division — the
structure of the rendered loss head. fexp is hypothesis-supplied
(GPU exp has no IEEE spec; its accuracy constant is exactly what the
repo's vjp_oracle harness validates empirically).
Instances For
The float softmax−onehot cotangent (one final rounded subtract; the onehot operand is exact).
Equations
- M.softmaxCECotF fexp z label k = M.sub (M.softmaxF fexp z k) (Proofs.oneHot n label k)
Instances For
Softmax perturbation, elementary ratio form: a coordinatewise logit
error δ moves every softmax output by at most e^(2δ) − 1. Proved by
sandwiching softmax(z̃) ∈ [e^(−2δ), e^(2δ)]·softmax(z) with bare exp
monotonicity — no mean-value theorem.
Relative budget of the pre-rounding float softmax against the real softmax at the same logits.
Equations
- Proofs.FloatModel.smKappa u eexp n = (eexp + Proofs.FloatModel.smRho u eexp n) / (1 - Proofs.FloatModel.smRho u eexp n)
Instances For
Absolute budget of the float softmax against the real softmax at the
REAL logits: head rounding + the e^(2δ) − 1 logit-perturbation term.
Equations
- Proofs.FloatModel.smErr u eexp δ n = u * (1 + Proofs.FloatModel.smKappa u eexp n) + Proofs.FloatModel.smKappa u eexp n + (Real.exp (2 * δ) - 1)
Instances For
Budget of the full rounded softmax−onehot cotangent against the certified real gradient.
Equations
- Proofs.FloatModel.cotErr u eexp δ n = u * (1 + Proofs.FloatModel.smErr u eexp δ n) + Proofs.FloatModel.smErr u eexp δ n
Instances For
cotErr is nonnegative (it bounds an absolute value) — under eexp ≥ 0,
δ ≥ 0, and the denominator condition smRho < 1. The cot_step_close
precondition for any backward grad-close that runs the softmax−onehot head
(e.g. the per-layer η-composition rungs).
Float softmax vs real softmax at the same logits (part A): the
rounded exp/sum/div head is within u·(1+κ) + κ absolutely, where
κ = (eexp + ρ)/(1 − ρ) compounds the exp accuracy and the sum
rounding. The sandwich is the same ratio argument as
softmax_perturb — division-perturbation never appears.
The rounded softmax−onehot cotangent is within cotErr of the
certified real gradient softmax(z) − onehot — the pdiv-certified
∂(crossEntropy)/∂logits (softmaxCE_grad). This discharges the
g̃ ≈ g hypothesis of the mlp_*_step_float_close capstones:
eg := cotErr u eexp δ n, where δ bounds the float-vs-real logits
(worst case: the forward layerBudget; in practice: an a-posteriori
measured value, since e^(2δ) − 1 is only sharp for small δ).
smErr is nonnegative under eexp ≥ 0, δ ≥ 0, and smRho < 1 — the absolute
softmax-vs-softmax budget bounds an absolute value, so it is itself ≥ 0. (Extracted
from softmax_ce_cot_close's internal hsm0; needed as the 0 ≤ eweight precondition
of any downstream dot at perturbed softmax weights, e.g. attention's output matmul.)
Float softmax at float logits vs real softmax at real logits — within smErr.
The rounding half (softmaxF_close, float-vs-real at the same logits) plus the
logit-perturbation half (softmax_perturb, real-vs-real under a coordinatewise
logit error δ), assembled by the triangle inequality. This is the per-row engine
for attention's softmax (each row's logits are the float scores, off the real scores
by δ); extracted from softmax_ce_cot_close's internal hsm (here without the
onehot subtraction, so it applies to any softmax position, not just the loss head).
Numeric head budget at the committed MNIST output (n = 10): for
any model at binary32 accuracy, exp accurate to eexp ≤ 10⁻⁶
(GPU exp is ~1–2 ULP; the constant is what vjp_oracle validates),
and float logits within δ = 1/100 of real, the rounded
softmax−onehot cotangent is within 21/1000 of the certified
gradient — almost all of it the e^(2δ) − 1 ≈ 2δ logit-perturbation
term; the head's own rounding contributes < 4·10⁻⁶.
δ = 1/100 is an a-posteriori-style hypothesis: the worst-case
forward logit budget (≈5100 at trained magnitudes) makes e^(2δ) − 1
vacuous, so a useful head budget needs the measured logit error —
exactly the hand-off point from worst-case to a-posteriori analysis.
Empirically validated (scripts/margin_probe.py): measured drift on a
real 12-epoch run is ≤ 1.6·10⁻⁵, 600× inside the 1/100 hypothesis.
Argmax preservation under a bounded logit perturbation (planning §3c).
If every coordinate of the perturbed logits z' is within B of the
reference logits z, and z's strict top-1 margin at k exceeds 2B
(z k − z i > 2B for every other class i), then k is still the strict
argmax of z'. The depth-1 honest fp8 claim: a B-accurate matmul cannot
flip the prediction on a >2B-margin input. B is a hypothesis, so the
statement holds both for the proven worst-case bound
(dense_close_mixed) and for any measured a-posteriori drift — the demo's
empirical B = max|Δlogit| plugs into the same theorem. Conditional like
the suite's quantitative ReLU margins.
Uniform (magnitude-bounded) per-logit budget of the mixed-precision dense
layer — dense_close_mixed specialized by ∑ᵢ|xᵢWᵢⱼ| ≤ m·w·a, |bⱼ| ≤ β,
so it is one constant B over all outputs j (the input
argmax_preserved needs). The accumulate u_acc rides the bias add and the
fan-in γ-factor (1+u_acc)^(m+1); the leaf u_leaf enters only via the flat
(2·u_leaf + u_leaf²) term — the two-roundoff separation of §1c.
Equations
Instances For
Mixed-precision dense forward error, uniform-magnitude budget. Under
|Wᵢⱼ| ≤ w, |bⱼ| ≤ β, |xᵢ| ≤ a, every E4M3-mixed logit is within the
closed-form denseMixedBudget of the exact-ℝ logit — evaluable by norm_num
at a concrete net.
Monotone upper bound for denseMixedBudget, keeping the (1+uacc)^(m+1)
power abstract: replace the accumulate by U ≥ uacc, the fan-in γ-factor by
g ≥ (1+uacc)^(m+1)−1, and the two leaf pieces by P ≥ (1+uleaf)²,
Q ≥ 2·uleaf+uleaf². The result has no power left, so a concrete instance
(e.g. m = 784) evaluates by norm_num without unfolding the 785-fold
npow — the layerBudget_le_of analogue for the two-roundoff budget.
The worst-case E4M3 per-logit budget at the MNIST-linear dims (784→n;
E4M3 leaf u_leaf ≤ 2⁻⁴, fp32 accumulate u_acc ≤ 2⁻²⁴; pixels |x| ≤ 1,
trained |W| ≤ 3/5, |b| ≤ 1): every E4M3-mixed logit is within 61 of
the exact-ℝ logit. The leaf term (2·2⁻⁴ ≈ 12.5%)·∑|xW| dominates (the fp32
fan-in γ at 784 is ≈5·10⁻⁵, negligible) — this is the worst-case, all-errors-
aligned figure. The demo (scripts/mnist_e4m3_demo.py) measures the actual
drift at max|Δlogit| = 0.38 (errors cancel), the a-posteriori B; both
feed argmax_preserved.
Verified E4M3 MNIST-linear argmax preservation (planning §3c capstone).
For the certified linear classifier at E4M3 leaf precision / fp32 accumulate,
pixels |x| ≤ 1, trained |W| ≤ 3/5, |b| ≤ 1: whenever the exact-ℝ logit
margin at the top class k exceeds 2·61 = 122, the E4M3-mixed forward keeps
k as the strict argmax — provably the same prediction. Depth-1 makes
the single-matmul bound the end-to-end bound, so this is the one realistic
fp8 case with an honest accuracy guarantee (no vacuous depth compounding).
The 122 is the worst-case threshold; with the demo's measured B = 0.38
the same argmax_preserved covers the >0.76-margin inputs — empirically
92.89% of the MNIST test set (scripts/mnist_e4m3_demo.py). fp32 ≈ exact-ℝ
(within u_acc), so the demo's fp32 margins are the relevant quantity.
The exact-arithmetic model: rnd = id, u = 0. Inhabits the interface
(the standard model isn't vacuous) and collapses every budget to 0.
Equations
- Proofs.FloatModel.exactModel = { rnd := id, u := 0, u_nonneg := Proofs.FloatModel.exactModel._proof_1, err := Proofs.FloatModel.exactModel._proof_2 }
Instances For
dotMixed with an exact leaf (u_leaf = 0) is the plain rounded dot.
The fp32 specialization: no input rounding ⇒ dot_close_mixed collapses to
dot_close (the leaf term 2·0 + 0² = 0 vanishes, the leaf-rounded
magnitudes become the real ones). Confirms the two-roundoff budget is a
genuine generalization of the single-u budget, not a reparametrization.