r34InputGradB IS the certified whole-net ResNet-34 gradient AT BATCH BATCH-NORM #
The input-gradient tie for the net the shipped trainers run: resnet34ForwardBFull, the
[3,4,6,3] ladder at bnBatchLA, at a variable batch N. The leaf ties it rests on are
ConvBackCertifiedTie's.
Nothing here is new mathematics. Two endpoint stage ties (stem and head) and one pool tie, then
the sixteen basic blocks stay opaque — they enter as HasVJPDiffAt witnesses, and the reverse
chain's block slots are pinned to their .backward — so the composition is checked between
variables. The chain is peeled by rw with a lemma proved over variable stages, so the module
checks with no budget raised.
The four pieces #
r34HeadBBack_eq_vjp_backwardandConvBackCertifiedTie's stage tiecbReluStridedBBack_eq_vjp_backward— the concrete endpoints (head and stem); the pool needs no lemma. The pool endpoint isrfl:batchMapHasVJPAtandmaxPool3s2FlatHasVJPAtVecare built field by field rather than transported with▸, sobatchMapAuxof the leaf and the lift's.backwardare the same term.r34BFullHasVJPAt— the generic eighteen-stage apexhead ∘ b16 ∘ … ∘ b1 ∘ stem, seventeen nestedvjpCompDiffAts and nothing else, overopaqueA0 … A16, one prefixdefper running activation — andr34BFullHasVJPAt_backward, its backward peeled into the eighteen stage backwards,rflat variable stages.r34InputGradB_eq_r34B_full_vjpandr34InputGradB_correct— the tie, and its reading as∑ pdiv … * dy: the chain IS the Jacobian-transpose of the eighteen-stage composition.resnet34ForwardBFull_eq_slots— the shape check: those eighteen stages AREresnet34ForwardBFull, the forwardresnet34FwdGraphBFull_faithfulsays the typed graph denotes. Without it the tie would be a statement about variables.
Scope #
A smooth-point statement: the tie assumes the stem relu clause (h_stem : R34StemSmoothAt …),
the stem pool's per-example condition (h_pool : StemPoolSmoothAt …: each window's maximum at
one position, or the window all zero) and 0 < εs, and takes each of
the sixteen blocks as an opaque HasVJPDiffAt witness at its running activation (a basic block's
two relu clauses are the caller's, inside that witness). One device: the data-parallel step,
collectives included, is ResNet34SyncStepTieB's. It is about the INPUT gradient; the parameter
gradients are ResNet34StepTieB's tie.
This statement takes no precision flag. The ImageNet run the book reports trains from
resnet34in_momdp64bf16, whose conv weight gradients are the bf16 kinds
(Foundation.Bf16GradNodes); that run's step is ResNet34StepTieB's and, data-parallel,
ResNet34SyncStepTieB's, both stated on the renderers' bf16 switch at the identity rounding
(Bf16Erasure).
The HEAD tie. batchMap (gapBack) ∘ batchMap (dense Wᵀ 0) IS r34HeadB's certified
backward. The head takes no hypothesis at all: GAP and dense are smooth and each is
batchMap of a per-example op, so r34HeadBHasVJP is GLOBAL — the one place in this net
where the certified backward comes with nothing attached. gapBack needs no rewrite; it is
definitionally the global-average-pool VJP's backward.
The stem's backward is the pool's scatter, then the conv-BN-relu stage's
(stemReluPoolLayer_vjp_backward). The tie rewrites with it rather than leaving this step to
its closing rfl, which reaches maxRecDepth at the net's numerals.
Whole-network batched ResNet-34 VJP, every stage opaque. head ∘ b16 ∘ … ∘ b1 ∘ stem,
seventeen vjpCompDiffAts and nothing else. ResNet-34's [3,4,6,3] ladder needs no
list of blocks and no separate downsample slot: a downsample block is just a block of a
different type, and the stem's pool lives INSIDE stem. Dimension-generic and parametric in
every component, so the tie below is checked between variables.
Pointwise (HasVJPAt), as every ResNet-34 statement is: relu is kinked, and this net has
two relu sites per block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The apex's backward, peeled — the head's backward, then each block's, then the stem's.
rfl over VARIABLE stages, where every witness sits at the same opaqueA point on both
sides; the tie below instantiates it by rw, so the kernel never re-derives the chain.
r34InputGradB IS the certified whole-net batch-BN ResNet-34 gradient. The committed
backward chain, with its stem BatchNorm and relu-mask slots filled by the certified per-op
backwards, its saved pool activation the stem's own, and its sixteen basic blocks left OPAQUE,
equals the backward of r34BFullHasVJPAt at those eighteen stages. unfold, the two
endpoint rws, the apex and stem peels, then rfl between identical block backwards — the
blocks are variables on both sides, so the kernel never looks inside one.
The batched chain IS the pdiv-contracted Jacobian of the eighteen-stage net — at every
batch size, loss cotangent and input pixel, at any input x where the stem relu is off its
kink (h_stem) and no stem-pool window ties (h_pool), for any block maps b1 … b16 carrying
HasVJPDiffAt witnesses at their running activations (hb1 … hb16), with 0 < εs. The tie
above read through the apex's own .correct. resnet34ForwardBFull_eq_slots below identifies
those eighteen stages with the committed forward.
THE SHAPE CHECK — the eighteen slots the tie is about ARE the committed forward.
resnet34ForwardBFull, regrouped into exactly the eighteen arguments r34BFullHasVJPAt
takes: the stem (7×7/s2 conv-BN-relu and He et al.'s 3×3/s2 pool), the [3,4,6,3] ladder as
sixteen basic blocks, and the GAP+dense head.
The tie keeps its blocks OPAQUE — they enter as the VJP witnesses, so its subject is a chain of VARIABLES and nothing in it says which net they are. This theorem puts the stem pool on both sides of one statement the kernel checks.