ConvNeXt whole-block backward-graph faithfulness (per-example / batch-1) #
The ConvNeXt analogue of mbResidBlockBackBatchedGraph_faithful (EfficientNet) and
r34BasicBlockBackBatchedGraph_faithful / r34DownBlockBackBatchedGraph_faithful (ResNet-34):
a backward StableHLO graph that denotes the proven whole-block VJP.
This file's graphs are per-example: ConvNeXt's channel LayerNorm (chanLNTensor3) is
per-example separable, so no batch-coupled machinery (EfficientNet's bnBatchLA) is needed, and
the batched ties (ConvNeXtStepTieGB.lean, ConvNeXtWholeBackCertifiedTieB.lean) are plain
batchMaps of these per-example maps. The skip is spelled with residualBackGraph, as in
EfficientNet's blocks.
chanLNBackGraph and its faithfulness come first, then the block, residual-block and downsample
capstones over it. chanLNBackGraph_faithful is the backward peer of chanLNGraph_faithful, and
chanLNBackGraph_eq_vjp chains it through chanLNTensor3Back_eq_chanLN_vjp
(ConvNeXtBackCertifiedTie.lean), so every capstone lands on the certified VJP rather than on a
hand-composed reverse chain. The block is residual (block body)
with an identity skip, so the brick is residualBackGraph (bodyBack …) dy, closed via
residualBackGraph_faithful.
The block body is layerScale ∘ project(1×1) ∘ gelu ∘ expand(1×1) ∘ LN ∘ depthwise(7×7); everything is smooth (GELU is smooth, conv/layerScale linear, LN
smooth given ε>0), so the body VJP is the unconditional vjpComp chain
convNextBlockBodyHasVJP and the only side condition is the LayerNorm positivity
0 < εn. The LN backward is the one non-rfl op, closed by chanLNBackGraph_eq_vjp.
One channel-LN backward site, mirroring ConvNeXtRender.lnBackSite at chLN := true
op-for-op: transpose the cotangent to [h·w, c], scale it by the real [c] γ, run the rowwise
LN input gradient at γ = 1 against the saved input's transposed view, transpose back. The two
transports are the reassoc / unassoc casts chanLNGraph uses.
The saved LN input enters as a VALUE (chanLNRows — its [h·w, c] view) alongside its SSA
name, as bnBack carries its own: lnRowBack recomputes x̂/istd from the
input rather than saving them. The backward peer of ConvNeXtFullT.chanLNGraph.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Channel-LN backward-graph faithfulness — the den-level peer of chanLNGraph_faithful.
Same six-step shape as the forward: the two
transports through den_{un,re}assocS, the three permutation/scale ops and the row backward
through their rfl gates, and the graph's rowScaleF-then-lnRowBack pair collapsed onto
rowLNVecFlatBack by rowLNBack_affine_eq.
The channel-LN backward graph denotes the CERTIFIED VJP. chanLNBackGraph_faithful lands
on chanLNTensor3Back, the hand-composed reverse chain;
chanLNTensor3Back_eq_chanLN_vjp carries it the last step onto
(chanLNTensor3HasVJP …).backward. Every capstone below is built on this statement, so each
ties its graph to the certified gradient rather than to another hand-written chain. β-free on
both sides.
The channel-LN block-body backward graph — the block body's reverse chain with
chanLNBackGraph for the LayerNorm and the LN affine at Vec c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Channel-LN block-body backward-graph faithfulness. The reverse-order graph denotes
cnxBodyWithHasVJP's backward at the shipped LayerNorm, under 0 < εn. The LN is the one
non-rfl op (a whole subtree, closed by chanLNBackGraph_eq_vjp); the depthwise, 1×1 conv,
GELU and layer-scale backs are their *_faithful lemmas.
The channel-LN stage-boundary downsample backward graph. Forward is flatConvStride2(2×2) ∘ chanLNTensor3, so the VJP in reverse order is
chanLNBackGraph ∘ convStridedBack, each at its forward input: LN is the outer backward at
x, and the strided conv's input is chanLNTensor3 … x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The channel-LN downsample: backward graph ↔ proven VJP, under 0 < p.ε, at the
LayerNorm the net uses. convStridedBack is rfl-faithful; the LN goes through
chanLNBackGraph_eq_vjp.
The channel-LN ConvNeXt block as a CertLayer — the form the shipped net's stages are
built from, with cnxResidBlockChBackGraph_faithful as its faithful field. This is the one to
chain for a real ConvNeXt stage.
Equations
- One or more equations did not get rendered due to their size.