The ResNet-34 / ResNet-50 backward chains — the ℝ maps the ResNet ties are about #
The hand-composed reverse of the committed ResNet forwards, as plain defs on the cotangent:
the two basic-block backwards (r34IdBlockBack, r34DownBlockBack), the per-example whole-net
chain r34InputGrad (the reverse of resnet34Forward_full_pc), and the batched chains
r34InputGradB / r50InputGradB (the reverses of resnet34ForwardB_full /
resnet50ForwardB_full, at a variable batch N, R50 also at a variable resolution q). Each
chain keeps its sixteen block backwards and its BatchNorm backwards as supplied maps and spells
only the endpoints — the stem's strided conv-back, the 3×3/s2 pool-back, the GAP-back and the
dense-back — so that the certified tie (ResNet34BackCertifiedTie, ResNet34BackCertifiedTieB,
ResNet50WholeBackCertifiedTieB) is a statement about a NAMED chain of the forward's shape.
⛔ maxPool3s2FlatBackB, the batched pool backward, is StableHLO.batchMapAux and not
batchMap: the pool's backward is indexed by the saved forward activation and every example
has its own, so a batchMap would hand example 0's argmax pattern to all of them. It is the one
endpoint the batch axis changed, and the reason this leaf imports StableHLO.lean.
⚠ Padding is SYMMETRIC at every stride-2 site of both nets (flatConvStride2Back), the
PyTorch-origin convention — not the XLA-SAME flatConvStride2XlaBack the TF-origin stems take.
⚠ At a variable q every dimension is written as an explicit 2 * (…) nest, never 8 * q: those
are equal Nats and NOT definitionally equal terms, and each stage demands its operand at exactly
the spelling it names.
Moved here from the float bridges that defined them beside their float twins on 2026-09-08
(planning/archive/float_second_pass.md); no number is stated about any of these chains.
The r34 identity basic-block input-gradient VJP at a smooth point — the reverse of rblkPC.
relu(F(x)+x) backward = the ReLU mask, then the residual split (cotangent to both the body and
the skip, added): residual bF ∘ reluMaskBack, with bF the reverse of F = bn₂∘conv₂ ∘ relu∘bn₁∘conv₁. The ReLU kinks read the fixed sign masks m_out/m_mid; the BN-backs bnB₁/
bnB₂ are the per-channel BatchNorm backwards, supplied. The residual-skip backward is the
forward's own Proofs.residual: the skip routes the cotangent to both branches and adds.
Equations
- Proofs.r34IdBlockBack W₁ W₂ bnB1 bnB2 m_out m_mid = Proofs.residual (Proofs.convFlatBack W₁ ∘ bnB1 ∘ Proofs.reluMaskBack m_mid ∘ Proofs.convFlatBack W₂ ∘ bnB2) ∘ Proofs.reluMaskBack m_out
Instances For
The r34 downsample basic-block input-gradient VJP at a smooth point — the reverse of
rblkPStridedPC. relu(proj(x) + body(x)) backward = the ReLU mask, then the two-branch
fan-in bProj(dy') + bBody(dy') (both branches non-trivial, summed). The strided convs reverse
via flatConvStride2Back; the BN-backs bnB₁/bnB₂/bnBp are the per-channel BatchNorm
backwards (supplied).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The whole ResNet-34 input-gradient VJP at a smooth point — the exact reverse of
resnet34Forward_full_pc: dense ∘ GAP ∘ [3,4,6,3] blocks ∘ maxpool ∘ stem reversed. The
stem/GAP/maxpool/dense endpoints are concrete (flatConvStride2Back/gapBack/maxPool3s2FlatBack/
dense (transposeᵀ) 0); the 16 block backwards a0B..e1B are supplied (each an
r34IdBlockBack or r34DownBlockBack at the tie). The [3,4,6,3] stage structure is in the
block maps' dims (down-blocks change channels×spatial; identity blocks preserve). The pool is
the 3×3/s2 stem pool's backward — the 2×2 maxPoolFlatBack this chain once used is a different
function of the same type, which is what the tie found.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched 3×3/s2 max-pool backward — maxPool3s2FlatBack per example, on that example's
OWN saved stem activation. ⛔ It is batchMapAux and not batchMap: a batchMap would hand
example 0's argmax pattern to every example (StableHLO.batchMapAux's own header records the
same trap on the emitter side). This is den (.maxPool3s2BackB …) up to the two spellings of
the scatter (ResNet34StepTieB.mpInB is the maxPool3s2BackFlat one).
Equations
- Proofs.maxPool3s2FlatBackB N c h w v = Proofs.StableHLO.batchMapAux N (fun (xv : Proofs.Vec (c * (2 * h) * (2 * w))) => Proofs.maxPool3s2FlatBack (Proofs.Tensor3.unflatten xv)) v
Instances For
The batched whole-net input-gradient backward of ResNet-34 — the exact reverse of
resnet34ForwardB_full = head ∘ [3,4,6,3] ∘ stem: dense-back → GAP-back → the sixteen basic
blocks' backwards → the 3×3/s2 pool back → the stem's relu mask, BatchNorm back and 7×7/s2
conv back. The block backwards and the stem's BatchNorm back are supplied; the conv, pool, GAP
and dense leaves are concrete and lifted over the N examples. ⭐ N is a variable: this chain
carries no numerals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched whole-net input-gradient backward of ResNet-50 — the exact reverse of
resnet50ForwardB_full = head ∘ [3,4,6,3] bottlenecks ∘ stem: dense-back → GAP-back → the
sixteen bottleneck backwards → the 3×3/s2 pool back → the stem's relu mask, BatchNorm back
and 7×7/s2 conv back. The bottleneck backwards and the stem's BatchNorm back are supplied;
the conv, pool, GAP and dense leaves are concrete and lifted over the N examples. ⭐ q is a
binder, so one chain covers resnet50in_fwd (q = 7, 224 px) and resnet50in160_fwd
(q = 5, 160 px — the net the quoted 76.66% trains). Stem and head ARE ResNet-34's
(r34StemB / r34HeadB) at R50's widths.
Equations
- One or more equations did not get rendered due to their size.