Backward-graph faithfulness for the ResNet-50 bottleneck block (batched) #
Each bottleneck form's backward graph (<blk>BackBatchedGraph) and the theorem that it denotes the
certified VJP (<blk>BackBatchedGraph_faithful) — the ResNet-50 peer of ResNet34BackB0, at the
batched index (bnBatchLA, batchMap, convBackBatched). Every stage is one other nets already
use, generic in {ic oc h w kH kW}, so the file is composition — no new stage, SHlo op or VJP:
| stage | what R50 uses it for | from |
|---|---|---|
cbReluB | the 1×1 reduce and the 3×3 (stride-1 blocks) | Foundation/Batched/StageLayers |
cbReluStridedB | the 3×3 of a downsample block | Foundation/Batched/StageLayers |
projB | the 1×1 expand (no activation) and the stride-1 skip | Foundation/Batched/Stages |
projStridedB | the strided projection skip | Foundation/Batched/StageLayers |
The three forms #
| form | where in R50 | R34 analogue |
|---|---|---|
r50Bottleneck… — identity | 12 blocks | r34BasicBlock… |
r50DownBlock… — strided projection | stages 2/3/4, block 0 | r34DownBlock… |
r50ProjBlock… — stride-1 projection | stage 1 block 0 only | none |
R34's stage 1 is ic = oc = 64, so its block 0 is an identity block. R50's stage 1 goes
64 → 256 at stride 1: the channels change, so it needs a projection, and the resolution does not,
so the projection is not strided. r50DownBlock cannot stand in for it — its type
Vec (N * (ic * (2*h) * (2*w))) → Vec (N * (oc * h * w)) puts the halving in the signature.
The stride is on the 3×3, not the leading 1×1 #
r50DownBody puts cbReluStridedB on the second conv: ResNet v1.5 / torchvision, what
jax/MainResnet50Imagenet.lean trains. The v1 placement (stride on the leading 1×1)
compiles, trains and descends, and is a different net (VerifiedSpec.Layer.bottleneckStage's
note). The leading 1×1 therefore runs at the input resolution (2*h)×(2*w).
Relu, and why every statement is _at #
R50 is relu throughout, so the VJPs are pointwise and hypothesis-threaded via vjpCompAt. A
bottleneck has three kinks: the two interior relus (h_s1, h_s2) and the post-residual relu
(h_out). The backward token is .selectPos, faithful by selectPos_faithful.
Contents #
r50BodyBackBatchedGraph— the stride-1 bodyprojB ∘ cbReluB ∘ cbReluB's backward graph;r50DownBodyBackBatchedGraphis its strided peer.r50BottleneckBackBatchedGraph_faithful— the identity blockrelu ∘ residual(F).r50ProjBlockBackBatchedGraph_faithful—relu ∘ residualProj(projB, F).r50DownBlockBackBatchedGraph_faithful—relu ∘ residualProj(projStridedB, F_s).
Each block is a CertLayer (r50BottleneckLayer, r50ProjBlockLayer, r50DownBlockLayer)
composed from the stage layers, and each theorem is that layer's faithful.
The identity bottleneck as a CertLayer: residual (cbReluLayer ; cbReluLayer ; projLayer),
then reluOut. An endomorphism (ic = oc, resolution unchanged), which is what lets
CertLayer.chain iterate it — a stage tail is n of these.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched R50 identity bottleneck's VJP at a smooth point — relu ∘ residual(F) with body
F = projB ∘ cbReluB ∘ cbReluB: the residual fan-in VJP, then the OUTER relu's pointwise VJP
at the pre-relu activation residual(F)(x) (r50BottleneckLayer's VJP). h_s2 is stated
at the SECOND stage's pre-relu activation, which lives at cbReluB … x — writing it at x
typechecks nowhere.
Three smoothness families, where r34BasicBlockBHasVJPAt needs two: the bottleneck's extra
interior conv brings its own relu.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The whole batched R50 identity bottleneck backward graph: selectPos (outer relu) ∘ residual
fan-in (body backward + identity skip). Same shape as r34BasicBlockBackBatchedGraph — the
outer relu is the LAST forward op, so its .selectPos is the OUTERMOST backward op, and the
masked cotangent feeds BOTH the body chain and the verbatim %dy skip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
CAPSTONE 1 — the whole batched R50 identity bottleneck: backward graph ↔ the proven VJP.
The three batched stage backward graphs chained at their forward activations, wrapped in the
residual additive fan-in (body cotangent + identity skip) and the OUTER post-residual relu,
proven equal to r50BottleneckBHasVJPAt. The 3-conv peer of
r34BasicBlockBackBatchedGraph_faithful, threaded through all three relu smoothness families.
Key fact, unchanged from R34: the outer relu's .selectPos mask is applied ONCE to the
incoming dy, and that masked cotangent is what the residual fan-in sees. It is
r50BottleneckLayer's faithful.
The stride-1 projection bottleneck as a CertLayer — R50 stage 1 block 0, the form with
no R34 analogue: residualProj (projLayer) (cbReluLayer ; cbReluLayer ; projLayer), then
reluOut. Changes channels, keeps resolution, so it is NOT an endomorphism and composes via
comp rather than chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched R50 stride-1 projection bottleneck's VJP at a smooth point —
relu ∘ residualProj(projB, F) with body F = projB ∘ cbReluB ∘ cbReluB and a stride-1
bn∘conv projection skip.
This is the form with no R34 analogue, and it exists in exactly one place in R50: stage 1
block 0, where channels go 64 → 256 but the resolution does not change. R34's stage 1 is
ic = oc = 64, so its block 0 is an identity block and this shape never arises.
Structurally it is CAPSTONE 1 with residual (identity skip) replaced by residualProj (both
paths nontrivial), and CAPSTONE 3 with every stride-2 op replaced by its stride-1 peer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The whole batched R50 stride-1 projection bottleneck backward graph: selectPos (outer relu) ∘
projected-residual fan-in (stride-1 projection-skip backward + body backward). Unlike the
identity block, both addV operands are nontrivial backward subgraphs; unlike CAPSTONE 3, the
skip is projBackBatchedGraph, not its strided sibling.
Equations
- One or more equations did not get rendered due to their size.
Instances For
CAPSTONE 2 — the whole batched R50 STRIDE-1 PROJECTION bottleneck: backward graph ↔ the
proven VJP. The R50-only block form (stage 1 block 0), with no R34 analogue to mirror. It is
r50ProjBlockLayer's faithful.
The strided projection bottleneck as a CertLayer — stages 2/3/4, block 0:
residualProj (projStridedLayer) (cbReluLayer ; cbReluStridedLayer ; projLayer), then
reluOut. Halves the resolution, which is why its input type carries 2*h/2*w. The stride
is on the 3×3 (cbReluStridedLayer at W₂), so h_s1 is stated at the input resolution and
h_s2 at the output one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched R50 strided projection bottleneck's VJP at a smooth point —
relu ∘ residualProj(projStridedB, F_s). The R50 peer of r34DownBlockBHasVJPAt, with the
bottleneck's third conv and its extra relu family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The whole batched R50 strided projection bottleneck backward graph: selectPos (outer relu) ∘
projected-residual fan-in (strided projection-skip backward + body backward).
Equations
- One or more equations did not get rendered due to their size.
Instances For
CAPSTONE 3 — the whole batched R50 STRIDED PROJECTION bottleneck: backward graph ↔ the proven
VJP. With CAPSTONES 1 and 2 this closes every block form in ResNet-50: 12 identity blocks,
3 strided projections and the one stride-1 projection. It is r50DownBlockLayer's
faithful.