5 ResNet-34

Deeper networks used to stop training

Before 2015, the dominant assumption in image classification was “deeper is better, up to a point.” The “up to a point” part was not metaphorical. If you took a 20-layer CNN that trained to 70% val accuracy and added 12 more convolutional layers, you didn’t get a 32-layer model with 72% accuracy. You got a 32-layer model that, after the same training budget, fit the training set worse than the 20-layer one did. The 32-layer model had strictly more capacity. It still trained worse. Something about deep stacks of convolutions made gradient flow degrade in a way that the optimizer couldn’t navigate around.

He et al. 2015 (arXiv:1512.03385) had the right observation: if the 12 extra layers in the deeper network were initialized to compute the identity, the 32-layer network would have at least the 20-layer’s performance, because it could replicate it exactly. So the question was not “can a deep network represent what a shallow one represents?” It provably could. The question was: why is optimizing 12 free-form layers to recover identity so much harder than just leaving identity there?

5.1 Run it first

Before any of the math, train the thing. Four commands and about fifty minutes of GPU time:

lake exe cache get                            # Mathlib oleans, ~30 s
./scripts/datasets/download_imagenette.sh     # 330 MB dl, 2.4 GB unpacked
lake build resnet34-verified-adam
./.lake/build/bin/resnet34-verified-adam data

On one RTX 4060 Ti (CUDA 12.9), from runs/2026-09-12-r34-ablation-fp32-seeds/full_s2.log: seed 2 of the five that §5.5.2 averages, run by the ablation driver’s full arm, which is this binary’s render and recipe under LEAN_MLIR_SEED=2. XLA’s startup banner and the resident-parameter notices are removed, the network description line is wrapped, each interval is wrapped onto an indented continuation, and epochs 5 through 75 are elided:

[pjrt_ffi] XLA backend: PJRT 0.114, 1 device(s)
[pjrt_ffi] command buffers: enabled (CUDA default)
[pjrt_ffi] compiled verified_mlir/resnet34_adam_train_step.mlir
             (@resnet34_adam_train_step, 405 outputs, 1 replica) in 6127 ms
[pjrt_ffi] compiled verified_mlir/resnet34_fwd.mlir
             (@resnet34_fwd, 1 outputs, 1 replica) in 596 ms
[pjrt_ffi] compiled verified_mlir/resnet34_fwd_eval.mlir
             (@resnet34_fwd_eval, 1 outputs, 1 replica) in 293 ms
Real ResNet-34 on Imagenette 224² (7×7-s2 stem→3×3-s2 overlapping max pool→
  [3,4,6,3] blocks w/ batch-norm, He et al. option-B 1×1 projection shortcuts,
  no conv biases; 56→28→14→7→GAP→dense)
  via the VERIFIED renderer → XLA/PJRT → GPU
  xla/pjrt verified_mlir/resnet34_adam_train_step.mlir
  xla/pjrt verified_mlir/resnet34_fwd.mlir
  xla/pjrt verified_mlir/resnet34_fwd_eval.mlir
  train 9469, val 3925; bs 32, ResNet-34 adam
    (cosine+warmup 3ep, baseLR 0.001000), He init
  running-stats BN: 36 layers, 17024 stat floats → eval via @resnet34_fwd_eval
Epoch 1/80: loss=1.971035 lr=0.000333
  epoch 1: val_acc = 1239/3925 = 31.566879%  top5 = 2766/3925 = 70.471338%
    [95% CI 30.13–33.04]
Epoch 2/80: loss=1.553382 lr=0.000667
  epoch 2: val_acc = 1471/3925 = 37.477707%  top5 = 3123/3925 = 79.566879%
    [95% CI 35.98–39.00]
Epoch 3/80: loss=1.381944 lr=0.001000
  epoch 3: val_acc = 1880/3925 = 47.898089%  top5 = 3159/3925 = 80.484076%
    [95% CI 46.34–49.46]
Epoch 4/80: loss=1.311593 lr=0.001000
  epoch 4: val_acc = 1851/3925 = 47.159236%  top5 = 3547/3925 = 90.369427%
    [95% CI 45.60–48.72]
Epoch 76/80: loss=0.502131 lr=0.000007
  epoch 76: val_acc = 3536/3925 = 90.089172%  top5 = 3859/3925 = 98.318471%
    [95% CI 89.11–90.99]
Epoch 79/80: loss=0.502245 lr=0.000000
  epoch 79: val_acc = 3535/3925 = 90.063694%  top5 = 3859/3925 = 98.318471%
    [95% CI 89.09–90.96]
Epoch 80/80: loss=0.502085 lr=0.000000
  epoch 80: val_acc = 3535/3925 = 90.063694%  top5 = 3859/3925 = 98.318471%
    [95% CI 89.09–90.96]
done (trained ResNet-34 adam + cosine/warmup via packed threading).

Eighty epochs at about 35 seconds each, 47 minutes in all, and 90.06% top-1 with 98.32% top-5 on Imagenette’s 3,925-image validation split. This is one seed of five; the five land at \(89.99 \pm 0.32\) top-1 (§5.5.2), and that mean is the number every later chapter compares against.

The residual block: ask for the difference, not the function

Their fix was a one-line architectural change. Instead of asking each block to learn a function \(y = f(x)\), ask it to learn a function \(y = f(x) + x\). The block’s job is no longer to become the new representation. Its job is to learn what to add to the current representation. At initialization, with randomly-small \(f\), each block is approximately the identity, and a stack of 16 such blocks is approximately a stack of 16 identities, which is to say, approximately the input. The network starts out near-identity at every depth and only gradually takes on structure as \(f\) trains. The optimization problem becomes “what residual should each block add” instead of “what function should each block be,” and the former turns out to be dramatically easier.

The change to the architecture is one + sign. The change to the training dynamics is the difference between “18 layers is about as deep as we can go” and “152 layers trains stably, so let us also add another zero on the ImageNet leaderboard.”

Why the proof is a one-liner

From the framework’s perspective, what is a residual block? \(\mathrm{residual}(x) = f(x) + \mathrm{id}(x)\), a sum of two functions sharing the same input. The VJP of an additive fan-in is “send the upstream gradient through both branches and add” (Theorem 12); the VJP of \(\mathrm{id}\) is the identity on the gradient (Theorem 14), and the VJP of \(f\) is whatever the inner block’s machinery gives us. Composition is just \(\mathrm{vjpComp}\). So the residual VJP is the additive fan-in lemma, with \(\mathrm{id}\) plugged into one slot.

That is Theorem 64 below, and its proof is one line. The residual is the one theorem the idea needs, and that theorem is mechanical. The engineering revolution was not in the math. It was in the realization that this operation was the missing piece for training deep networks. The fact that the framework absorbs the new architecture without any new math is the value proposition: once the foundation rules are in place, the next decade of image recognition follows from composing them.

ResNet-34 is sixteen of these blocks

ResNet-34 (the smallest “deep” variant in the original paper) is built from 16 residual blocks arranged in four stages of depths 3, 4, 6, 3, at channel widths 64, 128, 256, 512. Each stage starts with a stride-2 downsample (halving spatial resolution) before its stack of stride-1 blocks. The stages are glued together by a stem (a 7\(\times \)7 conv at stride 2 plus a max-pool, taking 224\(\times \)224\(\times \)3 input to 56\(\times \)56\(\times \)64 features) and a head (global average pool plus a 512-to-10 dense layer). Total: 34 weight-bearing layers, 21.3M parameters.

Two pieces of this template are new and worth naming:

1. The 7\(\times \)7 stride-2 stem. Earlier chapters’ networks operated at full input resolution. ResNet aggressively downsamples at the input so the bulk of compute happens at lower spatial resolution. The stem is one big conv that gets us from 224\(\times \)224 to 56\(\times \)56 in a single step.

2. Global average pool instead of flatten-plus-dense. Chapters 3 and 4 ended in a .flatten followed by a dense layer (\(6272 \to 512\) on MNIST, \(128 \to 512\) on CIFAR) that held most of the network’s parameters. ResNet collapses the final 7\(\times \)7\(\times \)512 feature map to a 512-vector by spatial averaging, then runs a single 512-to-10 dense. No flatten layer. The architectural move alone drops the model from what would have been a \(\sim \)200M-parameter AlexNet-era spec down to 21.3M.

Every chapter after this one is a variation on this template. MobileNetV2 swaps in depthwise-separable blocks. EfficientNet adds squeeze-and-excitation to them. ConvNeXt swaps in its own block. ViT replaces the whole convolutional spine with patches and attention. The stem-stages-head template, and the residual fan-in pattern, persist.

5.2 The theorems

Figure 5-1 is the dependency graph of this section.

The ladder.

From here every ImageNet chapter proves the same six statements about its network, and this is the first time all six appear. (i) The whole network at batch \(N\) has a VJP: the backward composed from the stages’ backwards is the \(\operatorname {pdiv}\)-contracted Jacobian of the forward. (ii) The hand-written backward chain the renderer emits is that backward. (iii) The emitted training step is the certified step: each of its gradient nodes denotes the certified batch gradient at the chain cotangent of the loss. (iv) Each node is the loss’s derivative in its parameter. (v) The backward is not the zero map, at one fixed weight setting — a seal. (vi) The data-parallel render’s mean over replicas is one device’s step on the global batch. Statements (i) and (iv) take the smooth-point hypotheses — \(\varepsilon {\gt} 0\) at every BatchNorm, the batch’s activations off every ReLU corner, and at the stem pool no tie for (i), none but twins for (iv); (ii) takes the stem’s and head’s clauses and a VJP witness per block; (iii) and (vi) are identities of the emitted text and take none; (v) is at fixed weights.

Twins at the stem pool. The stem’s \(3 \times 3\)/s2 pool is certified together with the ReLU before it (stemReluPoolLayer), so an all-zero window is admitted: every pre-activation there is negative and the pair is locally constant. What the per-example condition (StemPoolSmoothAt) still excludes is a window whose positive maximum sits at two cells. Real batches have such windows, from two cells reading identical input patches in a flat image region. There the network has no derivative in the image, so an input-gradient statement cannot hold; but the tied cells are the same function of the stem’s weights, so the loss gradients in the parameters allow them (StemPoolTwinAt), and routing a tied window’s cotangent to either twin gives the same parameter gradient (r34Stem_select_grads_eq). That is the “up to twins” in the hypothesis above, and why the theorem is instantiated at any routing to a maximal cell.

5.3 Example: ResNet-34 on Imagenette

ResNet-34 on 224\(\times \)224 Imagenette: 10 classes, real photographs, the transition point from “classroom dataset” to “actual image recognition.”

The architecture

The same vertical column as the previous chapters, now at production scale: a \(7 \times 7\) stride-2 stem and a max-pool drop the \(224 \times 224 \times 3\) input to \(56 \times 56 \times 64\), then four stages of residual blocks (depths \(3, 4, 6, 3\) at widths \(64, 128, 256, 512\)) do the work, and a global average pool replaces the flatten-plus-fat-dense head. Figure 5-2 is the network, and its inset shows the one new piece: each residual block adds its input back, \(y = f(x) + x\).

The verified trainer, which is the pattern every later chapter reuses

This is the reference configuration; Chapters 6 through 9 each swap the layers list and change almost nothing else.

import LeanMlir.Verified.NetsCore
import LeanMlir.Verified.Train

-- 1. The network. A VerifiedNetSpec, not a NetSpec: `slug` names the
--    committed render, and `bnChannels` drives BN statistic threading.
def resnet34Verified : VerifiedNetSpec where
  name     := "ResNet-34"
  slug     := "resnet34"
  inC      := 3
  imageH   := 224
  imageW   := 224
  data     := .imagenette
  layers   := [
    .convBnNB 3 64 7 2,          -- 7x7-s2 stem, no conv bias   224->112
    .maxPool 3 2,                -- He et al. 3x3-s2 OVERLAPPING 112->56
    .residualStage  64  64 3 1,  -- stage 1, 3 blocks            @56
    .residualStage  64 128 4 2,  -- stage 2, downsample + 3      56->28
    .residualStage 128 256 6 2,  -- stage 3, downsample + 5      28->14
    .residualStage 256 512 3 2,  -- stage 4, downsample + 2      14->7
    .globalAvgPool,              -- replaces flatten + fat dense
    .dense 512 10 ]
  blurb := "Real ResNet-34 on Imagenette 224² (7×7-s2 stem->3×3-s2 overlapping
            max pool->[3,4,6,3] blocks w/ batch-norm, He et al. option-B 1×1
            projection shortcuts, no conv biases; 56->28->14->7->GAP->dense)
            via the VERIFIED renderer -> %LOWERER% -> GPU"
  bnChannels := #[64, 64,64, ... ]   -- all 36, in forward order

-- 2. The schedule. Everything the optimizer needs beyond the render.
def resnet34AdamConfig : VerifiedConfig where
  epochs    := 80
  batchSize := 32

-- 3. The entry point: AdamW, cosine with a 3-epoch warmup, baseLR 1e-3.
--    Variant, batch and rate are overridable; the defaults are Run it first's.
def runResnet34Adam (argv : List String) : IO Unit := do
  let variant := (← IO.getEnv "LEAN_MLIR_VARIANT").getD "adam"
  let bs      := ((← IO.getEnv "LEAN_MLIR_BATCH").bind (·.toNat?)).getD
                   resnet34AdamConfig.batchSize
  let baseLR := match (← IO.getEnv "LEAN_MLIR_BASE_LR_U").bind (·.toNat?) with
    | some u => u.toFloat * 1e-6     -- micro-units: 100000 is 0.1
    | none   => 0.001
  resnet34Verified.toNet.trainAdamSched
    { resnet34AdamConfig with batchSize := bs }
    (argv.head?.getD "data") baseLR 0.9 0.999 3 variant

The one thing in that listing to carry forward is that the recipe is arguments, not architecture. The learning rate, the momentum pair, the warmup length and the variant string are all passed to the driver; none of them is a property of the network. Swapping AdamW for momentum is a different argument against the same proven gradient, which is what makes §5.5.2’s ablation a measurement of the recipe rather than of the model — and what Chapter 4 used to put three optimizers on one net.

The schedule. Chapter 4 trained at a constant rate. Annealing the rate to zero on a cosine is worth about five points here (\(-5.00 \pm 2.60\) in §5.5.2), the largest contribution of any knob in the recipe except augmentation itself, and more than the optimizer, the warmup, the weight decay and the label smoothing combined. It buys that by taking large steps while the loss surface is still coarse and small ones once it is not, which is the reason the warmup exists at the other end and the reason a constant rate has to be a compromise between the two.

This is the first chapter that uses the full production recipe (AdamW + cosine + warmup + weight decay + augmentation + label smoothing). Also the first chapter where .globalAvgPool replaces the flatten-plus-fat-dense head. Global average pooling (GAP) collapses each \(C \times H \times W\) feature map to a length-\(C\) vector by averaging over the spatial dimensions,

so the classifier head sees one summary scalar per channel instead of the full \(C \cdot H \cdot W\) flattened activation.

GAP is not ResNet’s invention. It comes from Network in Network (Lin et al. 2013, arXiv:1312.4400), which proposed it precisely as a replacement for the fully-connected layers at the top of a convolutional net: one feature map per class, averaged, fed straight to the softmax, with no fully-connected parameters to overfit. Inception-v1 (GoogLeNet, Szegedy et al. 2014, arXiv:1409.4842) adopted it a year later — dropping the fully-connected stack for an average pool and a single linear classifier — and reported it worth about \(0.6\% \) top-1 on its own. By 2015 it was standard equipment, which is why ResNet uses it without argument. We’ll see GAP again as the “Squeeze” step inside the squeeze-and-excitation block in Chapter 7, and at the head of every post-2015 vision architecture in the bestiary.

Results

§5.1 has the run: 80 epochs on one RTX 4060 Ti, finishing at 90.06% top-1 and 98.32% top-5 on Imagenette’s 3,925-image validation split, one seed of the five that average \(89.99 \pm 0.32\). That is the going rate for a scratch-trained ResNet-34 at this resolution and data size. From the log:

• Per-step time is about 120 ms at batch 32, 295 steps to the epoch, dominated by the four .residualStage groups where the \(3 \times 3\) convolutions at 64, 128, 256 and 512 channels are. The first stage alone, at 64 channels on the \(56 \times 56\) grid, is \(3 \times 3 \times 64 \times 64\) multiply-accumulates per output location, about \(1.2 \times 10^8\) per convolution, six convolutions in the stage, times the batch, and the backward costs about twice the forward again.

• Final loss plateaus near 0.50, not zero. That’s the label-smoothing floor: with \(\epsilon = 0.1\) and \(K = 10\) classes the smoothed target puts \(1 - \epsilon + \epsilon /K = 0.91\) on the true class and \(\epsilon /K = 0.01\) on each of the other nine, and the minimum possible cross-entropy against it is that target’s entropy, \(-0.91 \log 0.91 - 9 \cdot 0.01 \log 0.01 \approx 0.500\). The 0.502 at epoch 80 sits on that floor, so the model has essentially converged. More epochs would mostly just extend training time without budging the loss.

• BN layers: 36. Every residual block contains two normalized convolutions, and there are 16 blocks across the four stages (3+4+6+3): 32. The projection shortcuts that open stages 2–4 carry one each, and the stem one, for 36 total. Each one proves its own VJP via Theorem 50 and composes with the rest of the network via Theorem 11.

5.4 MLIR: Residual

What is already proven. A residual block is \(\mathrm{residual}(x) = f(x) + x\), an additive fan-in, where \(f\) is the conv \(\to \) BN \(\to \) relu \(\to \) conv \(\to \) BN inner block. As Theorem 64 states, its reverse-mode derivative is the additive-fan-in rule with the identity in one slot: “send the upstream gradient through both branches and add”. residualHasVJPAt proves exactly this at the evaluation point (a one-line proof: the fan-in lemma with the identity’s VJP plugged into one slot), and the inner \(f\)’s VJP is the convolution and BatchNorm backward (Theorems 35, 50). The whole block, and a tower of sixteen of them, composes by the chain rule vjpCompAt (Theorem 11).

The gap and how we close it. The residual fan-in is the structural heart of a deep ResNet, and it is visible in the emitted text. The forward saves \(a = f(x) + x\) and returns \(\mathrm{relu}(a)\). The backward first pushes the incoming cotangent back through that ReLU (a compare/select at the saved \(a\)), then runs \(f\)’s own backward on the result, and then, and this is the fan-in, adds the result of the ReLU mask to it again. Here it is in verified_mlir/resnet34_sgd_train_step.mlir for the last block of the fourth stage (s4b1: 512 channels at \(7\times 7\), batch 32), with the inner backward through BN\(_2\), conv\(_2\), the mid ReLU and BN\(_1\) elided down to conv\(_1\)’s input gradient (SSA names the artifact’s, lines wrapped):

%v1134 = stablehlo.reshape %v1095 : (tensor<32x25088xf32>)
      -> tensor<32x512x7x7xf32>
%v1135 = stablehlo.constant dense<0.0> : tensor<32x512x7x7xf32>
%v1136 = stablehlo.compare GT, %v1134, %v1135 : (tensor<32x512x7x7xf32>,
      tensor<32x512x7x7xf32>) -> tensor<32x512x7x7xi1>
%v1137 = stablehlo.select %v1136, %v1133, %v1135 : tensor<32x512x7x7xi1>,
      tensor<32x512x7x7xf32>
// ...
%v1211 = stablehlo.reverse %s4b1W1, dims = [2, 3] : tensor<512x512x3x3xf32>
%v1212 = stablehlo.transpose %v1211, dims = [1, 0, 2, 3]
      : (tensor<512x512x3x3xf32>) -> tensor<512x512x3x3xf32>
%v1213 = stablehlo.convolution(%v1210, %v1212)
      dim_numbers = [b, f, 0, 1]x[o, i, 0, 1]->[b, f, 0, 1],
      window = {stride = [1, 1], pad = [[1, 1], [1, 1]],
      lhs_dilate = [1, 1], rhs_dilate = [1, 1]}
      {batch_group_count = 1 : i64, feature_group_count = 1 : i64}
      : (tensor<32x512x7x7xf32>, tensor<512x512x3x3xf32>)
      -> tensor<32x512x7x7xf32>
// ...
%v1215 = stablehlo.reshape %v1214 : (tensor<32x25088xf32>)
      -> tensor<32x512x7x7xf32>
%v1216 = stablehlo.reshape %v1138 : (tensor<32x25088xf32>)
      -> tensor<32x512x7x7xf32>
%v1217 = stablehlo.add %v1215, %v1216 : tensor<32x512x7x7xf32>

Read it against the theorem. %v1134 is the saved pre-ReLU sum \(a\) and %v1133 the cotangent arriving from the head; %v1137 is their select, the cotangent at the fan-in. It then appears twice. Once it enters \(f\)’s backward, whose last operation is the convolution %v1213 against the first kernel reversed and transposed (%v1211, %v1212: Chapter 3’s reverseSwap, with the two steps in the other order), giving the gradient through the residual branch, %v1215. And once it is added directly: %v1216 is the same %v1137 flattened and reshaped (%v1138), and %v1217 = %v1215 + %v1216 is “send the gradient through both branches and add”. The skip term is the very tensor the branch term started from, which is why the gradient survives all sixteen blocks instead of attenuating away, and %v1218, its flattening, is the cotangent every parameter node of the block below reads. r34IdCotIn_eq_vjp is the theorem that this seven-node subgraph denotes \((\texttt{r34IdBHasVJPAt}).\mathrm{backward}\), the certified VJP of the whole block, and Theorem 68 threads it through all sixteen; the three downsampling blocks, whose skip is a \(1\times 1\) convolution and BatchNorm rather than the identity, have their own (r34DownCotIn_eq_vjp).

Caveats.

• The fan-in add holds at every input, because addition is linear.

• Two ReLUs per block are smooth-point bridges, the mid-block one and the post-add one (no pre-activation exactly zero), and the two BatchNorms inside \(f\) carry their \(\epsilon {\gt} 0\) condition (Theorem 50).

• Shape. The listing is one block of the trained net at batch 32; the same seven nodes repeat for all sixteen.

5.5 The recipe

5.5.1 What’s in it

Six ingredients first appear here, none of which are layers. They all live in TrainConfig or training code. They don’t touch the network; what each one is worth is measured in §5.5.2.

Adam (Kingma & Ba, 2014, arXiv:1412.6980). Replaces vanilla SGD. Maintains per-parameter running estimates of the first and second moments of the gradient and uses them for an adaptive per-parameter learning rate. Much faster convergence than SGD on most tasks, much more forgiving of learning-rate choice.

Cosine learning-rate schedule (Loshchilov & Hutter, 2016, arXiv:1608.03983). After warmup, the learning rate decays from its peak to near-zero following \(\mathrm{lr}(t) = \mathrm{lr}_{\max } \cdot \tfrac {1}{2}(1 + \cos (\pi t / T))\). Smoother than step schedules, and consistently produces slightly better final losses in practice. Warmup-then-anneal first won at scale at Stanford’s DAWNBench in 2018, in two forms: the CIFAR-10 entry ran Smith’s 1cycle, a linear triangle with a short anneal, and the ImageNet entry a four-epoch warmup into step decay, with progressive resizing (Howard et al., 2018) on top. The lineage traces back to Leslie Smith’s cyclical learning rates (Smith 2015, arXiv:1506.01186). The cosine form, with warmup and label smoothing, is He et al. 2018’s “Bag of Tricks” (arXiv:1812.01187), and that is the recipe this chapter’s ImageNet rows run.

Warmup (Goyal et al., 2017, arXiv:1706.02677). Linearly ramps the learning rate from zero to its peak over the first few epochs (3 for ResNet-34). Stabilizes early training when gradients are still reorganizing randomly-initialized weights. Becomes essential for larger models and larger batches; Chapter 9’s ViT-Tiny trains with one.

Weight decay. Adds a small L2 shrink to all trainable weights each step: \(w \leftarrow w - \eta \lambda w\), with \(\lambda = 10^{-4}\) here. Regularizer, discourages weights from growing without bound. Loshchilov & Hutter’s “decoupled” variant (AdamW, 2017, arXiv:1711.05101) is what actually ships in modern pipelines, and it’s what TrainConfig.weightDecay implements.

Augmentation. Our pipeline does random crops (\(256 \to 224\)) and random horizontal flips on Imagenette, hflip only on CIFAR, and nothing on MNIST. Lives in the data pipeline, not the network. We will explore data augmentation strategies in upcoming chapters.

Label smoothing (Szegedy et al., 2016, arXiv:1512.00567). Replaces the one-hot target with the smoothed \((1 - \varepsilon )\, \mathrm{onehot} + \varepsilon / K\): \(1 - \varepsilon + \varepsilon /K\) on the true class and \(\varepsilon / K\) on every other, the form Szegedy et al. give and the one TrainConfig.labelSmoothing and timm implement. Stops the network from producing arbitrarily large logits on the correct class, which keeps training stable and improves calibration. Explains the 0.50 loss floor in the Results section above: the target’s entropy at \(\varepsilon = 0.1\), \(K = 10\) is \(-0.91 \log 0.91 - 9 \cdot 0.01 \log 0.01 \approx 0.500\).

Every chapter after this one uses the same six ingredients. The NetSpec changes, and the recipe stays.

5.5.2 Ablation: what each ingredient contributes

So how much does each ingredient actually earn? Figure 5-3 is the full recipe and six leave-one-out variants, ResNet-34 on Imagenette, 80 epochs each. Every variant keeps the recipe intact except for the one component it names, so its difference from the full recipe measures that component’s contribution given everything else is present — not the order-dependent story an additive ladder tells.

Each point is plotted as its difference from the full recipe rather than as an accuracy, so the line at zero is the baseline and distance from it is what the ingredient contributes. The intervals are paired by seed, since arms sharing a seed share initialization and data order. An arm whose bar crosses zero is not placed, however suggestive its mean.

The two panels are the same seven arms in the two precisions, and the reason to draw them side by side is that a real effect should not move. None does: every arm’s fp32 mean falls inside the bf16 interval and every bf16 mean inside the fp32 one. Four arms are resolved in both. Label smoothing is resolved in fp32 (\(-0.69 \pm 0.42\)) but not bf16 (\(-0.50 \pm 0.62\)), where the means agree and only the interval is wider. Weight decay is resolved in neither (\(-0.02 \pm 0.61\), \(+0.14 \pm 0.45\)): ten runs do not place it, and the honest reading is that here it earns nothing measurable.

The cosine bar is the widest in both precisions because the constant-rate arm finishes wherever its noisy trajectory happens to be at epoch 80: fp32 seeds spread \(82.0\)–\(86.8\) (sd \(1.93\)), bf16 \(82.6\)–\(87.9\) (sd \(2.18\)). Its contribution is large and imprecise, and both precisions agreeing on how imprecise says the width belongs to the arm, not to either number format.

What the optimizer row is really measuring. Reading the \(-\)AdamW gap as “what the adaptive optimizer buys” assumes its replacement got a rate that suits it. Heavy-ball at \(\mu = 0.9\) multiplies the effective step by \(1/(1-\mu ) = 10\), so the comparison that isolates momentum is against plain SGD at ten times the rate — \(0.1\), not \(0.01\) — where both take the same size step and differ only in whether a velocity carries it. Figure 5-4 is that comparison.

At a matched step, plain SGD does not merely keep up with momentum — it finishes slightly ahead, by a paired \(+0.403 \pm 0.162\) with all five seeds agreeing in sign. The two lower bars overlap while that difference is resolved, which is no contradiction: the arms share seeds, so their difference is better determined than either rung’s distance from the baseline. The baseline carries no bar for the same reason — its difference from itself is zero on every seed, and its own spread sits inside the other two bars. The trajectories say the same about shape: the two never separate across the eighty epochs.

Momentum is therefore not doing something a velocity-free step cannot; it is taking a bigger one, slightly less well. The \(-2.27 \pm 0.59\) charged to “removing AdamW” is almost entirely the \(10\times \) momentum supplies for free: hold the effective step fixed and the gap closes to \(-1.86 \pm 0.57\), the remainder running the other way.

That is this ablation’s own limit: every non-adaptive row’s difference is partly a claim about how well its learning rate suits it, and an adaptive optimizer’s insensitivity to that rate hides the dependence. The figure measures the recipe as tuned, not its ingredients in isolation.

Augmentation is the largest single contribution (\(-7.33 \pm 0.49\) fp32, \(-7.11 \pm 0.38\) bf16; three times the next-largest knob). Imagenette has 9,469 training images for a 21.3M-parameter network, so without the random crop and flip the model overfits hard. Most of what the rest of the recipe gets credit for is augmentation.

5.6 ImageNet recipe

5.6.1 ResNet-34: the 2018 recipe

The Imagenette runs above all trained on \(\sim \)9.5K images for 80 epochs. This section is the same 21.8M-parameter network on 1.28M images and 1000 classes, trained on the standard 90-epoch schedule. The architecture is unchanged. Only the dataset, the output head width, and the training schedule differ.

This section runs it twice. The reference is the Lean\(\to \)JAX trainer of §B.4.2: JAX traces the generated program and hands XLA the graph. The verified path hands XLA pretty(provenGraph) — the rendered artifact the proofs reason about — through the PJRT C API, with no Python at run time. Same architecture, same recipe, same data loader, same compiler; the only difference is who wrote the StableHLO. Every ImageNet section reports the reference first, the verified path second, and then the two side by side.

The recipe in full: SGD with momentum \(0.9\) at batch 256, cosine LR with a 5-epoch warmup from peak \(0.1\), label smoothing \(0.1\), a random-resized crop to \(224\times 224\) plus a horizontal flip, \(\ell _2\) weight decay \(10^{-4}\) on the convolution and dense weights with BatchNorm’s \(\gamma \), \(\beta \) and the biases left undecayed, every block’s second BatchNorm starting its \(\gamma \) at \(0\), and running statistics that decay at \(0.9\). The crop is torchvision’s RandomResizedCrop (\(8\)–\(100\% \) of the area at a \(\frac{3}{4}\)–\(\frac{4}{3}\) aspect ratio, bilinear) on both halves, from the one generated shim. SGD with momentum and the weight decay are the original paper’s; the cosine schedule, the warmup, the label smoothing, the random-resized crop, the undecayed BatchNorm parameters and the zero-\(\gamma \) are He et al. 2018’s Bag of Tricks. What the rows do not take from that paper, each a training-time change that no later chapter’s recipe shares either: 120 epochs, Nesterov momentum, Xavier initialization, the hue/saturation/brightness jitter with PCA noise, and the ResNet-D downsampling blocks — the networks here are torchvision’s, ResNet-B in that paper’s naming and ResNet v1.5 elsewhere: the stride-2 on a bottleneck’s \(3\times 3\) rather than its first \(1\times 1\).

The reference (JAX)

The reference trainer is jax/MainResnetImagenet.lean, built as lake build resnet34-imagenet, with .imagenet streamed through tfds. It runs in bf16 — the convolutions cast to bfloat16 against fp32 master weights, the classifier head left in fp32 — which is a throughput choice rather than a fidelity one, and is why its column is the faster of the two in Table 5-3. Table 5-1 is the run.

That fp32 scoring is how the verified path and timm score, and the run’s own bf16 evaluation lands within \(0.01\) of it. Figure 5-5 is the run, epoch by epoch.

The bend near epoch 5 is the end of warmup; the steady late climb is the cosine anneal.

The verified path (PJRT)

The verified trainer is apps/imagenette/MainResnet34Imagenet.lean, built as lake build resnet34-imagenet-verified:

-- 1. Same backbone as the Imagenette net, 1000 classes instead of 10.
def resnet34ImagenetVerified : VerifiedNetSpec where
  name     := "ResNet-34 (ImageNet-1k)"
  slug     := "resnet34in"
  inC      := 3
  imageH   := 224
  imageW   := 224
  data     := .imagenet
  shimScript := "generated_resnet34_imagenet_shim.py"
  layers   := [
    .convBnNB 3 64 7 2,          -- 7x7-s2 stem -> BN -> relu    224->112
    .maxPool 3 2,                -- He et al. 3x3-s2, OVERLAPPING 112->56
    .residualStage  64  64 3 1,  -- stage1: 3 identity            @56
    .residualStage  64 128 4 2,  -- stage2: downsample + 3        56->28
    .residualStage 128 256 6 2,  -- stage3: downsample + 5        28->14
    .residualStage 256 512 3 2,  -- stage4: downsample + 2        14->7
    .globalAvgPool,
    .dense 512 1000 ]
  blurb := "ResNet-34 on full 1000-class ImageNet via the VERIFIED renderer ->
            %LOWERER% -> GPU, with the tfds batch shim supplying the same
            augmentation the Lean->JAX reference trainer uses"
  runningBN := true    -- 36 BatchNorms, read off the layer list

-- The head is the ONLY thing that may differ from the 10-class net.
-- Anything else moving means the spec drifted from its Imagenette twin.
#guard resnet34ImagenetVerified.toSpecs.size == resnet34Verified.toSpecs.size
#guard resnet34ImagenetVerified.toSpecs.pop.pop == resnet34Verified.toSpecs.pop.pop
#guard resnet34ImagenetVerified.toSpecs.back!  == (#[1000], 2)

-- 2. 90 epochs at batch 256.
def resnet34ImagenetConfig : VerifiedConfig where
  epochs    := 90
  batchSize := 256

-- 3. The entry point. Heavy-ball momentum, cosine with a 5-epoch warmup
--    at peak 0.1, weight decay 1e-4, label smoothing 0.1.
-- ⚠ LEAN_MLIR_EPOCHS *sets* the schedule; MAX_EPOCHS only ever CAPS it, and
--    `totalSteps := cfg.epochs * nb / accK` is what the cosine anneals over,
--    so capping at 90 would keep annealing over the default.
def runResnet34Imagenet (argv : List String) : IO Unit := do
  let variant := (← IO.getEnv "LEAN_MLIR_VARIANT").getD "mom256"
  let bs      := ((← IO.getEnv "LEAN_MLIR_BATCH").bind (·.toNat?)).getD
                   resnet34ImagenetConfig.batchSize
  let epochs  := ((← IO.getEnv "LEAN_MLIR_EPOCHS").bind (·.toNat?)).getD
                   resnet34ImagenetConfig.epochs
  let baseLR := match (← IO.getEnv "LEAN_MLIR_BASE_LR_U").bind (·.toNat?) with
    | some u => u.toFloat * 1e-6
    | none   => 0.1
  resnet34ImagenetVerified.toNet.trainAdamSched
    { resnet34ImagenetConfig with batchSize := bs, epochs := epochs }
    (argv.head?.getD "data") baseLR 0.9 0.999 5 variant

Three things in it are worth pulling out, because they are what makes the listing a claim rather than a description.

The slug is the artifact. resnet34in names verified_mlir/resnet34in_<variant>_train_step.mlir — momdp64wxbf16 for the run below — which is pretty(provenGraph) off the same renderer every earlier chapter used. Scaling to ImageNet needed nothing new in it. nClasses, the batch, the optimizer and the slug are all ordinary parameters, so the ImageNet artifacts are three #evals of machinery that was already proved. What had to be built was the data path, not the compiler.

The #guards pin it to the Imagenette net. The 1000-class spec must be the 10-class one with a different head, and the three guards fail the build if any other parameter shape moves. That is what licenses reading the Imagenette chapter’s theorems as being about this network’s body.

The shimScript is per-net and decides the data. It names this net’s own generated augmentation shim — the same shim the reference consumes, which is what makes the two a matched pair rather than two separate stories.

It runs with:

lake run r34-default-bf16-4gpu

The job config behind that name, scripts/jobs/r34-default-bf16-4gpu.conf, carries the device list, both replica knobs, the variant, the per-replica batch and the feed setting; §C says what the supervisor behind it does. Table 5-2 is the run.

The proof-carrying tier reaches this render as a step. Theorems 68 and 74 are stated at either precision, and read over \(\mathbb {R}\) the bf16 text’s gradient nodes are the certified ones. What they do not reach is the rounding: that the hardware rounds where the text says and nowhere else is trusted, as it is at every op of an f32 render.

The two paths, side by side

The two paths agree to \(0.16\) points on top-1 and \(0.15\) on top-5, and that is inside what one run can resolve. At \(n = 50{,}000\) the 95% Wilson interval is \(\pm 0.38\) points on either top-1 — \([73.59, 74.36]\) for the reference, \([73.75, 74.52]\) for the verified path — so the gap in the table is under half the interval, and at this scale a gap under about \(0.4\) points is not yet a result in either direction. That is the floor every side-by-side table in this book is read against. Paired on the same images the reading is the same: the two checkpoints disagree on \(5{,}807\) of them, \(2{,}863\) one way and \(2{,}944\) the other, and McNemar’s exact test puts \(p = 0.29\) on the \(81\) images between them.

The two halves ran one after the other on the same four cards (runs/2026-10-20-r34-bot-jax, runs/2026-10-20-r34-bot-verified), one seed per arm.

Both paths normalize over the global \(256\): the reference’s @jit mesh reduces the batch statistics across its shards, and each of the verified render’s 36 BatchNorms all-reduces its mean and variance across the four replicas — the data-parallel step Theorem 74 ties to one device’s step at \(256\).

The curves converge; they do not merely end together. The middle of the schedule is noisy on both paths — at peak learning rate SGD moves top-1 by a point or two between consecutive epochs, in both directions, three at the worst on either path — so the row is read for its ends. The verified path leads by one to three points through the first third and the lead closes as the cosine anneals: over the last fifteen epochs the two average within \(0.15\) of each other on top-1 and \(0.20\) on top-5. Table 5-4 is the selected epochs and Figure 5-6 every epoch.

A reasonable stopping point

For the fastest path through this book, the route is roughly:

• The intro chapters & Ch 1: framework setup (mandatory context).

• Ch 2–3: MLP and CNN worked examples, the simplest cases of the framework reaching real architectures.

• Skim Ch 4 (BatchNorm). It’s structurally the hardest chapter and the prose says so up front. The math is right (pdiv_bnNormalize’s three-term cancellation is formalized and matches the codegen), but it’s not the place to spend time if you’re not specifically interested in BN. Spend time running as many MNIST and CIFAR demos as possible.

• Read this chapter (Ch 5, ResNet-34). Residual blocks are where the chain rule shows it can carry composition through arbitrarily deep architectures, and the proof reduces to one additive-fan-in lemma you’ve already seen. Run the ResNet-50 RSB-A3 ImageNet training demo (§5-7; about a day on four cards).

• Stop here. Assume Chapters 6–9 (MobileNet, EfficientNet, ConvNeXt, ViT) and the Bestiary (Chapters 10–13) are correct, because they all reuse the same framework with new operators slotting into the same proof tree. Appendix B walks through how that claim is auditable if you ever want to spot-check it.

Reading through Ch 5 is enough to know the framework works. Read the AlphaGo Zero paper (bestiary entry), which combines reinforcement learning with a large residual network of convolutions.

5.6.2 ResNet-50: the 2018 recipe and RSB-A3

The basic block ResNet-34 is built from generalizes to the bottleneck block of ResNet-50 — a \(1\times 1\) down, a \(3\times 3\), a \(1\times 1\) back up — at 25.6M parameters against 21.8M. This section moves one lever at a time. First the architecture, with the recipe held fixed: ResNet-50 on the 2018 recipe of §5-5, unchanged, which is worth \(3.0\) points over ResNet-34 on the reference. Then the recipe, with the architecture held fixed: the same network on RSB-A3 (Wightman et al. 2021, “ResNet Strikes Back”), worth another half point on the reference and a point on the verified path. Both recipes run on both paths, so the result is a grid rather than a pair, and the table that closes the section is the 2018 column every later chapter’s recipe is diffed against.

The reference (JAX)

The reference is jax/MainResnet50Imagenet.lean, the bottleneck backbone on the same tfds stream, with the recipe as an argument. The 2018 row is the ResNet-34 recipe, zero-\(\gamma \) on each bottleneck’s last BatchNorm and the \(0.9\) statistics decay included (A3 keeps both), and BatchNorm’s \(\gamma \), \(\beta \) and the biases undecayed as there. A3 is LAMB at effective batch 2048 (accumulated as \(4\times 512\)), BCE over Mixup/CutMix targets binarized at timm’s \(0.2\) threshold, RandAugment, and train@160 / eval@224. Table 5-5 is both runs.

That fp32 scoring is how the verified path and timm score; the trainers’ own evaluation lands within \(0.04\) of it (through bf16 on 2018, fp32 on A3). A3 normalizes per \(512\)-image micro-batch because it accumulates \(4 \times 512\) to reach \(2048\); the 2018 row is a true global batch of \(256\). That is ghost batch norm (Hoffer, Hubara & Soudry 2017, arXiv:1705.08741): the statistics come from a fixed sub-batch rather than the whole batch, here as a side effect of accumulation rather than a choice, and the A3 render below reproduces it by accumulating the same way. The architecture lever: against ResNet-34’s \(73.98\% \) on the same recipe, the bottleneck is worth \(+3.03\) points. The recipe lever: A3 adds \(+0.57\) on the same network, in less wall clock, because it trains at \(160^2\). It lands \(0.52\) under the paper’s \(78.1\% \) and \(0.47\) under the \(78.05\% \) that timm’s own resnet50.a3_in1k weights score under this protocol, a tenth of a point past one run’s \(\pm 0.37\); the verified render of the same recipe, Table 5-6, lands on the paper’s number. This A3 is timm’s recipe as timm ran it, on both paths; the paragraph after the side-by-side table names the settings a bare transcription would miss, and the one not taken. Figure 5-7 is the two runs, epoch by epoch.

A3 starts far lower — \(0.10\% \) at epoch 1 against \(5.96\% \) — because its whole first epoch runs at timm’s warmup start of \(10^{-4}\), an eightieth of the peak, and BCE over mixup targets gives almost no signal until the logits separate; it trails for nearly the whole schedule, touching the lead at four epochs of the second half. At the matched epoch 90 it leads by \(0.11\) (\(77.11\) against \(77.00\)), and its last ten epochs of anneal add the rest. The schedules are different lengths, so at a shared epoch the two cosines are at different points in their decay; the endpoints are what the \(+0.57\) is measured from.

The verified path (PJRT)

The verified trainer is the ResNet-34 one of §5-5 with the bottleneck backbone substituted, and each recipe is its own render:

• 2018: resnet50in_momdp64wxbf16.

• A3: resnet50in160_lambaccdp4x128wxclipbcebf16, LAMB \(\times \) BCE-with-logits \(\times \) accumulation \(k=4\) at four replicas of \(128\) to the recipe’s \(2048\), train@160 / eval@224.

They run with:

lake run r50-2018-bf16-4gpu
lake run r50-a3-wxclip4x128-bf16-4gpu

Both renders all-reduce every BatchNorm’s mean and variance across the four replicas (Theorem 75), so the 2018 render normalizes over the global \(256\) and the A3 render over \(4 \times 128 = 512\), the ghost batch the reference’s accumulation gives it.

The A3 render carries the recipe as §5-8 tabulates it, including the three places a bare transcription would miss: BN \(\gamma /\beta \) and biases excluded from weight decay, LAMB’s gradient clip at timm’s default (after the all-reduce and the accumulation, at threshold \(kC\), Proofs.clipFactor_accum), and the no_weight_decay group left out of layer adaptation; all three are Theorem 76, and the four-fold accumulation is Theorem 77. The optimizer is also tied to the reference numerically, at the update as well as the gradient, seven variants to \(\sim \! 10^{-7}\). Both paths run \(625\) steps an epoch and leave \(0.08\% \) of it unused, because \(4 \nmid 2{,}502\). One thing differs from the reference: Mixup’s \(\lambda \) is drawn host-side, once per \(512\)-image micro-batch where the reference draws once per accumulated step, so agreement there is distributional rather than per-step.

The two paths, side by side

Table 5-7 is the two paths, row by row.

The BatchNorm statistic group is the setting that changes between the blocks, on both paths at once: the 2018 recipe normalizes over the global \(256\), and A3 over the \(512\)-image micro-batch its accumulation hands each step — ghost batch norm, on the reference and the verified path alike. A3 is timm’s recipe as timm ran it, in the settings a transcription of the paper would miss: the cosine stepped once an epoch, from \(10^{-4}\) over the five warmup epochs to the peak and down to a floor of \(10^{-6}\); Mixup or CutMix drawn per batch at \(p = 0.5\); RandAugment’s fill at the image mean; the BCE targets binarized at \(0.2\) — on both paths (r50-a3-jax-4gpu / r50-a3-wxclip4x128-bf16-4gpu, \(13.4 + 21.9\) h on the 4060 Ti box). Not taken, on either path: timm’s then-default cooldown_epochs 10 at the floor (the paper counts 100 epochs, and \(10^{-6}\) moves nothing).

Both A3 numbers are the final checkpoints rescored at timm’s eval resize, the short side at \(\lfloor 224 / 0.95 \rfloor = 235\) and the long side truncated as torchvision’s Resize does. The trainers scored them at \(236\) with the long side rounded, \(77.61\) / \(78.08\); the move is \(-13\) and \(-14\) images on top-1 and \(+24\) and \(+60\) on top-5, a rounding-sized protocol difference, and the pair keeps its order and its gap under either.

The two paths tie on 2018 and part on A3. On 2018 the gap is \(0.02\) points on top-1 and none on top-5, at one seed per cell (r50-2018-jax-4gpu / r50-2018-bf16-4gpu, \(22.2 + 30.1\) h on the same box, one after the other). Paired on the same images, the two checkpoints disagree on \(4{,}641\), \(2{,}326\) against \(2{,}315\), and McNemar’s exact test puts \(p = 0.88\) on the eleven-image difference: the ResNet-34 reading again. On A3 the verified path lands ahead, by \(0.47\) on top-1 and \(0.31\) on top-5, a tenth of a point past the 95% Wilson interval, \(\pm 0.37\) at \(77\% \) on \(50{,}000\) images. Paired, the A3 checkpoints disagree on \(4{,}017\), \(1{,}891\) against \(2{,}126\), and the \(235\)-image lead is \(p = 0.0002\) (each bitmap is from the same scoring of the final checkpoint as its headline). With one seed per arm a paired lead is a statement about two trained models, not about the two paths — the eight to nine percent of images the two disagree on is what two runs of one recipe produce, whichever is ahead — and whether A3’s lead is the path or the seed needs seeds per arm. The recipe delta keeps its sign on both paths: A3 beats 2018 by \(+0.57\) on the reference and \(+1.06\) on the verified path. A difference that reproduces across two independent implementations is harder to arrange by accident than agreement at one configuration, and it is what a one-row comparison cannot show; the half-point spread in its size is what four single-seed runs leave unresolved. One thing the table does not settle: the A3 column trains at \(160\) and evaluates at \(224\) while 2018 does both at \(224\), so the recipe delta confounds resolution with recipe, by A3’s own design.

The 2018 curves travel together; the A3 curves close most of the way. On 2018 the two paths swing both ways through the schedule, as ResNet-34’s do — the verified path minus the reference averages \(-0.61\), \(+0.17\), \(-0.58\), \(-0.19\) and \(+0.06\) over successive twenty-epoch windows, six points apart at the widest. On A3 the verified path runs one to three points ahead through the middle of the schedule — \(+0.58\), \(+3.06\), \(+1.45\) and \(+1.42\) by the same windows, eleven points at the widest — and the anneal closes most of it, to \(+0.50\) over the last twenty epochs and \(+0.53\) over the last ten, which is the \(0.47\) at the endpoint. Where A3’s route difference lives is not established; the one difference between its columns that 2018’s do not share is where the Mixup/CutMix draw happens, once per \(512\)-image micro-batch on the verified path against once per accumulated step on the reference, and it is untested. It is why these pairs are read at their endpoints and nowhere else (the rows are the runs’ own per-epoch evaluation, the reference’s through its bf16 forward on 2018 and through fp32 on A3; the headline numbers are the final checkpoints scored through fp32, within \(0.04\) of the last column). Table 5-8 is the selected epochs and Figure 5-8 every epoch.

What A3 changes from the 2018 recipe

The 2018-recipe row above is the original paper’s SGD-with-momentum plus the “bag of tricks” polish (cosine schedule, warmup, label smoothing, random-resized-crop). RSB-A3 is the 2021 “ResNet Strikes Back” recipe (Wightman et al.). Both rows are ResNet-50, which is the point: every knob that A3 sets differently is one lever of the three-year jump in how these networks are trained, and holding the architecture fixed is what stops the comparison confounding the recipe with the backbone. The backbone and the entry point are the same for both, and each recipe has its own spec, shim and render. Table 5-9 is the full diff.

What carries over unchanged: cosine LR decay, the 5-epoch warmup, the base augmentation in the row above, zero-\(\gamma \) initialization, bf16 convolution under an fp32 classifier head, and running-BN evaluation. The through-line of the 2018\(\to \)2021 shift is “regularize harder, train bigger”: heavier augmentation (RandAugment + Mixup + CutMix), a loss that accepts soft targets (BCE), an order-of-magnitude more weight decay applied selectively, and a large-batch optimizer (LAMB) to make the longer, noisier training converge, with FixRes buying back the compute the extra epochs would cost. On the reference every one of these is a one-line TrainConfig change; on the verified path each is a render variant or a shim setting on the same backbone, and the \(160\) train resolution is a spec of its own.

5.7 Side quest: the A2 and A1 recipes

A3 is the cheap tier of “ResNet Strikes Back”. The other two — A2 at 300 epochs and A1 at 600, both at \(224^2\) — render on the verified path as a2 and a1 (the reference’s a2-accum and a1), and neither has been run. Table 5-10 is the three tiers.

Under synchronised BatchNorm that is the recipe’s ghost batch of \(512\) per micro-step, as for A3. A1 is its own render rather than A2’s with a flag: the weight decay is baked into the artifact, \(0.01\) against A2’s \(0.02\).

A full schedule. Table 5-11 is four cards, each path’s own trainer timed on real ImageNet at the job’s shape — four replicas of \(128\) accumulated four times to \(2048\), \(625\) optimizer steps an epoch; the rates are the 2026-10-07 re-probe (runs/2026-10-07-d17-reprobe/), after torchvision’s crop and the bicubic RandAugment geometry entered the shims.

Table 5-12 is what the two renders carry, and where they stop short of the paper.

[TODO: timm’s index-level RASampler for the \(3\times \) repeats (both tiers’ code places the three copies adjacent in one optimizer step; A3 has no repeated augmentation, so no landed run carries it); neither tier has run — r50-a2-bf16-4gpu / r50-a1-bf16-4gpu, r50-a2accum-jax-4gpu / r50-a1-jax-4gpu.]

5.8 Recap

The residual block’s backward is a sum: the branch’s VJP plus the identity, or the projection’s where the shapes change. That is additive fan-in, and with the global average pool, the stride-2 convolution and the stem pool it is everything ResNet needs. Theorems 65 and 66 are the full-depth networks at batch statistics, the seals say their backward is not degenerate at the trained width, the steps are tied (Theorems 68 and 70), and the data-parallel twins (Theorem 74) say four cards computing a synchronised step compute one card’s step at four times the batch. This is also the chapter that sets the ImageNet pattern every later chapter repeats: a reference trainer, the verified path, the two side by side at the end, and the recipe measured one ingredient at a time rather than inherited.

What the chapter does not settle is the top of the recipe ladder: A3 ran on both paths and the verified render landed on the paper’s number, while A2 and A1 are rendered and timed, not run. What the network costs is parameters: a standard convolution does spatial mixing and channel mixing in one kernel and pays for both. The next chapter factors them, and the network that results has a ninth of the parameters.