Convolution parameter-gradient bridges (the MNIST CNN train step's conv parameters) #
The MNIST CNN (conv → relu → conv → relu → maxpool → dense → relu → dense → relu → dense)
train step has two kinds of parameters: the dense classifier head (whose grads reuse
IR.weight_grad_bridge/IR.bias_grad_bridge) and the convolution kernels/biases,
whose gradient is a correlation, not an outer product. This file supplies the conv
analogue of the dense bridges.
As for the MLP, the cotangent the backward chain delivers at each conv layer's output flows
through a backward graph — here the Tensor3-level IR.Back3 (convBackDenote,
maxPoolBackDenote, with IR.denote_subst3 the chain rule), exactly as the MLP used
IR.Back (mlpCotOut0/mlpCotOut1). Given that cotangent c, the conv kernel and
bias gradients (the transpose-trick conv2dWeightGrad/conv2dBiasGrad) are the
certified Jacobian of conv2d — as a function of the flattened kernel / of the bias —
contracted with c. Both bridges are the .correct field of the proven conv
parameter VJPs (conv2dWeightGradHasVJP/conv2dBiasGradHasVJP). The statements are
about those witnesses' backwards; no rendered text appears in them. The link from a
rendered conv gradient op to these witnesses is that op's den theorem (see CnnFold).
With the dense bridges in IR and the Back3 cotangent chain, this gives a bridge for
every parameter of the CNN train step. (The SGD wrapping θ − lr·∇ is identical to the
linear/MLP case.)
The next section adds the same bridges for the depthwise bias and the stride-2 conv kernel and bias, which the MobileNetV2, ResNet-34 and ConvNeXt fold ties use.
The rest are the conv's Jacobians in closed form and its drifts, read off the same certified
VJPs: the kernel map (conv2d_weight_pdiv, the drift conv2d_kernel_drift_sum), the input map
(the kernel tap convTap, conv2d_input_pdiv3, the locality bound convTap_out_l1 and the drift
conv2d_input_l1_drift) and the bias map (conv2d_bias_pdiv, conv2d_flat_bias_drift_sum), with
the weight and bias gradients as a flat dot and sum (convWeightGrad_eq_dot,
convBiasGrad_eq_sum). The MNIST CNN descent rungs (SgdDescent.Cnn) consume them.
Conv weight-gradient bridge. At any cotangent c at the conv layer's output
(and any kernel point v = Kernel4.flatten W), the backward of
conv2dWeightGradHasVJP (the transpose-trick kernel gradient) equals the certified Jacobian of conv2d viewed as a function of the flattened
kernel, contracted with c. The convolution analogue of IR.weight_grad_bridge;
it is the .correct field of conv2dWeightGradHasVJP.
Conv bias-gradient bridge. Likewise the conv bias gradient (db[o] = Σ spatial c) is the certified Jacobian of conv2d wrt the bias, contracted with
c — the .correct field of conv2dBiasGradHasVJP.
Conv weight SGD step — SGD form of conv_weight_grad_bridge. At the flattened
kernel v, v − lr·(conv2dWeightGradHasVJP backward at c) equals
v − lr·(certified ∂conv/∂kernel · c). A rewrite by the bridge; no rendered text
appears in the statement.
Conv bias SGD step — SGD form of conv_bias_grad_bridge. Likewise
b − lr·(conv2dBiasGradHasVJP backward at c) equals
b − lr·(certified ∂conv/∂bias · c).
Depthwise bias output, certified. Likewise bⁿ = b − lr·(spatial reduce) denotes
b − lr·(certified ∂(depthwiseConv2d)/∂b · cotangent).
Stem conv weight output, certified. sWⁿ = sW − lr·(strided transpose-trick grad) denotes
sW − lr·(certified ∂(flatConvStride2)/∂sW · cotangent), via flatConvStride2WeightGradHasVJP
(the ch6 strided conv weight VJP).
Stem conv bias output, certified. sbⁿ = sb − lr·(spatial reduce) denotes
sb − lr·(certified ∂(flatConvStride2)/∂sb · cotangent).
Per-entry conv drift, slab-refined: a kernel perturbation moves the
output entry (o, hi, wi) by at most a times the ℓ1 mass of the
channel-o slab (each output reads only its own slab).
Per-entry conv drift against the TOTAL ℓ1 mass — the form the relu
margins consume.
ℓ1 conv drift: summed over all output entries, the drift is at
most (h·w)·a·‖e‖₁ — the spatial multiplicity h·w is the price of
weight sharing (each kernel entry touches every spatial position).
Closed form of the conv weight-map pdiv — extracted from the
certified VJP (conv2dWeightGradHasVJP) by contracting its
.correct field against a basis vector. Kernel entry (o,cc,kh,kw)
touches output (co,hi,wi) iff co = o, with coefficient the padded
input read convPad. NB the right-hand side does not mention v:
the weight map is affine, so its Jacobian is point-free — this is
what lets the gradient difference along a step segment collapse to
the head drift alone.
The padded-input window for a fixed kernel slot, flattened over the
(hi, wi) spatial grid — the left operand of the conv weight-grad dot.
Equations
- Proofs.convPadWin kH kW x cc kh kw s = Proofs.convPad kH kW x cc kh kw (finProdFinEquiv.symm s).1 (finProdFinEquiv.symm s).2
Instances For
The cotangent slab for a fixed output channel, flattened over (hi, wi).
Equations
- Proofs.cotWin cot o s = cot o (finProdFinEquiv.symm s).1 (finProdFinEquiv.symm s).2
Instances For
The conv weight gradient is the spatial dot Σ_{hi,wi} convPad · cot
(the contraction conv2d_weight_pdiv certifies as ∂L/∂W_{o,cc,kh,kw}),
re-expressed as a flat Fin (h·w) dot of the padded-input window against
the cotangent slab — the form the float dot rounds.
The kernel tap that multiplies input entry (ci,hi,wi) in output
entry (co,ho,wo) — the input-side Jacobian entry of conv2d.
Depends on the kernel only, never the input (conv is linear in its
input). Deliberately let-free, like convPad.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A single conv tap is bounded by the kernel magnitude (out-of-pad taps are
zero) — the per-entry bound the conv-2 backward dot_perturbed_close uses.
The tap as a kernel-offset indicator sum: |convTap| is the sum
over kernel offsets (kh,kw) of |W co ci kh kw| pinned to the
unique offset aligning input (hi,wi) with output (ho,wo). The
workhorse for both mass bounds: summing it over OUTPUTS pins
(ho,wo) per offset, summing it over INPUTS pins (hi,wi).
Output-side tap mass: one input entry feeds at most oc·kH·kW
outputs, each through a tap bounded by wK — the ℓ1→ℓ1 operator
factor of a conv crossing as a function of its input.
Closed form of the conv input-map pdiv3 — extracted from the
certified input-VJP (conv2dHasVJP3) by contracting its
.correct field against a basis cotangent. Point-free in x:
conv is linear in its input.
Flat-coordinate form of conv2d_input_pdiv3 — the shape the chain
rule through flatConv W₂ b₂ consumes.
The real conv-2 backward ∑ convTap·c2R is magnitude-bounded by the tap
ℓ∞-mass (c·(2h)·(2w))·w₂ times the cotangent bound CP — the (loose,
uniform) bound on the real conv-1 cotangent.
Per-entry conv input drift: each output reads ic·kH·kW padded
inputs through taps bounded by wK.
ℓ1 conv input drift: each input entry feeds at most oc·kH·kW
outputs, so the total output drift is at most oc·kH·kW·wK times
the total input drift — locality, not a spatial count.
ℓ1 conv bias drift: summed over all output entries, at most
(h·w)·‖e‖₁ — one bias entry feeds every spatial position of its
channel.
Closed form of the conv bias-map pdiv — extracted from the
certified VJP (conv2dBiasGradHasVJP) by contracting its
.correct field against a basis vector, exactly as
conv2d_weight_pdiv. Bias entry o touches output (co,hi,wi)
iff co = o, with coefficient 1 — the Kronecker channel indicator.
Point-free (the bias map is affine), so along a step segment only
the head gradient moves.