The MNIST CNN descent rungs with the FloatModel binary32 gradient #
SgdDescent.Cnn proves one-step descent for both conv kernels and both conv biases of the
Chapter-3 MNIST CNN, assuming the gradient is accurate to η (an oracle). This file replaces
that oracle by a proof: cnn_conv2_float_sgd_descends, cnn_conv1_float_sgd_descends,
cnn_conv2_bias_float_sgd_descends and cnn_conv1_bias_float_sgd_descends take the FloatModel
transcription of the per-example gradient (FloatModel.cnnConv2FloatGrad and its three peers),
bound its distance from the certified gradient (cnn_conv2_grad_close and peers, budgets
FloatModel.cnnConv2GradBudget and peers), and feed that bound to the real rung. The update is
taken in ℝ; only the gradient is float-modelled.
The conv2-output cotangent chain is shared: cnn_conv2_cot_close bounds it at any (float or
exact) conv2 input, and the conv1 rungs reuse it at the float conv2 input, adding the rounded
transpose conv (convTap_back_close) and the conv1 ReLU mask (mask_scalar_close).
cnn_conv1_cot_close is that conv1-output cotangent, shared by the conv1 kernel and bias rungs.
The pool margins here stay MaxPool2MarginQ, with no twins. The proof model's pool backward
(MaxPool2IsArgmax) routes the cotangent to every cell attaining the window max, so at a tie it
is not the loss gradient, and a float rung needs windows without ties
(MaxPool2MarginQ.to_marginQUpTo_flat hands them to the real rungs). The rendered trainers'
select_and_scatter routes each window's cotangent to one cell instead; the two agree off ties.
Scalar ReLU-mask freeze — the (if z>0 then 1 else 0)·x peer of
reluMask_close. Under the sign margin ez < |z| the float and real masks
agree, so the masked value is 1-Lipschitz in x. The conv-output ReLU mask
𝟙[z₂>0] in the conv-2 grad-close sits on a scalar cell (not a Vec), so
it needs this rather than the vector reluMask_close.
The binary32 conv-2 weight gradient (FloatModel transcription of the
per-example gradient) — the conv peer of mlpInputFloatGrad. At kernel entry (o,cc,kh,kw) it is the
float dot of the (exact) padded-input window convPadWin against the float
conv-output cotangent slab cotWin c̃Conv o, where the float cotangent
c̃Conv rounds every step of the backward — conv-output ReLU mask 𝟙[z̃₂>0],
pool argmax selector (read on the FLOAT post-relu), and the head
W₃ᵀ·mask(z̃₃)·W₄ᵀ·mask(z̃₄)·W₅ᵀ·(float softmax−onehot) at the float
pre-activations. The M-free reluMask/maxPoolFlat/relu are exact in
float; M.convF/M.dense/M.softmaxCECotF carry the rounding.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conv-2 float-backward grad-close budget — the closed-form η the
rounded W₂ gradient stays within of the certified one. Bottom-up: the
forward rounding nest (Econv → E₃ → E₄ → δlogit, conv at fan-in
c·kH·kW, the dense head at c·h·w / d₃) feeds the head cotErr; the
backward then rides two cot_step layerBudgets (W₅/W₄) and the unmasked
W₃ layerBudget to econv; finally the spatial dot (fan-in (2h)·(2w))
contributes its Higham γ on the float-cotangent magnitude Ctilde plus the
per-entry cotangent drift econv. The conv peer of the MLP's
mulErr/layerBudget/cotErr nest, deeper by the pool + the dot.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conv-2-output cotangent error budget, as a function of the conv-2
input magnitude aX2 and rounding eX2 — the e₂ of cnnConv2GradBudget
(where aX2 = a, eX2 = 0) and the e₂ inside cnnConv1GradBudget (where
aX2 = A₁, eX2 = E₁). Factored so the conv-1 rung reuses the conv-2
cotangent chain at a FLOAT conv-2 input.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The real conv-2-output cotangent magnitude bound — aX2/eX2-independent
(the head cotangent and the two masked Wᵀ steps are magnitude-frozen).
Equations
- Proofs.FloatModel.cnnConv2CotMag d₃ d₄ nC w₃ w₄ w₅ = Proofs.FloatModel.layerAct d₃ w₃ 0 (Proofs.FloatModel.layerAct d₄ w₄ 0 (Proofs.FloatModel.layerAct nC w₅ 0 1))
Instances For
The conv-2-output cotangent is float-close at a float conv-2 input
— the conv-2 cotangent chain of cnn_conv2_grad_close, factored to
take the conv-2 input (X2, X2F) with |X2F − X2| ≤ eX2, |X2| ≤ aX2. The
conv-2 rungs instantiate the exact input X2 = X2F = x₁, eX2 = 0; the
conv-1 rung X2 = relu(z₁), X2F = relu(z̃₁), eX2 = E₁. The
chain: float forward from X2 (convF_close → dense_close×3) → head
(softmax_ce_cot_close) → cot_step_close×2 → unmasked W₃ dense_close →
pool-back (poolBack_close) → conv-2 ReLU mask (mask_scalar_close).
The real conv-2-output cotangent is magnitude-bounded by cnnConv2CotMag
— the aX2/eX2-independent ℓ∞ bound (the conv-2 ReLU mask and pool
selector only shrink, the head cotangent is in [−1,1], the two masked Wᵀ
steps and the unmasked W₃ ride layerAct). Used to bound the real conv-1
cotangent ∑ convTap·c₂ in the conv-1 rung.
The binary32 conv-2 weight gradient is within an explicit budget of the
certified one — the conv-layer peer of mlp_w0_grad_close. With
the conv-2 input x₁ exact, the FloatModel W₂ gradient
M.cnnConv2FloatGrad … stays within cnnConv2GradBudget of the certified
gradAt. The chain: float forward (convF_close → dense_close×3, relu
and pool error-transparent) ⟶ head (softmax_ce_cot_close) ⟶ two masked
Wᵀ cot_step_close (W₅ under z̃₄, W₄ under z̃₃) ⟶ unmasked W₃ dense_close
⟶ pool-backward freeze (poolBack_close) ⟶ conv-output ReLU mask freeze
(mask_scalar_close) ⟶ the spatial dot (dot_perturbed_close). Four
quantitative margins are carried (conv-output Econv, pool Econv POST-relu,
z̃₃ E₃, z̃₄ E₄); the bridge cnn_conv2_loss_gradAt_reluMask turns the
gradAt into the dot the float gradient rounds. Everything up to the dot is
cnn_conv2_cot_close at the exact conv-2 input.
One SGD step with the FloatModel binary32 conv-2 kernel gradient decreases
one example's cross-entropy loss; the gradient's accuracy is proven, not
assumed. The conv peer of mlp_input_float_sgd_descends: the gradient is the
FloatModel binary32 W₂ gradient M.cnnConv2FloatGrad …, and its accuracy is proven by
cnn_conv2_grad_close (η := cnnConv2GradBudget, discharged per kernel
entry via k4Idx_surj), not assumed. The two rounding-margin families are
carried as hypotheses: the per-layer ROUND margins
(hmarginConv/Pool/3/4, feeding the grad-close) and the gradient-radius
STEP margins + hsmall/h1/h2 (feeding cnn_conv2_sgd_descends's
drift-freeze and the descent geometry). The conv-2 input x₁ is exact.
Scope: one example, W₂ moving with every other parameter fixed, and the
update taken in ℝ — only the gradient is float-modelled.
The float conv-1-output cotangent: the conv-1 ReLU mask 𝟙[z̃₁>0] times the float conv-2
backward M.dot (convTap W₂ slab) (float conv-2-output cotangent slab), the conv-2 cotangent
taken at the FLOAT conv-2 input relu(z̃₁). The conv-1 kernel and bias gradients
(cnnConv1FloatGrad, cnnConv1BiasFloatGrad) are its rounded dot against the padded input
window and its rounded sum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The certified conv-1-output cotangent, in the reluMask form that
cnn_conv1_loss_gradAt_reluMask and cnn_conv1_bias_loss_gradAt_reluMask contract against
the padded input window and sum: the conv-1 ReLU mask times the conv-2 backward
∑ convTap·c₂ of the conv-2-output cotangent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The binary32 conv-1 weight gradient (FloatModel transcription of the
per-example gradient) — the conv-1 peer of cnnConv2FloatGrad, one conv-backward deeper. At kernel
entry (o,cc,kh,kw) it is the float dot of the (exact) padded-input window
convPadWin x₀ against the slab of the float conv-1-output cotangent cnnConv1CotF at the
conv-1 kernel u. All M-ops carry the rounding; reluMask/maxPoolFlat/relu/convTap
are exact.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conv-1 cotangent drift budget: the conv-2 backward (transpose conv) of the float
conv-2-output cotangent, a rounded dot over the slab c·(2h)·(2w) — its Higham γ against the
float-cotangent magnitude CP + e₂ plus the per-entry drift e₂, with the conv-2 cotangent
chain (cnnConv2CotMag / cnnConv2CotBudget) at the FLOAT conv-2 input (aX2 = A₁,
eX2 = E₁).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conv-1 float-backward grad-close budget — the conv-2 budget
(cnnConv2GradBudget-shaped) deepened by one conv layer: the conv-1 spatial dot (fan-in
(2h)·(2w)) rides the conv-1 cotangent drift eback = cnnConv1CotBudget and the float
conv-1-cotangent magnitude C1t = c·(2h)·(2w)·w₂·CP + eback.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The float conv-2 backward (transpose conv) against a perturbed
cotangent. The rounded M.dot of the exact convTap slab against the
float conv-2-output cotangent c2F, vs the certified ∑ convTap·c2R — the
convTap-flattening (sum_t3) plus dot_perturbed_close (fan-in
c·(2h)·(2w), per-entry tap bound w₂, float-cotangent magnitude C2t,
drift e₂). Generic in (c2F, c2R) so the conv-1 rung passes the conv-2
cotangent tensors abstractly.
The conv-1-output cotangent is float-close — the part cnn_conv1_grad_close and
cnn_conv1_bias_grad_close share. Under the five margins, at every conv-1 output cell the
float cotangent cnnConv1CotF is within cnnConv1CotBudget of the certified cnnConv1CotR,
and its magnitude within c·(2h)·(2w)·w₂·cnnConv2CotMag + cnnConv1CotBudget. The chain: the
conv-1 forward closes (convF_close), so the conv-2 input does (relu_close); the conv-2
cotangent chain at that float input (cnn_conv2_cot_close, with its real magnitude
cnn_conv2_cot_real_abs_le); the rounded transpose conv (convTap_back_close, with
convTap_back_abs_le); the conv-1 ReLU mask freezes (mask_scalar_close).
The binary32 conv-1 weight gradient is within an explicit budget of the
certified one — the conv-1 peer of
cnn_conv2_grad_close, one conv-backward deeper. With x₀ exact, the
FloatModel W₁ gradient M.cnnConv1FloatGrad … stays within
cnnConv1GradBudget. The conv-2 cotangent chain is reused at a FLOAT conv-2
input relu(z̃₁) (cnn_conv2_cot_close); the conv-2 backward is a rounded
dot of the (exact) convTap slab against the float conv-2 cotangent slab
(dot_perturbed_close over c·(2h)·(2w)); the conv-1 ReLU mask freezes
(mask_scalar_close); the conv-1 weight dot rounds it
(dot_perturbed_close over (2h)·(2w)). Five quantitative margins are
carried; the bridge cnn_conv1_loss_gradAt_reluMask turns the gradAt
into the dot.
One SGD step with the FloatModel binary32 conv-1 kernel gradient decreases
one example's cross-entropy loss; the gradient's accuracy is proven, not
assumed. The conv-1 peer of cnn_conv2_float_sgd_descends: the gradient is
the FloatModel binary32 W₁ gradient M.cnnConv1FloatGrad …, accuracy proven by cnn_conv1_grad_close
(η := cnnConv1GradBudget, discharged per kernel entry via k4Idx_surj),
wired into the abstract cnn_conv1_sgd_descends. Five per-layer ROUND
margins feed the grad-close; the gradient-radius STEP margins +
hsmall/h1/h2 feed the drift-freeze and descent geometry. Both conv
kernels of the Chapter-3 CNN now have a float-gradient descent statement.
Scope: one example, W₁ moving with every other parameter fixed, and the
update taken in ℝ — only the gradient is float-modelled.
The binary32 conv-2 bias gradient (FloatModel transcription of the
per-example gradient) — the bias peer of cnnConv2FloatGrad: at output channel o it is the float SUM
M.sum (cotWin c̃Conv o) of the same float conv-2-output cotangent slab
(the bias Jacobian is the channel indicator, so there is no convPadWin
left operand and no per-slot kernel index — one entry per channel).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The conv-2 bias-gradient grad-close budget — cnnConv2GradBudget with
the a· input factor stripped (the bias Jacobian carries no input window):
the spatial sum's Higham γ over (2h)·(2w) against the float-cotangent
magnitude (cnnConv2CotMag + cnnConv2CotBudget) plus the per-entry
cotangent drift cnnConv2CotBudget. The cotangent chain is the exact
conv-2-input (aX2 = a, eX2 = 0) instance of the factored
cnnConv2CotBudget / cnnConv2CotMag.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The binary32 conv-2 BIAS gradient is within an explicit budget of the
certified one — the bias peer of cnn_conv2_grad_close, built on the
factored conv-2 cotangent chain at the exact conv-2 input x₁
(cnn_conv2_cot_close with aX2 = a, eX2 = 0) and the spatial-SUM core
sum_perturbed_close. The bridge cnn_conv2_bias_loss_gradAt_reluMask
turns the gradAt into the sum the float bias gradient rounds. Four
quantitative margins (conv-output, pool POST-relu, z̃₃, z̃₄) freeze the
routing.
One SGD step with the FloatModel binary32 conv-2 bias gradient decreases one
example's cross-entropy loss; the gradient's accuracy is proven, not
assumed — the bias peer of cnn_conv2_float_sgd_descends: the gradient is
the FloatModel binary32 bias gradient M.cnnConv2BiasFloatGrad …,
and its accuracy is proven by cnn_conv2_bias_grad_close
(η := cnnConv2BiasGradBudget, discharged per output channel — the bias IS
a vector, so no flatten/unflatten plumbing), not assumed. The two
rounding-margin families are carried as hypotheses, exactly as in the
weight rungs. Scope: one example, b₂ moving, update taken in ℝ.
The binary32 conv-1 bias gradient (FloatModel transcription of the
per-example gradient) — the bias peer of cnnConv1FloatGrad: at output channel o it is
the float SUM M.sum (cotWin …) of the same float conv-1-output cotangent slab
(cnnConv1CotF), with no convPadWin left operand.
Equations
- M.cnnConv1BiasFloatGrad W₁ b₁ x₀ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ fexp label o = M.sum (Proofs.cotWin (M.cnnConv1CotF W₁ b₁ x₀ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ fexp label) o)
Instances For
The conv-1 bias-gradient grad-close budget — cnnConv1GradBudget with
the a· input factors stripped (the bias Jacobian carries no input window):
the spatial sum's Higham γ over (2h)·(2w) against the float conv-1
cotangent magnitude C1t = c(2h)(2w)·w₂·CP + eback plus the per-entry drift
eback = cnnConv1CotBudget.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The binary32 conv-1 BIAS gradient is within an explicit budget of the
certified one — the bias peer of cnn_conv1_grad_close, built on the
factored conv-2 cotangent chain at the FLOAT conv-2 input relu(z̃₁)
(cnn_conv2_cot_close), the conv-2 backward convTap_back_close, the
conv-1 ReLU-mask freeze (mask_scalar_close), and the spatial-SUM core
sum_perturbed_close. Five quantitative margins freeze the routing; the
bridge cnn_conv1_bias_loss_gradAt_reluMask turns the gradAt into the
sum.
One SGD step with the FloatModel binary32 conv-1 bias gradient decreases one
example's cross-entropy loss; the gradient's accuracy is proven, not
assumed — the bias peer of cnn_conv1_float_sgd_descends, the deepest
descent rung: the gradient is the FloatModel binary32 bias gradient
M.cnnConv1BiasFloatGrad …, accuracy proven by cnn_conv1_bias_grad_close
(η := cnnConv1BiasGradBudget, discharged per output channel — the bias IS a
vector), not assumed. With this, both conv kernels and both conv biases of
the Chapter-3 CNN have a float-gradient descent statement. Scope: one
example, b₁ moving, update taken in ℝ.