Documentation

LeanMlir.Proofs.Nets.ResNet.ResNet34FullB

ResNet-34 at TRUE BATCH-NORM — the whole net's forward and graph #

ResNet-34's whole-net ℝ forward, its typed forward graph, and the faithfulness tying them, at batch BatchNorm: bnBatchLA (= the proven bnBatchTensor4 at the network's left-assoc index), reduce [0,2,3] — one mu/var per channel across the batch, the one op that couples examples. Every committed ResNet-34 forward and train-step artifact (resnet34_fwd.mlir, resnet34_sgd_train_step.mlir, resnet34in_mom256_train_step.mlir, the Adam/momentum steps) reduces [0,2,3]; the *_fwd_eval artifacts normalise with running statistics.

What is new here, and what is not #

Nothing about the blocks is new. The batched stages (cbReluB, cbReluStridedB, projStridedB in Foundation/Batched/StageLayers.lean, and projB in Foundation/Batched/Stages.lean), their _at VJPs and their backward-graph faithfulness are all at bnBatchLA, and ResNet34BackB0 assembles them into the two block kinds. This file adds the level above: a net-level ℝ forward, a net-level forward graph, and the faithfulness tying them.

Padding is symmetric at every stride-2 site, as ResNet-34's render emits and as the PyTorch-origin convention requires (.convStrided, NOT .convStridedXla — B0's stem is the XLA-SAME one and the two tokens have identical types). scripts/gates/convention_audit.py checks this at the artifact tier and nothing checks it here, so it is stated: stem 7x7/s2, the three downsample conv1s and the three 1x1 projections are all flatConvStride2.

The stem pool is 3x3/s2 (maxPool3s2Flat), not 2x2. Same type, different function, so a swap type-checks.

Precision is a flag on the graph. Every conv site is .convAt bf16 id … / .convStridedAt bf16 id … (StableHLO.PrecisionSwitch, the renderers' own switch), so one builder describes the f32 artifact (bf16 := false) and the bf16 one (bf16 := true, the kinds resnet34in_momdp64bf16 emits); BatchNorm, relu, pool and head carry no flag because no render switches them. The faithfulness theorems hold at either value through Bf16Erasure (Bf16Fold.denOp_convAt_id: the bf16 kind at the identity rounding is its f32 peer), so the typed graph denotes resnet34ForwardBFull whichever precision the text declares. The rounding itself is not modelled here, as it is not at f32: den is over ℝ at both values.

Conventions this net runs at #

depth[3,4,6,3] basic blocks, 64 to 512
BatchNormbatch (bnBatchLA, reduce [0,2,3], width N*h*w)
activationrelu (one kink), TWO per block — the body's mid-relu and the post-residual one
stride-2 paddingsymmetric at all seven sites
stem7x7/s2 conv-bn-relu, then 3x3/s2 max-pool
headGAP then dense, generic in the class count
artifactsresnet34_sgd_train_step, resnet34_adam*, resnet34in_mom*

The head is generic in nCls, so one statement covers the 10-class Imagenette artifacts and the 1000-class resnet34in ones.

N stays a variable throughout: the batch size is never pinned here (the 224-px resolution and the 64…512 widths are literals); it is pinned only where a Maps envelope turns a width into a rational. On the data-parallel artifacts the render's N is the PER-REPLICA batch; their BatchNorm is synchronised, and ResNet34SyncB is this file's twin for them: replica r's forward graph denotes shard r of resnet34ForwardBFull (R * N), this file's forward at the global batch.

References #

source
structure Proofs.R34IdW (c : ℕ) :
Type

Weights of one identity basic block: two 3x3 convs at width c, BatchNorm after each.

Instances For
    source
    structure Proofs.R34DownW (ic oc : ℕ) :
    Type

    Weights of one downsample basic block: strided 3x3 (ic -> oc, halves spatial), 3x3, and the 1x1 stride-2 option-B projection on the skip. BatchNorm after each of the three.

    Instances For
      source
      structure Proofs.R34BWeights (nCls : ℕ) :
      Type

      Every ResNet-34 parameter: stem (7x7/s2, 3->64) + the [3,4,6,3] basic blocks + dense head. Generic in the class count.

      Instances For
        source
        @[reducible]
        noncomputable def Proofs.r34IdB (N h w : ℕ) {c : ℕ} (p : R34IdW c) :
        Vec (N * (c * h * w)) → Vec (N * (c * h * w))

        Batched identity basic block relu(F(x) + x), F = projB . cbReluB. The outer relu after the residual add is ResNet's structural difference from MobileNetV2/EfficientNet, whose residual add IS the block output — and it is why every r34 block carries TWO smoothness clauses.

        Equations
        Instances For
          source
          @[reducible]
          noncomputable def Proofs.r34DownB (N h w : ℕ) {ic oc : ℕ} (p : R34DownW ic oc) :
          Vec (N * (ic * (2 * h) * (2 * w))) → Vec (N * (oc * h * w))

          Batched downsample basic block relu(F_s(x) + proj_s(x)): body strided-conv1 then conv2, skip a 1x1 stride-2 projection. Both stride-2 sites are SYMMETRIC padding.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[reducible]
            noncomputable def Proofs.r34StemB (N h w : ℕ) {ic oc : ℕ} (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (γs βs : Vec oc) :
            Vec (N * (ic * (2 * (2 * h)) * (2 * (2 * w)))) → Vec (N * (oc * h * w))

            Batched stem: 7x7/s2 conv -> bn -> relu, then He et al.'s 3x3/s2 max-pool.

            Equations
            Instances For
              source
              theorem Proofs.r34IdB_apply (N h w : ℕ) {c : ℕ} (p : R34IdW c) (v : Vec (N * (c * h * w))) :
              r34IdB N h w p v = relu (N * (c * h * w)) (residual (projB N p.W₂ p.b₂ p.ε₂ p.γ₂ p.β₂ ∘ StableHLO.cbReluB N p.W₁ p.b₁ p.ε₁ p.γ₁ p.β₁) v)

              The identity block, APPLIED: the outer relu of the residual sum. A proof that needs the relu or the residual exposed rewrites with this instead of restating the goal by show.

              source
              theorem Proofs.r34DownB_apply (N h w : ℕ) {ic oc : ℕ} (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) :
              r34DownB N h w p v = relu (N * (oc * h * w)) (residualProj (StableHLO.projStridedB N p.Wp p.bp p.εp p.γp p.βp) (projB N p.W₂ p.b₂ p.ε₂ p.γ₂ p.β₂ ∘ StableHLO.cbReluStridedB N p.W₁ p.b₁ p.ε₁ p.γ₁ p.β₁) v)

              The downsample block, APPLIED: the outer relu of the projected residual sum.

              source
              theorem Proofs.r34StemB_apply (N h w : ℕ) {ic oc : ℕ} (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (γs βs : Vec oc) (x : Vec (N * (ic * (2 * (2 * h)) * (2 * (2 * w))))) :
              r34StemB N h w Ws bs εs γs βs x = StableHLO.batchMap N (maxPool3s2Flat oc h w) (StableHLO.cbReluStridedB N Ws bs εs γs βs x)

              The stem, APPLIED: the pool of the strided conv-BN-relu.

              source
              @[reducible]
              noncomputable def Proofs.r34HeadB (N h w : ℕ) {c nCls : ℕ} (Wd : Mat c nCls) (bd : Vec nCls) :
              Vec (N * (c * h * w)) → Vec (N * nCls)

              Batched head: global average pool, then the dense classifier.

              Equations
              Instances For
                source
                theorem Proofs.r34HeadB_apply (N h w : ℕ) {c nCls : ℕ} (Wd : Mat c nCls) (bd : Vec nCls) (v : Vec (N * (c * h * w))) :
                r34HeadB N h w Wd bd v = StableHLO.batchMap N (dense Wd bd) (StableHLO.batchMap N (globalAvgPoolFlat c h w) v)

                ResNet-34's GAP-and-dense tail, APPLIED.

                source
                noncomputable def Proofs.resnet34ForwardBFull (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) :
                Vec (N * nCls)

                The full batch-BN ResNet-34 forward, N*(3*224*224) -> N*nCls. Nested-application form, as efficientnetForwardBFull and mobilenetv2ForwardBFull both are, so a whole-net proof can peel it one block at a time.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Proofs.StableHLO.r34IdGraphB (p epsStr : String) (N h w : ℕ) {c : ℕ} (pw : R34IdW c) (bf16 : Bool) (e : SHlo (N * (c * h * w))) :
                  SHlo (N * (c * h * w))

                  Identity basic-block graph: relu(addV(bn(conv(relu(bn(conv e)))), e)). The skip reuses the block-input subtree e in both addV operands, as the render does.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Proofs.StableHLO.r34IdGraphB_faithful (p epsStr : String) (N h w : ℕ) {c : ℕ} (pw : R34IdW c) (bf16 : Bool) (e : SHlo (N * (c * h * w))) :
                    den (r34IdGraphB p epsStr N h w pw bf16 e) = r34IdB N h w pw (den e)
                    source
                    def Proofs.StableHLO.r34DownGraphB (p epsStr : String) (N h w : ℕ) {ic oc : ℕ} (pw : R34DownW ic oc) (bf16 : Bool) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) :
                    SHlo (N * (oc * h * w))

                    Downsample basic-block graph: relu(addVB(body, projection)) — body first, the order the render emits (so pretty of this graph is the rendered block's text); residualProj proj body adds them the other way round, which the faithfulness proof absorbs with add_comm. Both branches read the block-input subtree e; both stride-2 convs are .convStrided (symmetric padding).

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem Proofs.StableHLO.r34DownGraphB_faithful (p epsStr : String) (N h w : ℕ) {ic oc : ℕ} (pw : R34DownW ic oc) (bf16 : Bool) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) :
                      den (r34DownGraphB p epsStr N h w pw bf16 e) = r34DownB N h w pw (den e)
                      source
                      def Proofs.StableHLO.r34StemGraphB (epsStr : String) (N h w : ℕ) {ic oc : ℕ} (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (γs βs : Vec oc) (bf16 : Bool) (e : SHlo (N * (ic * (2 * (2 * h)) * (2 * (2 * w))))) :
                      SHlo (N * (oc * h * w))

                      Stem graph: 7x7/s2 conv -> bn -> relu -> 3x3/s2 max-pool.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem Proofs.StableHLO.r34StemGraphB_faithful (epsStr : String) (N h w : ℕ) {ic oc : ℕ} (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (γs βs : Vec oc) (bf16 : Bool) (e : SHlo (N * (ic * (2 * (2 * h)) * (2 * (2 * w))))) :
                        den (r34StemGraphB epsStr N h w Ws bs εs γs βs bf16 e) = r34StemB N h w Ws bs εs γs βs (den e)
                        source
                        def Proofs.StableHLO.r34HeadGraphB (N h w : ℕ) {c nCls : ℕ} (Wd : Mat c nCls) (bd : Vec nCls) (e : SHlo (N * (c * h * w))) :
                        SHlo (N * nCls)

                        Head graph: GAP then dense.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem Proofs.StableHLO.r34HeadGraphB_faithful (N h w : ℕ) {c nCls : ℕ} (Wd : Mat c nCls) (bd : Vec nCls) (e : SHlo (N * (c * h * w))) :
                          den (r34HeadGraphB N h w Wd bd e) = r34HeadB N h w Wd bd (den e)
                          source
                          def Proofs.StableHLO.resnet34FwdGraphBFull (N : ℕ) (epsStr : String) {nCls : ℕ} (w : R34BWeights nCls) (bf16 : Bool) (e : SHlo (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) :
                          SHlo (N * nCls)

                          The full batch-BN ResNet-34 forward graph. Block prefixes are the render's (s1b0/d2/s2b0/... ), so the typed graph diffs against resnet34_fwd's batched peers name for name. bf16 selects the conv kinds at every site (.convAt / .convStridedAt).

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem Proofs.StableHLO.resnet34FwdGraphBFull_faithful (N : ℕ) (epsStr : String) {nCls : ℕ} (w : R34BWeights nCls) (bf16 : Bool) (e : SHlo (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) :
                            den (resnet34FwdGraphBFull N epsStr w bf16 e) = resnet34ForwardBFull N w (den e)

                            Forward-graph faithfulness for ResNet-34 at batch BN: the typed graph denotes the whole-net forward, at either precision — bf16 := false is the f32 artifacts' graph, bf16 := true the bf16 ones' (resnet34in_momdp64bf16's kinds), and the right-hand side is the same resnet34ForwardBFull.