MobileNetV2 — every parameter gradient node IS the loss's derivative in that parameter #
mnv2_net_tiedB says each of the 210 parameter gradient nodes (158 emitted at the default
convBias := false) denotes its layer's parameter Jacobian contracted with the cotangent the
emitted backward chain threads to it, from a loss cotangent g; the *_eq_vjp lemmas say the
chain's segments are certified VJP backwards. mnv2_net_lossGrad composes them: for any loss L
of the logits whose gradient at the net's output is g, every node is ∂L/∂θ of the WHOLE net with
that one parameter varied. mnv2_net_lossGrad_smoothedCE discharges hL for the label-smoothed
loss the artifacts ship.
How. ResNet50ParamGrad's shape:
- Per stage (at variable widths): the loss read at each internal activation of the stem, the
t = 1block, the stride-1 body, the stride-2 body and the head (mnv2StemG*,mnv2NoExpG*,mnv2BodyG*,mnv2SBodyG*,mnv2HeadG*), its gradient the chain's own cotangent through relu6 (relu6HasVJPAt, whose backward ISrelu6MaskB), batch BN, and the conv, depthwise and XLA-SAMEstrided depthwise input-VJPs. The stride-1 body bundle covers both the skip blocks and the two widenings: a skip block's body sees the lossu ↦ Gn (u + v), whose gradient at the body output is stilldyOut(mnv2_resid_lossTiedB). - Per net: the loss read after each block (
mnv2Suf*), pulled back through the seventeen certified block VJPs and the head's, and eachΦidentified with the whole net at updated weights by a standalonemnv2_factor_*theorem.
Hypotheses. MNV2PosB (every BN ε > 0), MNV2SmoothAtB (all 35 relu6 sites off both kinks
at the real activations); for the smoothed loss every example's target summing to one and
0 < nCls.
theorem
Proofs.MobileNetV2TieB.dStridedXlaInB_eq_batchMapBackward
{N c h w kH kW : ℕ}
(W : DepthwiseKernel c kH kW)
(b : Vec c)
(x : Vec (N * (c * (2 * h) * (2 * w))))
(dy : Vec (N * (c * h * w)))
:
dStridedXlaInB N W b dy = (batchMapHasVJP (depthwiseStride2FlatXla W b) (depthwiseStride2FlatXlaHasVJP W b) ⋯).backward x dy
dStridedXlaInB — the emitted XLA-SAME strided depthwise input-cotangent — is the batched
strided depthwise VJP's backward, at any saved input.
noncomputable def
Proofs.MobileNetV2TieB.mnv2StemGC
(N h w : ℕ)
{oc : ℕ}
(Gn : Vec (N * (oc * h * w)) → Vec 1)
(εs : ℝ)
(γs βs : Vec oc)
:
The loss at the stem conv's output.
Equations
- Proofs.MobileNetV2TieB.mnv2StemGC N h w Gn εs γs βs z = Proofs.MobileNetV2TieB.mnv2StemGN N h w Gn (Proofs.StableHLO.bnBatchLA N oc h w εs γs βs z)
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2StemGC_hasGradAt
{N h w ic oc : ℕ}
(Ws : Kernel4 oc ic 3 3)
(bs : Vec oc)
(εs : ℝ)
(hεs : 0 < εs)
(γs βs : Vec oc)
(x : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : MNV2StemSmoothAtB N h w Ws bs εs γs βs x)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StemB N h w Ws bs εs γs βs x) dy)
:
HasGradAt (mnv2StemGN N h w Gn)
(StableHLO.bnBatchLA N oc h w εs γs βs (StableHLO.batchMap N (flatConvStride2Xla Ws bs) x))
(mnv2StemCotN N h w Ws bs εs γs βs x dy) ∧ HasGradAt (mnv2StemGC N h w Gn εs γs βs) (StableHLO.batchMap N (flatConvStride2Xla Ws bs) x)
(mnv2StemCotC N h w Ws bs εs γs βs x dy)
def
Proofs.MobileNetV2TieB.mnv2StemLossTiedB
{N h w ic oc : ℕ}
(xN cotN vN epsStr : String)
(Ws : Kernel4 oc ic 3 3)
(bs : Vec oc)
(εs : ℝ)
(γs βs : Vec oc)
(x : Vec (N * (ic * (2 * h) * (2 * w))))
(Φ : Kernel4 oc ic 3 3 → Vec oc → Vec oc → Vec oc → Vec 1)
(dy : Vec (N * (oc * h * w)))
:
Stem, every parameter node a loss derivative — the four nodes mnv2StemTiedB 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
theorem
Proofs.MobileNetV2TieB.mnv2_stem_lossTiedB
{N h w ic oc : ℕ}
(xN cotN vN epsStr : String)
(Ws : Kernel4 oc ic 3 3)
(bs : Vec oc)
(εs : ℝ)
(hεs : 0 < εs)
(γs βs : Vec oc)
(x : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : MNV2StemSmoothAtB N h w Ws bs εs γs βs x)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StemB N h w Ws bs εs γs βs x) dy)
{Φ : Kernel4 oc ic 3 3 → Vec oc → Vec oc → Vec oc → Vec 1}
(hΦ : ∀ (W : Kernel4 oc ic 3 3) (b γ β : Vec oc), Φ W b γ β = Gn (mnv2StemB N h w W b εs γ β x))
:
mnv2StemLossTiedB xN cotN vN epsStr Ws bs εs γs βs x Φ dy
noncomputable def
Proofs.MobileNetV2TieB.mnv2NoExpGPc
(N h w : ℕ)
{ic oc : ℕ}
(Gn : Vec (N * (oc * h * w)) → Vec 1)
(p : IVWNoExp ic oc)
:
The loss at the project conv's output (Gn is the loss at the block output, bnₚ's).
Equations
- Proofs.MobileNetV2TieB.mnv2NoExpGPc N h w Gn p z = Gn (Proofs.StableHLO.bnBatchLA N oc h w p.pε p.pγ p.pβ z)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2NoExpGDn
(N h w : ℕ)
{ic oc : ℕ}
(Gn : Vec (N * (oc * h * w)) → Vec 1)
(p : IVWNoExp ic oc)
:
The loss at the depthwise BN's output.
Equations
- Proofs.MobileNetV2TieB.mnv2NoExpGDn N h w Gn p u = Proofs.MobileNetV2TieB.mnv2NoExpGPc N h w Gn p (Proofs.StableHLO.batchMap N (Proofs.flatConv p.pW p.pb) (Proofs.relu6 (N * (ic * h * w)) u))
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2NoExpGDc
(N h w : ℕ)
{ic oc : ℕ}
(Gn : Vec (N * (oc * h * w)) → Vec 1)
(p : IVWNoExp ic oc)
:
The loss at the depthwise conv's output.
Equations
- Proofs.MobileNetV2TieB.mnv2NoExpGDc N h w Gn p z = Proofs.MobileNetV2TieB.mnv2NoExpGDn N h w Gn p (Proofs.StableHLO.bnBatchLA N ic h w p.dε p.dγ p.dβ z)
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2NoExpGPc_hasGradAt
{N h w ic oc : ℕ}
(p : IVWNoExp ic oc)
(hq : IVNoExpPos p)
(v : Vec (N * (ic * h * w)))
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2NoExpB N h w p v) dy)
:
HasGradAt (mnv2NoExpGPc N h w Gn p)
(StableHLO.batchMap N (flatConv p.pW p.pb) (StableHLO.dwbrB N p.dW p.db p.dε p.dγ p.dβ v))
(mnv2NoExpCotPc N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2NoExpGDn_hasGradAt
{N h w ic oc : ℕ}
(p : IVWNoExp ic oc)
(hq : IVNoExpPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVNoExpSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2NoExpB N h w p v) dy)
:
HasGradAt (mnv2NoExpGDn N h w Gn p)
(StableHLO.bnBatchLA N ic h w p.dε p.dγ p.dβ (StableHLO.batchMap N (depthwiseFlat p.dW p.db) v))
(mnv2NoExpCotDn N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2NoExpGDc_hasGradAt
{N h w ic oc : ℕ}
(p : IVWNoExp ic oc)
(hq : IVNoExpPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVNoExpSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2NoExpB N h w p v) dy)
:
HasGradAt (mnv2NoExpGDc N h w Gn p) (StableHLO.batchMap N (depthwiseFlat p.dW p.db) v) (mnv2NoExpCotDc N h w p v dy)
def
Proofs.MobileNetV2TieB.mnv2NoExpLossTiedB
{N h w ic oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVWNoExp ic oc)
(v : Vec (N * (ic * h * w)))
(Φ : IVWNoExp ic oc → Vec 1)
(dy : Vec (N * (oc * h * w)))
:
t = 1 block, every parameter node a loss derivative — the eight nodes mnv2NoExpTiedB
ties. The project BN's γ/β read dyOut itself: nothing follows the linear bottleneck.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_noexp_lossTiedB
{N h w ic oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVWNoExp ic oc)
(hq : IVNoExpPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVNoExpSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2NoExpB N h w p v) dy)
{Φ : IVWNoExp ic oc → Vec 1}
(hΦ : ∀ (p' : IVWNoExp ic oc), Φ p' = Gn (mnv2NoExpB N h w p' v))
:
mnv2NoExpLossTiedB xN cotN vN epsStr p v Φ dy
noncomputable def
Proofs.MobileNetV2TieB.mnv2BodyGPc
(N h w : ℕ)
{ic mid oc : ℕ}
(Gb : Vec (N * (oc * h * w)) → Vec 1)
(p : IVW ic mid oc)
:
Equations
- Proofs.MobileNetV2TieB.mnv2BodyGPc N h w Gb p z = Gb (Proofs.StableHLO.bnBatchLA N oc h w p.pε p.pγ p.pβ z)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2BodyGDn
(N h w : ℕ)
{ic mid oc : ℕ}
(Gb : Vec (N * (oc * h * w)) → Vec 1)
(p : IVW ic mid oc)
:
Equations
- Proofs.MobileNetV2TieB.mnv2BodyGDn N h w Gb p u = Proofs.MobileNetV2TieB.mnv2BodyGPc N h w Gb p (Proofs.StableHLO.batchMap N (Proofs.flatConv p.pW p.pb) (Proofs.relu6 (N * (mid * h * w)) u))
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2BodyGDc
(N h w : ℕ)
{ic mid oc : ℕ}
(Gb : Vec (N * (oc * h * w)) → Vec 1)
(p : IVW ic mid oc)
:
Equations
- Proofs.MobileNetV2TieB.mnv2BodyGDc N h w Gb p z = Proofs.MobileNetV2TieB.mnv2BodyGDn N h w Gb p (Proofs.StableHLO.bnBatchLA N mid h w p.dε p.dγ p.dβ z)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2BodyGEc
(N h w : ℕ)
{ic mid oc : ℕ}
(Gb : Vec (N * (oc * h * w)) → Vec 1)
(p : IVW ic mid oc)
:
Equations
- Proofs.MobileNetV2TieB.mnv2BodyGEc N h w Gb p z = Proofs.MobileNetV2TieB.mnv2BodyGEn N h w Gb p (Proofs.StableHLO.bnBatchLA N mid h w p.eε p.eγ p.eβ z)
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2BodyGPc_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * h * w)))
{Gb : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGb : HasGradAt Gb (mnv2ExpOnlyB N h w p v) dy)
:
HasGradAt (mnv2BodyGPc N h w Gb p)
(StableHLO.batchMap N (flatConv p.pW p.pb) (StableHLO.dwbrB N p.dW p.db p.dε p.dγ p.dβ (mnv2XE N h w p v)))
(mnv2CotPc N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2BodyGDn_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVSmoothAtB N h w p v)
{Gb : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGb : HasGradAt Gb (mnv2ExpOnlyB N h w p v) dy)
:
HasGradAt (mnv2BodyGDn N h w Gb p)
(StableHLO.bnBatchLA N mid h w p.dε p.dγ p.dβ (StableHLO.batchMap N (depthwiseFlat p.dW p.db) (mnv2XE N h w p v)))
(mnv2CotDn N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2BodyGDc_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVSmoothAtB N h w p v)
{Gb : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGb : HasGradAt Gb (mnv2ExpOnlyB N h w p v) dy)
:
HasGradAt (mnv2BodyGDc N h w Gb p) (StableHLO.batchMap N (depthwiseFlat p.dW p.db) (mnv2XE N h w p v))
(mnv2CotDc N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2BodyGEn_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVSmoothAtB N h w p v)
{Gb : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGb : HasGradAt Gb (mnv2ExpOnlyB N h w p v) dy)
:
HasGradAt (mnv2BodyGEn N h w Gb p)
(StableHLO.bnBatchLA N mid h w p.eε p.eγ p.eβ (StableHLO.batchMap N (flatConv p.eW p.eb) v)) (mnv2CotEn N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2BodyGEc_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVSmoothAtB N h w p v)
{Gb : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGb : HasGradAt Gb (mnv2ExpOnlyB N h w p v) dy)
:
HasGradAt (mnv2BodyGEc N h w Gb p) (StableHLO.batchMap N (flatConv p.eW p.eb) v) (mnv2CotEc N h w p v dy)
def
Proofs.MobileNetV2TieB.mnv2Stride1LossTiedB
{N h w ic mid oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVW ic mid oc)
(v : Vec (N * (ic * h * w)))
(Φ : IVW ic mid oc → Vec 1)
(dy : Vec (N * (oc * h * w)))
:
Stride-1 body, every parameter node a loss derivative — the twelve nodes
mnv2Stride1TiedB ties, Φ the loss at the body output as a function of the weight record.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_stride1_lossTiedB
{N h w ic mid oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVSmoothAtB N h w p v)
{Gb : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGb : HasGradAt Gb (mnv2ExpOnlyB N h w p v) dy)
{Φ : IVW ic mid oc → Vec 1}
(hΦ : ∀ (p' : IVW ic mid oc), Φ p' = Gb (mnv2ExpOnlyB N h w p' v))
:
mnv2Stride1LossTiedB xN cotN vN epsStr p v Φ dy
The stride-1 body bundle, from the loss Gb at the body output. A widening block (b11,
b17) is this at Gb := Gn.
theorem
Proofs.MobileNetV2TieB.mnv2_resid_lossTiedB
{N h w mid c : ℕ}
(xN cotN vN epsStr : String)
(p : IVW c mid c)
(hq : IVPos p)
(v : Vec (N * (c * h * w)))
(hs : IVSmoothAtB N h w p v)
{Gn : Vec (N * (c * h * w)) → Vec 1}
{dy : Vec (N * (c * h * w))}
(hGn : HasGradAt Gn (mnv2ResidB N h w p v) dy)
{Φ : IVW c mid c → Vec 1}
(hΦ : ∀ (p' : IVW c mid c), Φ p' = Gn (mnv2ResidB N h w p' v))
:
mnv2Stride1LossTiedB xN cotN vN epsStr p v Φ dy
A skip block's twelve nodes. The identity skip is a constant once a body parameter varies,
so the loss at the body output has gradient dyOut there and the body bundle applies.
noncomputable def
Proofs.MobileNetV2TieB.mnv2SBodyGPc
(N h w : ℕ)
{ic mid oc : ℕ}
(Gn : Vec (N * (oc * h * w)) → Vec 1)
(p : IVW ic mid oc)
:
Equations
- Proofs.MobileNetV2TieB.mnv2SBodyGPc N h w Gn p z = Gn (Proofs.StableHLO.bnBatchLA N oc h w p.pε p.pγ p.pβ z)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SBodyGDn
(N h w : ℕ)
{ic mid oc : ℕ}
(Gn : Vec (N * (oc * h * w)) → Vec 1)
(p : IVW ic mid oc)
:
Equations
- Proofs.MobileNetV2TieB.mnv2SBodyGDn N h w Gn p u = Proofs.MobileNetV2TieB.mnv2SBodyGPc N h w Gn p (Proofs.StableHLO.batchMap N (Proofs.flatConv p.pW p.pb) (Proofs.relu6 (N * (mid * h * w)) u))
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SBodyGDc
(N h w : ℕ)
{ic mid oc : ℕ}
(Gn : Vec (N * (oc * h * w)) → Vec 1)
(p : IVW ic mid oc)
:
Equations
- Proofs.MobileNetV2TieB.mnv2SBodyGDc N h w Gn p z = Proofs.MobileNetV2TieB.mnv2SBodyGDn N h w Gn p (Proofs.StableHLO.bnBatchLA N mid h w p.dε p.dγ p.dβ z)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2SBodyGEc
(N h w : ℕ)
{ic mid oc : ℕ}
(Gn : Vec (N * (oc * h * w)) → Vec 1)
(p : IVW ic mid oc)
:
Equations
- Proofs.MobileNetV2TieB.mnv2SBodyGEc N h w Gn p z = Proofs.MobileNetV2TieB.mnv2SBodyGEn N h w Gn p (Proofs.StableHLO.bnBatchLA N mid (2 * h) (2 * w) p.eε p.eγ p.eβ z)
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2SBodyGPc_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StridedB N h w p v) dy)
:
HasGradAt (mnv2SBodyGPc N h w Gn p)
(StableHLO.batchMap N (flatConv p.pW p.pb) (StableHLO.dwbrBstrided N p.dW p.db p.dε p.dγ p.dβ (mnv2XES N h w p v)))
(mnv2SCotPc N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2SBodyGDn_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : IVStridedSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StridedB N h w p v) dy)
:
HasGradAt (mnv2SBodyGDn N h w Gn p)
(StableHLO.bnBatchLA N mid h w p.dε p.dγ p.dβ
(StableHLO.batchMap N (depthwiseStride2FlatXla p.dW p.db) (mnv2XES N h w p v)))
(mnv2SCotDn N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2SBodyGDc_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : IVStridedSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StridedB N h w p v) dy)
:
HasGradAt (mnv2SBodyGDc N h w Gn p) (StableHLO.batchMap N (depthwiseStride2FlatXla p.dW p.db) (mnv2XES N h w p v))
(mnv2SCotDc N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2SBodyGEn_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : IVStridedSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StridedB N h w p v) dy)
:
HasGradAt (mnv2SBodyGEn N h w Gn p)
(StableHLO.bnBatchLA N mid (2 * h) (2 * w) p.eε p.eγ p.eβ (StableHLO.batchMap N (flatConv p.eW p.eb) v))
(mnv2SCotEn N h w p v dy)
theorem
Proofs.MobileNetV2TieB.mnv2SBodyGEc_hasGradAt
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : IVStridedSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StridedB N h w p v) dy)
:
HasGradAt (mnv2SBodyGEc N h w Gn p) (StableHLO.batchMap N (flatConv p.eW p.eb) v) (mnv2SCotEc N h w p v dy)
def
Proofs.MobileNetV2TieB.mnv2Stride2LossTiedB
{N h w ic mid oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVW ic mid oc)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(Φ : IVW ic mid oc → Vec 1)
(dy : Vec (N * (oc * h * w)))
:
Stride-2 block, every parameter node a loss derivative — the twelve nodes
mnv2Stride2TiedB ties; the depthwise nodes are the XLA-SAME strided ones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_stride2_lossTiedB
{N h w ic mid oc : ℕ}
(xN cotN vN epsStr : String)
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : IVStridedSmoothAtB N h w p v)
{Gn : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hGn : HasGradAt Gn (mnv2StridedB N h w p v) dy)
{Φ : IVW ic mid oc → Vec 1}
(hΦ : ∀ (p' : IVW ic mid oc), Φ p' = Gn (mnv2StridedB N h w p' v))
:
mnv2Stride2LossTiedB xN cotN vN epsStr p v Φ dy
noncomputable def
Proofs.MobileNetV2TieB.mnv2HeadGA
(N : ℕ)
{oc nCls : ℕ}
(L : Vec (N * nCls) → Vec 1)
(Wd : Mat oc nCls)
(bd : Vec nCls)
:
The loss at the GAP output (the classifier's input).
Equations
- Proofs.MobileNetV2TieB.mnv2HeadGA N L Wd bd a = L (Proofs.StableHLO.batchMap N (Proofs.dense Wd bd) a)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2HeadGHr
(N h w : ℕ)
{oc nCls : ℕ}
(L : Vec (N * nCls) → Vec 1)
(Wd : Mat oc nCls)
(bd : Vec nCls)
:
The loss at the head relu6's output.
Equations
- Proofs.MobileNetV2TieB.mnv2HeadGHr N h w L Wd bd u = Proofs.MobileNetV2TieB.mnv2HeadGA N L Wd bd (Proofs.StableHLO.batchMap N (Proofs.globalAvgPoolFlat oc h w) u)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2HeadGHn
(N h w : ℕ)
{oc nCls : ℕ}
(L : Vec (N * nCls) → Vec 1)
(Wd : Mat oc nCls)
(bd : Vec nCls)
:
The loss at the head BN's output.
Equations
- Proofs.MobileNetV2TieB.mnv2HeadGHn N h w L Wd bd u = Proofs.MobileNetV2TieB.mnv2HeadGHr N h w L Wd bd (Proofs.relu6 (N * (oc * h * w)) u)
Instances For
noncomputable def
Proofs.MobileNetV2TieB.mnv2HeadGHc
(N h w : ℕ)
{oc nCls : ℕ}
(L : Vec (N * nCls) → Vec 1)
(εh : ℝ)
(γh βh : Vec oc)
(Wd : Mat oc nCls)
(bd : Vec nCls)
:
The loss at the head conv's output.
Equations
- Proofs.MobileNetV2TieB.mnv2HeadGHc N h w L εh γh βh Wd bd z = Proofs.MobileNetV2TieB.mnv2HeadGHn N h w L Wd bd (Proofs.StableHLO.bnBatchLA N oc h w εh γh βh z)
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2HeadGHc_hasGradAt
{N h w ic oc nCls : ℕ}
(Wh : Kernel4 oc ic 1 1)
(bh : Vec oc)
(εh : ℝ)
(hεh : 0 < εh)
(γh βh : Vec oc)
(Wd : Mat oc nCls)
(bd : Vec nCls)
(v : Vec (N * (ic * h * w)))
(hs : MNV2HeadSmoothAtB N h w Wh bh εh γh βh v)
{L : Vec (N * nCls) → Vec 1}
{g : Vec (N * nCls)}
(hL : HasGradAt L (mnv2HeadB N h w Wh bh εh γh βh Wd bd v) g)
:
HasGradAt (mnv2HeadGHn N h w L Wd bd) (StableHLO.bnBatchLA N oc h w εh γh βh (StableHLO.batchMap N (flatConv Wh bh) v))
(mnv2HeadCotHn N h w Wh bh εh γh βh Wd v g) ∧ HasGradAt (mnv2HeadGHc N h w L εh γh βh Wd bd) (StableHLO.batchMap N (flatConv Wh bh) v)
(mnv2HeadCotHc N h w Wh bh εh γh βh Wd v g)
def
Proofs.MobileNetV2TieB.mnv2HeadLossTiedB
{N h w ic oc nCls : ℕ}
(xN cotN vN epsStr : String)
(Wh : Kernel4 oc ic 1 1)
(bh : Vec oc)
(εh : ℝ)
(γh βh : Vec oc)
(Wd : Mat oc nCls)
(bd : Vec nCls)
(v : Vec (N * (ic * h * w)))
(Φ : Kernel4 oc ic 1 1 → Vec oc → Vec oc → Vec oc → Mat oc nCls → Vec nCls → Vec 1)
(g : Vec (N * nCls))
:
Head, every parameter node a loss derivative — the six nodes mnv2HeadTiedB ties, Φ
the loss as a function of (hW, hb, hγ, hβ, Wd, bd).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_head_lossTiedB
{N h w ic oc nCls : ℕ}
(xN cotN vN epsStr : String)
(Wh : Kernel4 oc ic 1 1)
(bh : Vec oc)
(εh : ℝ)
(hεh : 0 < εh)
(γh βh : Vec oc)
(Wd : Mat oc nCls)
(bd : Vec nCls)
(v : Vec (N * (ic * h * w)))
(hs : MNV2HeadSmoothAtB N h w Wh bh εh γh βh v)
{L : Vec (N * nCls) → Vec 1}
{g : Vec (N * nCls)}
(hL : HasGradAt L (mnv2HeadB N h w Wh bh εh γh βh Wd bd v) g)
{Φ : Kernel4 oc ic 1 1 → Vec oc → Vec oc → Vec oc → Mat oc nCls → Vec nCls → Vec 1}
(hΦ :
∀ (W : Kernel4 oc ic 1 1) (b γ β : Vec oc) (Wd' : Mat oc nCls) (bd' : Vec nCls),
Φ W b γ β Wd' bd' = L (mnv2HeadB N h w W b εh γ β Wd' bd' v))
:
mnv2HeadLossTiedB xN cotN vN epsStr Wh bh εh γh βh Wd bd v Φ g
theorem
Proofs.MobileNetV2TieB.mnv2NoExpB_hasGradAt_comp
{N h w ic oc : ℕ}
(p : IVWNoExp ic oc)
(hq : IVNoExpPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVNoExpSmoothAtB N h w p v)
{G : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hG : HasGradAt G (mnv2NoExpB N h w p v) dy)
:
HasGradAt (fun (y : Vec (N * (ic * h * w))) => G (mnv2NoExpB N h w p y)) v (mnv2NoExpCotIn N h w p v dy)
Pull the loss gradient back through the t = 1 block (mnv2NoExpCotIn_eq_vjp).
theorem
Proofs.MobileNetV2TieB.mnv2ExpOnlyB_hasGradAt_comp
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * h * w)))
(hs : IVSmoothAtB N h w p v)
{G : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hG : HasGradAt G (mnv2ExpOnlyB N h w p v) dy)
:
HasGradAt (fun (y : Vec (N * (ic * h * w))) => G (mnv2ExpOnlyB N h w p y)) v (mnv2CotInBody N h w p v dy)
…through a widening block (mnv2ExpOnlyCotIn_eq_vjp).
theorem
Proofs.MobileNetV2TieB.mnv2ResidB_hasGradAt_comp
{N h w c mid : ℕ}
(p : IVW c mid c)
(hq : IVPos p)
(v : Vec (N * (c * h * w)))
(hs : IVSmoothAtB N h w p v)
{G : Vec (N * (c * h * w)) → Vec 1}
{dy : Vec (N * (c * h * w))}
(hG : HasGradAt G (mnv2ResidB N h w p v) dy)
:
HasGradAt (fun (y : Vec (N * (c * h * w))) => G (mnv2ResidB N h w p y)) v (mnv2ResidCotIn N h w p v dy)
…through a skip block (mnv2ResidCotIn_eq_vjp).
theorem
Proofs.MobileNetV2TieB.mnv2StridedB_hasGradAt_comp
{N h w ic mid oc : ℕ}
(p : IVW ic mid oc)
(hq : IVPos p)
(v : Vec (N * (ic * (2 * h) * (2 * w))))
(hs : IVStridedSmoothAtB N h w p v)
{G : Vec (N * (oc * h * w)) → Vec 1}
{dy : Vec (N * (oc * h * w))}
(hG : HasGradAt G (mnv2StridedB N h w p v) dy)
:
HasGradAt (fun (y : Vec (N * (ic * (2 * h) * (2 * w)))) => G (mnv2StridedB N h w p y)) v (mnv2StridedCotIn N h w p v dy)
…and through a stride-2 block (mnv2StridedCotIn_eq_vjp).
The net after block b16: block b17, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB16 N w y = Proofs.MobileNetV2TieB.mnv2SufB17 N w (Proofs.mnv2ExpOnlyB N 7 7 w.b17 y)
Instances For
The net after block b15: block b16, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB15 N w y = Proofs.MobileNetV2TieB.mnv2SufB16 N w (Proofs.mnv2ResidB N 7 7 w.b16 y)
Instances For
The net after block b14: block b15, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB14 N w y = Proofs.MobileNetV2TieB.mnv2SufB15 N w (Proofs.mnv2ResidB N 7 7 w.b15 y)
Instances For
The net after block b13: block b14, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB13 N w y = Proofs.MobileNetV2TieB.mnv2SufB14 N w (Proofs.mnv2StridedB N 7 7 w.b14 y)
Instances For
The net after block b12: block b13, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB12 N w y = Proofs.MobileNetV2TieB.mnv2SufB13 N w (Proofs.mnv2ResidB N 14 14 w.b13 y)
Instances For
The net after block b11: block b12, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB11 N w y = Proofs.MobileNetV2TieB.mnv2SufB12 N w (Proofs.mnv2ResidB N 14 14 w.b12 y)
Instances For
The net after block b10: block b11, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB10 N w y = Proofs.MobileNetV2TieB.mnv2SufB11 N w (Proofs.mnv2ExpOnlyB N 14 14 w.b11 y)
Instances For
The net after block b9: block b10, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB9 N w y = Proofs.MobileNetV2TieB.mnv2SufB10 N w (Proofs.mnv2ResidB N 14 14 w.b10 y)
Instances For
The net after block b8: block b9, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB8 N w y = Proofs.MobileNetV2TieB.mnv2SufB9 N w (Proofs.mnv2ResidB N 14 14 w.b9 y)
Instances For
The net after block b7: block b8, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB7 N w y = Proofs.MobileNetV2TieB.mnv2SufB8 N w (Proofs.mnv2ResidB N 14 14 w.b8 y)
Instances For
The net after block b6: block b7, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB6 N w y = Proofs.MobileNetV2TieB.mnv2SufB7 N w (Proofs.mnv2StridedB N 14 14 w.b7 y)
Instances For
The net after block b5: block b6, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB5 N w y = Proofs.MobileNetV2TieB.mnv2SufB6 N w (Proofs.mnv2ResidB N 28 28 w.b6 y)
Instances For
The net after block b4: block b5, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB4 N w y = Proofs.MobileNetV2TieB.mnv2SufB5 N w (Proofs.mnv2ResidB N 28 28 w.b5 y)
Instances For
The net after block b3: block b4, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB3 N w y = Proofs.MobileNetV2TieB.mnv2SufB4 N w (Proofs.mnv2StridedB N 28 28 w.b4 y)
Instances For
The net after block b2: block b3, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB2 N w y = Proofs.MobileNetV2TieB.mnv2SufB3 N w (Proofs.mnv2ResidB N 56 56 w.b3 y)
Instances For
The net after block b1: block b2, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufB1 N w y = Proofs.MobileNetV2TieB.mnv2SufB2 N w (Proofs.mnv2StridedB N 56 56 w.b2 y)
Instances For
The net after the stem: block b1, then the rest.
Equations
- Proofs.MobileNetV2TieB.mnv2SufStem N w y = Proofs.MobileNetV2TieB.mnv2SufB1 N w (Proofs.mnv2NoExpB N 112 112 w.b1 y)
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_factor_stem
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(W : Kernel4 32 3 3 3)
(b γ β : Vec 32)
:
mobilenetv2ForwardBFull N
{ sW := W, sb := b, sε := w.sε, sγ := γ, sβ := β, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4, b5 := w.b5,
b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufStem N w (mnv2StemB N 112 112 W b w.sε γ β x)
The net with the stem's parameters varied is the suffix after the stem at the varied stem.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b1
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVWNoExp 32 16)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := p, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12,
b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε,
hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB1 N w (mnv2NoExpB N 112 112 p (mnv2PreB0 N w x))
The net with block b1's weights varied is the suffix after b1 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b2
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 16 96 24)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := p, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12,
b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε,
hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB2 N w (mnv2StridedB N 56 56 p (mnv2PreB1 N w x))
The net with block b2's weights varied is the suffix after b2 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b3
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 24 144 24)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := p, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12,
b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε,
hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB3 N w (mnv2ResidB N 56 56 p (mnv2PreB2 N w x))
The net with block b3's weights varied is the suffix after b3 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b4
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 24 144 32)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := p,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12,
b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε,
hγ := w.hγ, hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB4 N w (mnv2StridedB N 28 28 p (mnv2PreB3 N w x))
The net with block b4's weights varied is the suffix after b4 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b5
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 32 192 32)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := p, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB5 N w (mnv2ResidB N 28 28 p (mnv2PreB4 N w x))
The net with block b5's weights varied is the suffix after b5 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b6
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 32 192 32)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := p, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB6 N w (mnv2ResidB N 28 28 p (mnv2PreB5 N w x))
The net with block b6's weights varied is the suffix after b6 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b7
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 32 192 64)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := p, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB7 N w (mnv2StridedB N 14 14 p (mnv2PreB6 N w x))
The net with block b7's weights varied is the suffix after b7 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b8
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 64 384 64)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := p, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB8 N w (mnv2ResidB N 14 14 p (mnv2PreB7 N w x))
The net with block b8's weights varied is the suffix after b8 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b9
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 64 384 64)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := p, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := w.b13,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB9 N w (mnv2ResidB N 14 14 p (mnv2PreB8 N w x))
The net with block b9's weights varied is the suffix after b9 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b10
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 64 384 64)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := p, b11 := w.b11, b12 := w.b12, b13 := w.b13,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB10 N w (mnv2ResidB N 14 14 p (mnv2PreB9 N w x))
The net with block b10's weights varied is the suffix after b10 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b11
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 64 384 96)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := p, b12 := w.b12, b13 := w.b13,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB11 N w (mnv2ExpOnlyB N 14 14 p (mnv2PreB10 N w x))
The net with block b11's weights varied is the suffix after b11 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b12
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 96 576 96)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := p, b13 := w.b13,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB12 N w (mnv2ResidB N 14 14 p (mnv2PreB11 N w x))
The net with block b12's weights varied is the suffix after b12 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b13
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 96 576 96)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12, b13 := p,
b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB13 N w (mnv2ResidB N 14 14 p (mnv2PreB12 N w x))
The net with block b13's weights varied is the suffix after b13 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b14
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 96 576 160)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12,
b13 := w.b13, b14 := p, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB14 N w (mnv2StridedB N 7 7 p (mnv2PreB13 N w x))
The net with block b14's weights varied is the suffix after b14 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b15
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 160 960 160)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12,
b13 := w.b13, b14 := w.b14, b15 := p, b16 := w.b16, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB15 N w (mnv2ResidB N 7 7 p (mnv2PreB14 N w x))
The net with block b15's weights varied is the suffix after b15 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b16
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 160 960 160)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12,
b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := p, b17 := w.b17, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB16 N w (mnv2ResidB N 7 7 p (mnv2PreB15 N w x))
The net with block b16's weights varied is the suffix after b16 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_b17
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(p : IVW 160 960 320)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12,
b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := p, hW := w.hW, hb := w.hb, hε := w.hε, hγ := w.hγ,
hβ := w.hβ, fcW := w.fcW, fcb := w.fcb }
x = mnv2SufB17 N w (mnv2ExpOnlyB N 7 7 p (mnv2PreB16 N w x))
The net with block b17's weights varied is the suffix after b17 at the varied block.
theorem
Proofs.MobileNetV2TieB.mnv2_factor_head
(N : ℕ)
{nCls : ℕ}
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(W : Kernel4 1280 320 1 1)
(b γ β : Vec 1280)
(Wd : Mat 1280 nCls)
(bd : Vec nCls)
:
mobilenetv2ForwardBFull N
{ sW := w.sW, sb := w.sb, sε := w.sε, sγ := w.sγ, sβ := w.sβ, b1 := w.b1, b2 := w.b2, b3 := w.b3, b4 := w.b4,
b5 := w.b5, b6 := w.b6, b7 := w.b7, b8 := w.b8, b9 := w.b9, b10 := w.b10, b11 := w.b11, b12 := w.b12,
b13 := w.b13, b14 := w.b14, b15 := w.b15, b16 := w.b16, b17 := w.b17, hW := W, hb := b, hε := w.hε, hγ := γ,
hβ := β, fcW := Wd, fcb := bd }
x = mnv2HeadB N 7 7 W b w.hε γ β Wd bd (mnv2PreB17 N w x)
The net with the head varied is the head at the varied parameters.
def
Proofs.MobileNetV2TieB.MNV2NetLossTiedB
(N : ℕ)
{nCls : ℕ}
(xN cotN vN epsStr : String)
(w : MNV2BWeights nCls)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(L : Vec (N * nCls) → Vec 1)
(g : Vec (N * nCls))
:
Every MobileNetV2 parameter gradient node is the derivative of L in that parameter, for a
loss L of the logits and g the cotangent the chain starts from: the 210 slots
mnv2_net_tiedB ties, each at the cotangent the emitted chain threads to it, stated against L
of mobilenetv2ForwardBFull with that one parameter varied.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.MobileNetV2TieB.mnv2_net_lossGrad
(N : ℕ)
{nCls : ℕ}
(xN cotN vN epsStr : String)
(w : MNV2BWeights nCls)
(hq : MNV2PosB w)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(hx : MNV2SmoothAtB N w x)
{L : Vec (N * nCls) → Vec 1}
{g : Vec (N * nCls)}
(hL : HasGradAt L (mobilenetv2ForwardBFull N w x) g)
:
MNV2NetLossTiedB N xN cotN vN epsStr w x L g
Every MobileNetV2 parameter gradient node is the derivative of the loss in that
parameter. For any loss L of the logits with gradient g at the net's output, each of the
210 slots mnv2_net_tiedB ties — at the same cotangent — is ∂L/∂θ of the WHOLE net,
mobilenetv2ForwardBFull with that one parameter varied (a stem field, a block's weight record
w.bk := p with one slot changed, or a head field).
Hypotheses: every BN ε positive (MNV2PosB) and all 35 relu6 sites off both kinks at the real
activations (MNV2SmoothAtB). The loss enters only through hL;
mnv2_net_lossGrad_smoothedCE discharges it for the loss the artifacts ship.
theorem
Proofs.MobileNetV2TieB.mnv2_net_lossGrad_smoothedCE
(N : ℕ)
{nCls : ℕ}
(hK : 0 < nCls)
(xN cotN vN epsStr aStr negAK bStr logN ohN : String)
(α B : ℝ)
(w : MNV2BWeights nCls)
(hq : MNV2PosB w)
(x : Vec (N * (3 * (2 * 112) * (2 * 112))))
(hx : MNV2SmoothAtB N w x)
(t : Vec (N * (1 * nCls)))
(ht : ∀ (n : Fin N), ∑ k : Fin nCls, targetRow N nCls t n k = 1)
:
MNV2NetLossTiedB N xN cotN vN epsStr w x (smoothedBatchLoss N nCls α B t)
(BackLinks.unrowB N nCls
(StableHLO.den
(smoothedLossCotGraph N nCls α B aStr negAK bStr logN ohN (BackLinks.rowB N nCls (mobilenetv2ForwardBFull N w x))
t)))
The loss the artifacts ship: every node is the derivative of the batched label-smoothed
cross-entropy smoothedBatchLoss, g the six-op cotangent the render emits.