PoC: the full-16 (262-param) EfficientNet-B0 train step, proof-tied (the §1 fold, den) #
The §1 fold for the batched 262-param EfficientNet-B0
train step efficientnetTrainStepFaithfulV (EfficientNetRender.lean). 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.lean's *SgdB_eq_grad),
so every lemma here is the un-fused fold — ResNet34PoCB (conv, dense weight, BN) or EnetPoCG
(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 flatConvStride2Xla_weight_grad_has_vjp.correct. The op is the XLA-SAME
convStridedXlaWeightSgdB the render emits at the stem (EfficientNetRender.lean), 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 (dense_weight_grad_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 dense_bias_grad_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 cifar_bn_render_gamma_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 cifar_bn_render_beta_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 — ResNet34PoCB.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 depthwise_weight_grad_has_vjp3.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
strided VJP is already flat, so Σ_n of depthwiseStride2_weight_grad_has_vjp.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.