The full-16 (262-param) EfficientNet-B0 train step, proof-tied (the fold, den) #
The fold for the batched 262-param EfficientNet-B0
train step efficientnetTrainStepText (EfficientNetRender.Basic). Every emitted param-SGD op
denotes the certified loss-descent step — θ − lr·(certified Jacobian · cotangent).
The batched wrinkle vs mnv2. EfficientNet trains at the batched index N·(c·h·w) with the
fused-batch param-SGD ops (convWeightSgdB/denseWeightSgdB/bn{Gamma,Beta}SgdB/…), whose den
carries a batch sum Σ_n over the per-example gradients (the shared-weight batched gradient).
So unlike mnv2 (per-example, one ∑_j pdiv·cot), each fold here is "the per-example bridge applied
inside Σ_n" — the batch-sum bridge. For the linear families (conv/dense weight, bias) this is a
Finset.sum_congr of the per-example .correct; for BN γ/β the den already folds N into the
per-channel reduction count m = N·(h·w), so it is the cert's exact LHS (delegation).
Each fused op is θ − lr· its un-fused gradient node by rfl (StableHLO.Basic's *SgdB_eq_grad),
so every lemma here is the un-fused fold — GradNodeB's (conv, dense weight, BN, the XLA-SAME
stem, depthwise, the rectangular dense bias) — under that wrapper.
Batched 1×1-conv weight op denotes the certified Σ_n batched weight gradient. Each emitted
convWeightSgdB (expand/project/head) denotes flatten W − lr·Σ_n (∂conv2d/∂W · cotₙ) at the
per-example slice n, via Σ_n of conv_weight_grad_bridge. Generic in dims + cotangent.
Batched strided-stem 3×3 conv weight op denotes the certified Σ_n batched weight gradient.
Σ_n of flatConvStride2XlaWeightGradHasVJP.correct. The op is the XLA-SAME
convStridedXlaWeightSgdB the render emits at the stem (EfficientNetRender.Basic), whose
weight-grad correlation pad is shifted one position; its den is the odd-phase weight VJP,
so the certified gradient here is the gradient of the net that ships.
Batched dense weight op denotes the certified Σ_n batched weight gradient. Σ_n of the
dense outer-product .correct (denseWeightGrad_correct). Covers the SE squeeze/excite denses
(W₁ : c→r, W₂ : r→c) and the head classifier. Generic in b (the grad is b-independent).
Batched dense bias op denotes the certified Σ_n batched bias gradient (Σ_{n} cotₙ per
output) — Σ_n of denseBiasGrad_correct. Covers the SE b₁/b₂ and the head bias.
Batched BN γ op denotes the certified per-channel γ gradient over the merged batch+spatial
axis m = N·(h·w). True batch-norm's γ grad is per-channel BN's γ grad at m = N·h·w
(γ enters affinely — no batch coupling in the param grad), so this is a direct delegation to
the generic bnPerChannel_gamma_sgd_certified at m = N·(h·w) (the den's exact reduction count,
via the network→oc-major reindex bnchwFwd). Generic in the free β.
Batched BN β op denotes the certified per-channel β gradient Σ_{batch,spatial} cot at
m = N·(h·w). Used for every BN β AND (as the channel-sum) every conv/depthwise bias. Direct
delegation to bnPerChannel_beta_sgd_certified. The pdiv form carries a free v/γ (β's grad
is the channel-sum, independent of them).
One batched BN layer's fused γ and β SGD nodes, tied — GradNodeB.BnPairTiedB under
θ − lr·: the emitted bnGammaSgdB / bnBetaSgdB denote the certified per-channel γ and β
steps at the layer's pre-BN activation v and output cotangent cot.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Batched stride-1 depthwise weight op denotes the certified Σ_n batched weight gradient.
Σ_n of the flattened depthwiseWeightGradHasVJP3.correct (the per-slice grad bridge from
mnv2_render_depthwiseW_flat_certified). Generic in the kernel size (3×3 and 5×5).
Batched strided depthwise weight op denotes the certified Σ_n batched weight gradient. The
op is the XLA-SAME depthwiseStridedXlaWeightSgdB the render emits at the four strided
MBConvs (b2 / b4 / b6 / b12, EfficientNetRender.Basic) — the weight-grad correlation pad
shifted one position, as the stem's — so, as for the stem, the certified gradient is the
gradient of the net that ships. The strided VJP is already flat, so Σ_n of
depthwiseStride2XlaWeightGradHasVJP.correct.
A stride-1 conv weight SGD node, tied (convWB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-1 depthwise weight SGD node, tied (depthwiseWB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A dense bias SGD node, tied — free in W and x, which b's gradient ignores.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Each clause holds, every argument implicit (read off the goal by a step tie's constructor).
At a square witness, as every use is (the gradient ignores W and x).