ResNet-34 — every parameter gradient node IS the loss's derivative in that parameter #

r34_net_tiedB says each of the 146 parameter gradient nodes denotes its layer's parameter Jacobian contracted with the cotangent the emitted backward chain threads to it; the *CotIn_eq_vjp lemmas say the block-input cotangents are certified VJP backwards; and r34_lossCot_is_smoothedCE_grad identifies the loss cotangent row by row. r34_net_lossGrad composes them: at the same cotangents, every node is ∂L/∂θ of the WHOLE net with that one parameter varied, L the batched label-smoothed cross-entropy (smoothedBatchLoss) the trainer minimises.

How. Three layers, each generic where it can be:

Per node kind (ParamGradNodes): a node is ∂G/∂θ whenever its cotangent is the gradient of G — the loss read at that op's output — there (HasGradAt).
Per block kind (this file, at variable widths): the loss read at each internal activation of an identity / downsample block, the stem and the head (r34IdG*, r34DownG*, r34StemG*), with its gradient the chain's own cotangent (r34IdGC1_hasGradAt, …), pulled back one certified stage at a time (HasGradAt.comp). The bundles r34IdLossTiedB / r34DownLossTiedB / r34StemLossTiedB / r34HeadLossTiedB state all of a block's nodes against Φ, the loss as a function of that block's weight record.
Per net: the loss read after each block (r34Suf*), its gradient pulled back through the sixteen certified block VJPs (r34IdB_hasGradAt_comp, r34DownB_hasGradAt_comp), and Φ identified with the whole net at updated weights (r34_factor_*) — each a standalone rfl; inside the capstone the same identity is a kernel deep recursion at the literal widths.

Hypotheses. R34PosB (every BN ε > 0), R34SmoothAtB (every relu off its kink and the stem pool tie-free at the real activations), every example's target summing to one, 0 < nCls.

source

noncomputable def Proofs.ResNet34TieB.r34IdGA (N h w : ℕ) {c : ℕ} (Gn : Vec (N * (c * h * w)) → Vec 1) :

Vec (N * (c * h * w)) → Vec 1

The loss at the outer relu's input a.

Equations

Proofs.ResNet34TieB.r34IdGA N h w Gn u = Gn (Proofs.relu (N * (c * h * w)) u)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34IdGN2 (N h w : ℕ) {c : ℕ} (Gn : Vec (N * (c * h * w)) → Vec 1) (v : Vec (N * (c * h * w))) :

Vec (N * (c * h * w)) → Vec 1

The loss at bn₂'s output (the skip v held fixed).

Equations

Proofs.ResNet34TieB.r34IdGN2 N h w Gn v u = Proofs.ResNet34TieB.r34IdGA N h w Gn fun (i : Fin (N * (c * h * w))) => u i + v i

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34IdGC2 (N h w : ℕ) {c : ℕ} (Gn : Vec (N * (c * h * w)) → Vec 1) (p : R34IdW c) (v : Vec (N * (c * h * w))) :

Vec (N * (c * h * w)) → Vec 1

The loss at conv₂'s output.

Equations

Proofs.ResNet34TieB.r34IdGC2 N h w Gn p v z = Proofs.ResNet34TieB.r34IdGN2 N h w Gn v (Proofs.StableHLO.bnBatchLA N c h w p.ε₂ p.γ₂ p.β₂ z)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34IdGN1 (N h w : ℕ) {c : ℕ} (Gn : Vec (N * (c * h * w)) → Vec 1) (p : R34IdW c) (v : Vec (N * (c * h * w))) :

Vec (N * (c * h * w)) → Vec 1

The loss at bn₁'s output.

Equations

Proofs.ResNet34TieB.r34IdGN1 N h w Gn p v u = Proofs.ResNet34TieB.r34IdGC2 N h w Gn p v (Proofs.StableHLO.batchMap N (Proofs.flatConv p.W₂ p.b₂) (Proofs.relu (N * (c * h * w)) u))

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34IdGC1 (N h w : ℕ) {c : ℕ} (Gn : Vec (N * (c * h * w)) → Vec 1) (p : R34IdW c) (v : Vec (N * (c * h * w))) :

Vec (N * (c * h * w)) → Vec 1

The loss at conv₁'s output.

Equations

Proofs.ResNet34TieB.r34IdGC1 N h w Gn p v z = Proofs.ResNet34TieB.r34IdGN1 N h w Gn p v (Proofs.StableHLO.bnBatchLA N c h w p.ε₁ p.γ₁ p.β₁ z)

Instances For

source

theorem Proofs.ResNet34TieB.r34IdGA_hasGradAt {N h w c : ℕ} (p : R34IdW c) (v : Vec (N * (c * h * w))) (hs : R34IdSmoothAt N h w p v) {Gn : Vec (N * (c * h * w)) → Vec 1} {dy : Vec (N * (c * h * w))} (hGn : HasGradAt Gn (r34IdB N h w p v) dy) :

HasGradAt (r34IdGA N h w Gn) (residual (projB N p.W₂ p.b₂ p.ε₂ p.γ₂ p.β₂ ∘ StableHLO.cbReluB N p.W₁ p.b₁ p.ε₁ p.γ₁ p.β₁) v) (r34IdCotA N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34IdGN2_hasGradAt {N h w c : ℕ} (p : R34IdW c) (v : Vec (N * (c * h * w))) (hs : R34IdSmoothAt N h w p v) {Gn : Vec (N * (c * h * w)) → Vec 1} {dy : Vec (N * (c * h * w))} (hGn : HasGradAt Gn (r34IdB N h w p v) dy) :

HasGradAt (r34IdGN2 N h w Gn v) (StableHLO.bnBatchLA N c h w p.ε₂ p.γ₂ p.β₂ (StableHLO.batchMap N (flatConv p.W₂ p.b₂) (StableHLO.cbReluB N p.W₁ p.b₁ p.ε₁ p.γ₁ p.β₁ v))) (r34IdCotA N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34IdGC2_hasGradAt {N h w c : ℕ} (p : R34IdW c) (hq : R34IdPos p) (v : Vec (N * (c * h * w))) (hs : R34IdSmoothAt N h w p v) {Gn : Vec (N * (c * h * w)) → Vec 1} {dy : Vec (N * (c * h * w))} (hGn : HasGradAt Gn (r34IdB N h w p v) dy) :

HasGradAt (r34IdGC2 N h w Gn p v) (StableHLO.batchMap N (flatConv p.W₂ p.b₂) (StableHLO.cbReluB N p.W₁ p.b₁ p.ε₁ p.γ₁ p.β₁ v)) (r34IdCotC2 N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34IdGN1_hasGradAt {N h w c : ℕ} (p : R34IdW c) (hq : R34IdPos p) (v : Vec (N * (c * h * w))) (hs : R34IdSmoothAt N h w p v) {Gn : Vec (N * (c * h * w)) → Vec 1} {dy : Vec (N * (c * h * w))} (hGn : HasGradAt Gn (r34IdB N h w p v) dy) :

HasGradAt (r34IdGN1 N h w Gn p v) (StableHLO.bnBatchLA N c h w p.ε₁ p.γ₁ p.β₁ (StableHLO.batchMap N (flatConv p.W₁ p.b₁) v)) (r34IdCotN1 N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34IdGC1_hasGradAt {N h w c : ℕ} (p : R34IdW c) (hq : R34IdPos p) (v : Vec (N * (c * h * w))) (hs : R34IdSmoothAt N h w p v) {Gn : Vec (N * (c * h * w)) → Vec 1} {dy : Vec (N * (c * h * w))} (hGn : HasGradAt Gn (r34IdB N h w p v) dy) :

HasGradAt (r34IdGC1 N h w Gn p v) (StableHLO.batchMap N (flatConv p.W₁ p.b₁) v) (r34IdCotC1 N h w p v dy)

source

def Proofs.ResNet34TieB.r34IdLossTiedB {N h w c : ℕ} (xN cotN vN epsStr : String) (p : R34IdW c) (v : Vec (N * (c * h * w))) (Φ : R34IdW c → Vec 1) (dy : Vec (N * (c * h * w))) :

Prop

Identity block, every parameter node a loss derivative. With Gn the loss read at the block's output and Φ the loss as a function of the block's weight record (hΦ), each of the eight nodes r34IdTiedB ties — at the same cotangents — is ∂Φ/∂slot with that one slot varied.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Proofs.ResNet34TieB.r34_idblock_lossTiedB {N h w c : ℕ} (xN cotN vN epsStr : String) (p : R34IdW c) (hq : R34IdPos p) (v : Vec (N * (c * h * w))) (hs : R34IdSmoothAt N h w p v) {Gn : Vec (N * (c * h * w)) → Vec 1} {dy : Vec (N * (c * h * w))} (hGn : HasGradAt Gn (r34IdB N h w p v) dy) {Φ : R34IdW c → Vec 1} (hΦ : ∀ (p' : R34IdW c), Φ p' = Gn (r34IdB N h w p' v)) :

r34IdLossTiedB xN cotN vN epsStr p v Φ dy

source

noncomputable def Proofs.ResNet34TieB.r34DownGA (N h w : ℕ) {oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) :

Vec (N * (oc * h * w)) → Vec 1

The loss at the downsample block's pre-relu sum.

Equations

Proofs.ResNet34TieB.r34DownGA N h w Gn u = Gn (Proofs.relu (N * (oc * h * w)) u)

Instances For

source

@[reducible]

noncomputable def Proofs.ResNet34TieB.r34DownProjOut (N h w : ℕ) {ic oc : ℕ} (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (oc * h * w))

The projection branch's output, bnₚ(convₚ v).

Equations

Proofs.ResNet34TieB.r34DownProjOut N h w p v = Proofs.StableHLO.projStridedB N p.Wp p.bp p.εp p.γp p.βp v

Instances For

source

@[reducible]

noncomputable def Proofs.ResNet34TieB.r34DownBodyOut (N h w : ℕ) {ic oc : ℕ} (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (oc * h * w))

The body branch's output, bn₂(conv₂(relu(bn₁(conv₁ v)))).

Equations

Proofs.ResNet34TieB.r34DownBodyOut N h w p v = Proofs.projB N p.W₂ p.b₂ p.ε₂ p.γ₂ p.β₂ (Proofs.StableHLO.cbReluStridedB N p.W₁ p.b₁ p.ε₁ p.γ₁ p.β₁ v)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34DownGN2 (N h w : ℕ) {ic oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (oc * h * w)) → Vec 1

The loss at bn₂'s output (projection branch fixed, on the left).

Equations

Proofs.ResNet34TieB.r34DownGN2 N h w Gn p v u = Proofs.ResNet34TieB.r34DownGA N h w Gn fun (i : Fin (N * (oc * h * w))) => Proofs.ResNet34TieB.r34DownProjOut N h w p v i + u i

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34DownGC2 (N h w : ℕ) {ic oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (oc * h * w)) → Vec 1

Equations

Proofs.ResNet34TieB.r34DownGC2 N h w Gn p v z = Proofs.ResNet34TieB.r34DownGN2 N h w Gn p v (Proofs.StableHLO.bnBatchLA N oc h w p.ε₂ p.γ₂ p.β₂ z)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34DownGN1 (N h w : ℕ) {ic oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (oc * h * w)) → Vec 1

Equations

Proofs.ResNet34TieB.r34DownGN1 N h w Gn p v u = Proofs.ResNet34TieB.r34DownGC2 N h w Gn p v (Proofs.StableHLO.batchMap N (Proofs.flatConv p.W₂ p.b₂) (Proofs.relu (N * (oc * h * w)) u))

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34DownGC1 (N h w : ℕ) {ic oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (oc * h * w)) → Vec 1

Equations

Proofs.ResNet34TieB.r34DownGC1 N h w Gn p v z = Proofs.ResNet34TieB.r34DownGN1 N h w Gn p v (Proofs.StableHLO.bnBatchLA N oc h w p.ε₁ p.γ₁ p.β₁ z)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34DownGNp (N h w : ℕ) {ic oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (oc * h * w)) → Vec 1

The loss at bnₚ's output (body branch fixed, on the right).

Equations

Proofs.ResNet34TieB.r34DownGNp N h w Gn p v u = Proofs.ResNet34TieB.r34DownGA N h w Gn fun (i : Fin (N * (oc * h * w))) => u i + Proofs.ResNet34TieB.r34DownBodyOut N h w p v i

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34DownGCp (N h w : ℕ) {ic oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) :

Vec (N * (oc * h * w)) → Vec 1

Equations

Proofs.ResNet34TieB.r34DownGCp N h w Gn p v z = Proofs.ResNet34TieB.r34DownGNp N h w Gn p v (Proofs.StableHLO.bnBatchLA N oc h w p.εp p.γp p.βp z)

Instances For

source

theorem Proofs.ResNet34TieB.r34DownGA_hasGradAt {N h w ic oc : ℕ} (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : R34DownSmoothAt N h w p v) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34DownB N h w p v) dy) :

HasGradAt (r34DownGA N h w Gn) (r34DownPre N h w p v) (r34DownCotA N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34DownGN2_hasGradAt {N h w ic oc : ℕ} (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : R34DownSmoothAt N h w p v) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34DownB N h w p v) dy) :

HasGradAt (r34DownGN2 N h w Gn p v) (r34DownBodyOut N h w p v) (r34DownCotA N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34DownGNp_hasGradAt {N h w ic oc : ℕ} (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : R34DownSmoothAt N h w p v) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34DownB N h w p v) dy) :

HasGradAt (r34DownGNp N h w Gn p v) (r34DownProjOut N h w p v) (r34DownCotA N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34DownGC2_hasGradAt {N h w ic oc : ℕ} (p : R34DownW ic oc) (hq : R34DownPos p) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : R34DownSmoothAt N h w p v) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34DownB N h w p v) dy) :

HasGradAt (r34DownGC2 N h w Gn p v) (StableHLO.batchMap N (flatConv p.W₂ p.b₂) (StableHLO.cbReluStridedB N p.W₁ p.b₁ p.ε₁ p.γ₁ p.β₁ v)) (r34DownCotC2 N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34DownGN1_hasGradAt {N h w ic oc : ℕ} (p : R34DownW ic oc) (hq : R34DownPos p) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : R34DownSmoothAt N h w p v) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34DownB N h w p v) dy) :

HasGradAt (r34DownGN1 N h w Gn p v) (StableHLO.bnBatchLA N oc h w p.ε₁ p.γ₁ p.β₁ (StableHLO.batchMap N (flatConvStride2 p.W₁ p.b₁) v)) (r34DownCotN1 N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34DownGC1_hasGradAt {N h w ic oc : ℕ} (p : R34DownW ic oc) (hq : R34DownPos p) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : R34DownSmoothAt N h w p v) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34DownB N h w p v) dy) :

HasGradAt (r34DownGC1 N h w Gn p v) (StableHLO.batchMap N (flatConvStride2 p.W₁ p.b₁) v) (r34DownCotC1 N h w p v dy)

source

theorem Proofs.ResNet34TieB.r34DownGCp_hasGradAt {N h w ic oc : ℕ} (p : R34DownW ic oc) (hq : R34DownPos p) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : R34DownSmoothAt N h w p v) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34DownB N h w p v) dy) :

HasGradAt (r34DownGCp N h w Gn p v) (StableHLO.batchMap N (flatConvStride2 p.Wp p.bp) v) (r34DownCotCp N h w p v dy)

source

def Proofs.ResNet34TieB.r34DownLossTiedB {N h w ic oc : ℕ} (xN cotN vN epsStr : String) (p : R34DownW ic oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (Φ : R34DownW ic oc → Vec 1) (dy : Vec (N * (oc * h * w))) :

Prop

Downsample block, every parameter node a loss derivative — the twelve nodes r34DownTiedB ties.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Proofs.ResNet34TieB.r34_downblock_lossTiedB {N h w ic oc : ℕ} (xN cotN vN epsStr : String) (p : R34DownW ic oc) (hq : R34DownPos p) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : R34DownSmoothAt N h w p v) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34DownB N h w p v) dy) {Φ : R34DownW ic oc → Vec 1} (hΦ : ∀ (p' : R34DownW ic oc), Φ p' = Gn (r34DownB N h w p' v)) :

r34DownLossTiedB xN cotN vN epsStr p v Φ dy

source

noncomputable def Proofs.ResNet34TieB.r34StemGP (N h w : ℕ) {oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) :

Vec (N * (oc * (2 * h) * (2 * w))) → Vec 1

The loss at the stem relu's output (the pool's input).

Equations

Proofs.ResNet34TieB.r34StemGP N h w Gn u = Gn (Proofs.StableHLO.batchMap N (Proofs.maxPool3s2Flat oc h w) u)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34StemGN (N h w : ℕ) {oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) :

Vec (N * (oc * (2 * h) * (2 * w))) → Vec 1

The loss at the stem BN's output.

Equations

Proofs.ResNet34TieB.r34StemGN N h w Gn u = Proofs.ResNet34TieB.r34StemGP N h w Gn (Proofs.relu (N * (oc * (2 * h) * (2 * w))) u)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34StemGC (N h w : ℕ) {oc : ℕ} (Gn : Vec (N * (oc * h * w)) → Vec 1) (εs : ℝ) (γs βs : Vec oc) :

Vec (N * (oc * (2 * h) * (2 * w))) → Vec 1

The loss at the stem conv's output.

Equations

Proofs.ResNet34TieB.r34StemGC N h w Gn εs γs βs z = Proofs.ResNet34TieB.r34StemGN N h w Gn (Proofs.StableHLO.bnBatchLA N oc (2 * h) (2 * w) εs γs βs z)

Instances For

source

theorem Proofs.ResNet34TieB.r34StemGC_hasGradAt {N h w ic oc : ℕ} (hc : 0 < oc) (hh : 0 < h) (hw : 0 < w) (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (hεs : 0 < εs) (γs βs : Vec oc) (x : Vec (N * (ic * (2 * (2 * h)) * (2 * (2 * w))))) (hstem : R34StemSmoothAt N h w Ws bs εs γs βs x) (hpool : StemPoolSmoothAt N h w (StableHLO.cbReluStridedB N Ws bs εs γs βs x)) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34StemB N h w Ws bs εs γs βs x) dy) :

HasGradAt (r34StemGN N h w Gn) (StableHLO.bnBatchLA N oc (2 * h) (2 * w) εs γs βs (StableHLO.batchMap N (flatConvStride2 Ws bs) x)) (r34StemCotN N h w Ws bs εs γs βs x dy) ∧ HasGradAt (r34StemGC N h w Gn εs γs βs) (StableHLO.batchMap N (flatConvStride2 Ws bs) x) (r34StemCotC N h w Ws bs εs γs βs x dy)

source

def Proofs.ResNet34TieB.r34StemLossTiedB {N h w ic oc : ℕ} (xN cotN vN epsStr : String) (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (γs βs : Vec oc) (x : Vec (N * (ic * (2 * (2 * h)) * (2 * (2 * w))))) (Φ : Kernel4 oc ic 7 7 → Vec oc → Vec oc → Vec oc → Vec 1) (dy : Vec (N * (oc * h * w))) :

Prop

Stem, every parameter node a loss derivative — the four nodes r34StemTiedB ties, Φ the loss as a function of the stem's (W, b, γ, β).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Proofs.ResNet34TieB.r34_stem_lossTiedB {N h w ic oc : ℕ} (hc : 0 < oc) (hh : 0 < h) (hw : 0 < w) (xN cotN vN epsStr : String) (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (hεs : 0 < εs) (γs βs : Vec oc) (x : Vec (N * (ic * (2 * (2 * h)) * (2 * (2 * w))))) (hstem : R34StemSmoothAt N h w Ws bs εs γs βs x) (hpool : StemPoolSmoothAt N h w (StableHLO.cbReluStridedB N Ws bs εs γs βs x)) {Gn : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hGn : HasGradAt Gn (r34StemB N h w Ws bs εs γs βs x) dy) {Φ : Kernel4 oc ic 7 7 → Vec oc → Vec oc → Vec oc → Vec 1} (hΦ : ∀ (W : Kernel4 oc ic 7 7) (b γ β : Vec oc), Φ W b γ β = Gn (r34StemB N h w W b εs γ β x)) :

r34StemLossTiedB xN cotN vN epsStr Ws bs εs γs βs x Φ dy

source

def Proofs.ResNet34TieB.r34HeadLossTiedB {N h w c nCls : ℕ} (xN cotN : String) (Wd : Mat c nCls) (bd : Vec nCls) (v : Vec (N * (c * h * w))) (Φ : Mat c nCls → Vec nCls → Vec 1) (g : Vec (N * nCls)) :

Prop

Head, both parameter nodes loss derivatives — the classifier weight and bias nodes r34HeadTiedB ties, Φ the loss as a function of (Wd, bd).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Proofs.ResNet34TieB.r34_head_lossTiedB {N h w c nCls : ℕ} (xN cotN : String) (Wd : Mat c nCls) (bd : Vec nCls) (v : Vec (N * (c * h * w))) {L : Vec (N * nCls) → Vec 1} {g : Vec (N * nCls)} (hL : HasGradAt L (r34HeadB N h w Wd bd v) g) {Φ : Mat c nCls → Vec nCls → Vec 1} (hΦ : ∀ (W : Mat c nCls) (b : Vec nCls), Φ W b = L (r34HeadB N h w W b v)) :

r34HeadLossTiedB xN cotN Wd bd v Φ g

source

noncomputable def Proofs.ResNet34TieB.r34SufE1 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (512 * 7 * 7)) → Vec (N * nCls)

The net after block e1 — the head.

Equations

Proofs.ResNet34TieB.r34SufE1 N w = Proofs.r34HeadB N 7 7 w.Wd w.bd

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufE0 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (512 * 7 * 7)) → Vec (N * nCls)

The net after block e0: block e1, then the rest.

Equations

Proofs.ResNet34TieB.r34SufE0 N w y = Proofs.ResNet34TieB.r34SufE1 N w (Proofs.r34IdB N 7 7 w.e1 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufD4 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (512 * 7 * 7)) → Vec (N * nCls)

The net after block d4: block e0, then the rest.

Equations

Proofs.ResNet34TieB.r34SufD4 N w y = Proofs.ResNet34TieB.r34SufE0 N w (Proofs.r34IdB N 7 7 w.e0 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufC4 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (256 * 14 * 14)) → Vec (N * nCls)

The net after block c4: block d4, then the rest.

Equations

Proofs.ResNet34TieB.r34SufC4 N w y = Proofs.ResNet34TieB.r34SufD4 N w (Proofs.r34DownB N 7 7 w.d4 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufC3 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (256 * 14 * 14)) → Vec (N * nCls)

The net after block c3: block c4, then the rest.

Equations

Proofs.ResNet34TieB.r34SufC3 N w y = Proofs.ResNet34TieB.r34SufC4 N w (Proofs.r34IdB N 14 14 w.c4 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufC2 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (256 * 14 * 14)) → Vec (N * nCls)

The net after block c2: block c3, then the rest.

Equations

Proofs.ResNet34TieB.r34SufC2 N w y = Proofs.ResNet34TieB.r34SufC3 N w (Proofs.r34IdB N 14 14 w.c3 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufC1 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (256 * 14 * 14)) → Vec (N * nCls)

The net after block c1: block c2, then the rest.

Equations

Proofs.ResNet34TieB.r34SufC1 N w y = Proofs.ResNet34TieB.r34SufC2 N w (Proofs.r34IdB N 14 14 w.c2 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufC0 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (256 * 14 * 14)) → Vec (N * nCls)

The net after block c0: block c1, then the rest.

Equations

Proofs.ResNet34TieB.r34SufC0 N w y = Proofs.ResNet34TieB.r34SufC1 N w (Proofs.r34IdB N 14 14 w.c1 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufD3 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (256 * 14 * 14)) → Vec (N * nCls)

The net after block d3: block c0, then the rest.

Equations

Proofs.ResNet34TieB.r34SufD3 N w y = Proofs.ResNet34TieB.r34SufC0 N w (Proofs.r34IdB N 14 14 w.c0 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufB2 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (128 * 28 * 28)) → Vec (N * nCls)

The net after block b2: block d3, then the rest.

Equations

Proofs.ResNet34TieB.r34SufB2 N w y = Proofs.ResNet34TieB.r34SufD3 N w (Proofs.r34DownB N 14 14 w.d3 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufB1 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (128 * 28 * 28)) → Vec (N * nCls)

The net after block b1: block b2, then the rest.

Equations

Proofs.ResNet34TieB.r34SufB1 N w y = Proofs.ResNet34TieB.r34SufB2 N w (Proofs.r34IdB N 28 28 w.b2 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufB0 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (128 * 28 * 28)) → Vec (N * nCls)

The net after block b0: block b1, then the rest.

Equations

Proofs.ResNet34TieB.r34SufB0 N w y = Proofs.ResNet34TieB.r34SufB1 N w (Proofs.r34IdB N 28 28 w.b1 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufD2 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (128 * 28 * 28)) → Vec (N * nCls)

The net after block d2: block b0, then the rest.

Equations

Proofs.ResNet34TieB.r34SufD2 N w y = Proofs.ResNet34TieB.r34SufB0 N w (Proofs.r34IdB N 28 28 w.b0 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufA2 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (64 * 56 * 56)) → Vec (N * nCls)

The net after block a2: block d2, then the rest.

Equations

Proofs.ResNet34TieB.r34SufA2 N w y = Proofs.ResNet34TieB.r34SufD2 N w (Proofs.r34DownB N 28 28 w.d2 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufA1 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (64 * 56 * 56)) → Vec (N * nCls)

The net after block a1: block a2, then the rest.

Equations

Proofs.ResNet34TieB.r34SufA1 N w y = Proofs.ResNet34TieB.r34SufA2 N w (Proofs.r34IdB N 56 56 w.a2 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufA0 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (64 * 56 * 56)) → Vec (N * nCls)

The net after block a0: block a1, then the rest.

Equations

Proofs.ResNet34TieB.r34SufA0 N w y = Proofs.ResNet34TieB.r34SufA1 N w (Proofs.r34IdB N 56 56 w.a1 y)

Instances For

source

noncomputable def Proofs.ResNet34TieB.r34SufStem (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) :

Vec (N * (64 * 56 * 56)) → Vec (N * nCls)

The net after the stem: block a0, then the rest.

Equations

Proofs.ResNet34TieB.r34SufStem N w y = Proofs.ResNet34TieB.r34SufA0 N w (Proofs.r34IdB N 56 56 w.a0 y)

Instances For

source

theorem Proofs.ResNet34TieB.r34_factor_stem (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (W : Kernel4 64 3 7 7) (b γ β : Vec 64) :

resnet34ForwardBFull N { sW := W, sb := b, sε := w.sε, sγ := γ, sβ := β, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufStem N w (r34StemB N 56 56 W b w.sε γ β x)

The net with the stem's parameters varied is the suffix after the stem at the varied stem.

source

theorem Proofs.ResNet34TieB.r34_factor_a0 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 64) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := p, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufA0 N w (r34IdB N 56 56 p (r34Pre0 N w x))

The net with block a0's weights varied is the suffix after a0 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_a1 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 64) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := p, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufA1 N w (r34IdB N 56 56 p (r34Pre1 N w x))

The net with block a1's weights varied is the suffix after a1 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_a2 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 64) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := p, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufA2 N w (r34IdB N 56 56 p (r34Pre2 N w x))

The net with block a2's weights varied is the suffix after a2 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_d2 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34DownW 64 128) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := p, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufD2 N w (r34DownB N 28 28 p (r34Pre3 N w x))

The net with block d2's weights varied is the suffix after d2 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_b0 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 128) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := p, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufB0 N w (r34IdB N 28 28 p (r34Pre4 N w x))

The net with block b0's weights varied is the suffix after b0 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_b1 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 128) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := p, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufB1 N w (r34IdB N 28 28 p (r34Pre5 N w x))

The net with block b1's weights varied is the suffix after b1 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_b2 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 128) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := p, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufB2 N w (r34IdB N 28 28 p (r34Pre6 N w x))

The net with block b2's weights varied is the suffix after b2 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_d3 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34DownW 128 256) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := p, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufD3 N w (r34DownB N 14 14 p (r34Pre7 N w x))

The net with block d3's weights varied is the suffix after d3 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_c0 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 256) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := p, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufC0 N w (r34IdB N 14 14 p (r34Pre8 N w x))

The net with block c0's weights varied is the suffix after c0 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_c1 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 256) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := p, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufC1 N w (r34IdB N 14 14 p (r34Pre9 N w x))

The net with block c1's weights varied is the suffix after c1 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_c2 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 256) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := p, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufC2 N w (r34IdB N 14 14 p (r34Pre10 N w x))

The net with block c2's weights varied is the suffix after c2 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_c3 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 256) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := p, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufC3 N w (r34IdB N 14 14 p (r34Pre11 N w x))

The net with block c3's weights varied is the suffix after c3 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_c4 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 256) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := p, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufC4 N w (r34IdB N 14 14 p (r34Pre12 N w x))

The net with block c4's weights varied is the suffix after c4 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_d4 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34DownW 256 512) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := p, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufD4 N w (r34DownB N 7 7 p (r34Pre13 N w x))

The net with block d4's weights varied is the suffix after d4 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_e0 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 512) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := p, e1 := w.e1, Wd := w.Wd, bd := w.bd } x = r34SufE0 N w (r34IdB N 7 7 p (r34Pre14 N w x))

The net with block e0's weights varied is the suffix after e0 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_e1 (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (p : R34IdW 512) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := p, Wd := w.Wd, bd := w.bd } x = r34SufE1 N w (r34IdB N 7 7 p (r34Pre15 N w x))

The net with block e1's weights varied is the suffix after e1 at the varied block.

source

theorem Proofs.ResNet34TieB.r34_factor_head (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (W : Mat 512 nCls) (b : Vec nCls) :

resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := W, bd := b } x = r34HeadB N 7 7 W b (r34Pre16 N w x)

The net with the classifier varied is the head at the varied classifier.

source

theorem Proofs.ResNet34TieB.r34IdB_hasGradAt_comp {N h w c : ℕ} (p : R34IdW c) (hq : R34IdPos p) (v : Vec (N * (c * h * w))) (hs : R34IdSmoothAt N h w p v) {G : Vec (N * (c * h * w)) → Vec 1} {dy : Vec (N * (c * h * w))} (hG : HasGradAt G (r34IdB N h w p v) dy) :

HasGradAt (fun (y : Vec (N * (c * h * w))) => G (r34IdB N h w p y)) v (r34IdCotIn N h w p v dy)

Pull the loss gradient back through an identity block: the certified block VJP, read at the chain's own fan-in (r34IdCotIn_eq_vjp).

source

theorem Proofs.ResNet34TieB.r34DownB_hasGradAt_comp {N h w ic oc : ℕ} (p : R34DownW ic oc) (hq : R34DownPos p) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (hs : R34DownSmoothAt N h w p v) {G : Vec (N * (oc * h * w)) → Vec 1} {dy : Vec (N * (oc * h * w))} (hG : HasGradAt G (r34DownB N h w p v) dy) :

HasGradAt (fun (y : Vec (N * (ic * (2 * h) * (2 * w)))) => G (r34DownB N h w p y)) v (r34DownCotIn N h w p v dy)

…and through a downsample block (r34DownCotIn_eq_vjp).

source

theorem Proofs.ResNet34TieB.r34_net_lossGrad (N : ℕ) {nCls : ℕ} (hK : 0 < nCls) (xN cotN vN epsStr aStr negAK bStr logN ohN : String) (α B : ℝ) (w : R34BWeights nCls) (hq : R34PosB w) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) (hx : R34SmoothAtB N w x) (t : Vec (N * (1 * nCls))) (ht : ∀ (n : Fin N), ∑ k : Fin nCls, targetRow N nCls t n k = 1) :

have L := smoothedBatchLoss N nCls α B t; have g := BackLinks.unrowB N nCls (StableHLO.den (smoothedLossCotGraph N nCls α B aStr negAK bStr logN ohN (BackLinks.rowB N nCls (resnet34ForwardBFull N w x)) t)); have dyE1 := r34HeadCotBlk N 7 7 w.Wd w.bd (r34Pre16 N w x) g; have dyE0 := r34IdCotIn N 7 7 w.e1 (r34Pre15 N w x) dyE1; have dyD4 := r34IdCotIn N 7 7 w.e0 (r34Pre14 N w x) dyE0; have dyC4 := r34DownCotIn N 7 7 w.d4 (r34Pre13 N w x) dyD4; have dyC3 := r34IdCotIn N 14 14 w.c4 (r34Pre12 N w x) dyC4; have dyC2 := r34IdCotIn N 14 14 w.c3 (r34Pre11 N w x) dyC3; have dyC1 := r34IdCotIn N 14 14 w.c2 (r34Pre10 N w x) dyC2; have dyC0 := r34IdCotIn N 14 14 w.c1 (r34Pre9 N w x) dyC1; have dyD3 := r34IdCotIn N 14 14 w.c0 (r34Pre8 N w x) dyC0; have dyB2 := r34DownCotIn N 14 14 w.d3 (r34Pre7 N w x) dyD3; have dyB1 := r34IdCotIn N 28 28 w.b2 (r34Pre6 N w x) dyB2; have dyB0 := r34IdCotIn N 28 28 w.b1 (r34Pre5 N w x) dyB1; have dyD2 := r34IdCotIn N 28 28 w.b0 (r34Pre4 N w x) dyB0; have dyA2 := r34DownCotIn N 28 28 w.d2 (r34Pre3 N w x) dyD2; have dyA1 := r34IdCotIn N 56 56 w.a2 (r34Pre2 N w x) dyA2; have dyA0 := r34IdCotIn N 56 56 w.a1 (r34Pre1 N w x) dyA1; have cotPool := r34IdCotIn N 56 56 w.a0 (r34Pre0 N w x) dyA0; r34StemLossTiedB xN cotN vN epsStr w.sW w.sb w.sε w.sγ w.sβ x (fun (W : Kernel4 64 3 7 7) (b γ β : Vec 64) => L (resnet34ForwardBFull N { sW := W, sb := b, sε := w.sε, sγ := γ, sβ := β, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) cotPool ∧ r34IdLossTiedB xN cotN vN epsStr w.a0 (r34Pre0 N w x) (fun (p : R34IdW 64) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := p, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyA0 ∧ r34IdLossTiedB xN cotN vN epsStr w.a1 (r34Pre1 N w x) (fun (p : R34IdW 64) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := p, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyA1 ∧ r34IdLossTiedB xN cotN vN epsStr w.a2 (r34Pre2 N w x) (fun (p : R34IdW 64) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := p, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyA2 ∧ r34DownLossTiedB xN cotN vN epsStr w.d2 (r34Pre3 N w x) (fun (p : R34DownW 64 128) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := p, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyD2 ∧ r34IdLossTiedB xN cotN vN epsStr w.b0 (r34Pre4 N w x) (fun (p : R34IdW 128) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := p, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyB0 ∧ r34IdLossTiedB xN cotN vN epsStr w.b1 (r34Pre5 N w x) (fun (p : R34IdW 128) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := p, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyB1 ∧ r34IdLossTiedB xN cotN vN epsStr w.b2 (r34Pre6 N w x) (fun (p : R34IdW 128) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := p, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyB2 ∧ r34DownLossTiedB xN cotN vN epsStr w.d3 (r34Pre7 N w x) (fun (p : R34DownW 128 256) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := p, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyD3 ∧ r34IdLossTiedB xN cotN vN epsStr w.c0 (r34Pre8 N w x) (fun (p : R34IdW 256) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := p, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyC0 ∧ r34IdLossTiedB xN cotN vN epsStr w.c1 (r34Pre9 N w x) (fun (p : R34IdW 256) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := p, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyC1 ∧ r34IdLossTiedB xN cotN vN epsStr w.c2 (r34Pre10 N w x) (fun (p : R34IdW 256) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := p, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyC2 ∧ r34IdLossTiedB xN cotN vN epsStr w.c3 (r34Pre11 N w x) (fun (p : R34IdW 256) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := p, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyC3 ∧ r34IdLossTiedB xN cotN vN epsStr w.c4 (r34Pre12 N w x) (fun (p : R34IdW 256) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := p, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyC4 ∧ r34DownLossTiedB xN cotN vN epsStr w.d4 (r34Pre13 N w x) (fun (p : R34DownW 256 512) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := p, e0 := w.e0, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyD4 ∧ r34IdLossTiedB xN cotN vN epsStr w.e0 (r34Pre14 N w x) (fun (p : R34IdW 512) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := p, e1 := w.e1, Wd := w.Wd, bd := w.bd } x)) dyE0 ∧ r34IdLossTiedB xN cotN vN epsStr w.e1 (r34Pre15 N w x) (fun (p : R34IdW 512) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := p, Wd := w.Wd, bd := w.bd } x)) dyE1 ∧ r34HeadLossTiedB xN cotN w.Wd w.bd (r34Pre16 N w x) (fun (W : Mat 512 nCls) (b : Vec nCls) => L (resnet34ForwardBFull N { sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, a0 := w.a0, a1 := w.a1, a2 := w.a2, d2 := w.d2, b0 := w.b0, b1 := w.b1, b2 := w.b2, d3 := w.d3, c0 := w.c0, c1 := w.c1, c2 := w.c2, c3 := w.c3, c4 := w.c4, d4 := w.d4, e0 := w.e0, e1 := w.e1, Wd := W, bd := b } x)) g

Every ResNet-34 parameter gradient node is the derivative of the batched smoothed loss in that parameter. r34_net_tiedB threads the label-smoothed cotangent g down the emitted backward chain and ties each of the 146 parameter nodes to its layer's Jacobian at the cotangent reaching it. Here each node, at that same cotangent, is ∂L/∂θ of the WHOLE net — L the batched label-smoothed cross-entropy smoothedBatchLoss of resnet34ForwardBFull with that one parameter varied (a stem field, a block's weight record w.blk := p with one slot changed, or the classifier).

Hypotheses: every BN ε positive (R34PosB), every relu off its kink and the stem pool tie-free at the real activations (R34SmoothAtB), every example's target summing to one, and at least one class.

Documentation

LeanMlir.Proofs.Nets.ResNet.ResNet34ParamGrad

ResNet-34 — every parameter gradient node IS the loss's derivative in that parameter #