EfficientNet's MBConv1 and head backward graphs #
The backward graphs of the two EfficientNet stage forwards not covered in EfficientNetBackB0.lean:
mbNoExpBackBatchedGraph_faithful (MBConv1, projB ∘ seB ∘ dwbsB — no expand stage) and
headBackBatchedGraph_faithful (dense ∘ GAP ∘ cbsB).
Every stage here is GLOBAL #
EfficientNet is swish/sigmoid throughout, both smooth, so every layer below has ok = True: the
backward graph denotes the VJP at every input, no side conditions. Contrast MNv4/R34/R50, whose
relu kinks force _at.
Where each EfficientNet stage forward's backward graph lives:
| forward | backward-graph theorem |
|---|---|
mbStridedFwdB | mbDownBodyBackBatchedGraph_faithful certifies mbStridedFwdBHasVJP itself |
mbExpFwdB | mbBodyBackBatchedGraph_faithful certifies mbExpFwdBHasVJP at ic = oc (the graph's type) |
mbNoExpFwdB | mbNoExpBackBatchedGraph_faithful (below) |
headFwdB | headBackBatchedGraph_faithful (below) |
noncomputable def
Proofs.StableHLO.mbNoExpBackBatchedGraph
{N ic oc h w kHd kWd r : ℕ}
(Wd : DepthwiseKernel ic kHd kWd)
(bd : Vec ic)
(εd : ℝ)
(γd βd : Vec ic)
(Wz₁ : Mat ic r)
(bz₁ : Vec r)
(Wz₂ : Mat r ic)
(bz₂ : Vec ic)
(Wp : Kernel4 oc ic 1 1)
(bp : Vec oc)
(εp : ℝ)
(γp βp : Vec oc)
(x : Vec (N * (ic * h * w)))
(e : SHlo (N * (oc * h * w)))
:
mbNoExpFwdB's backward graph — MBConv1 has no expand stage, so the chain is
dwbsB⁻¹ ∘ seB⁻¹ ∘ projB⁻¹.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Proofs.StableHLO.mbNoExpBackBatchedGraph_faithful
{N ic oc h w kHd kWd r : ℕ}
(Wd : DepthwiseKernel ic kHd kWd)
(bd : Vec ic)
(εd : ℝ)
(hεd : 0 < εd)
(γd βd : Vec ic)
(Wz₁ : Mat ic r)
(bz₁ : Vec r)
(Wz₂ : Mat r ic)
(bz₂ : Vec ic)
(Wp : Kernel4 oc ic 1 1)
(bp : Vec oc)
(εp : ℝ)
(hεp : 0 < εp)
(γp βp : Vec oc)
(x : Vec (N * (ic * h * w)))
(e : SHlo (N * (oc * h * w)))
:
den (mbNoExpBackBatchedGraph Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp x e) = (mbNoExpFwdBHasVJP N Wd bd εd hεd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp hεp γp βp).backward x (den e)
noncomputable def
Proofs.StableHLO.headBackBatchedGraph
{N c oc h w nC : ℕ}
(Wh : Kernel4 oc c 1 1)
(bh : Vec oc)
(εh : ℝ)
(γh βh : Vec oc)
(Wfc : Mat oc nC)
(_bfc : Vec nC)
(x : Vec (N * (c * h * w)))
(e : SHlo (N * nC))
:
headFwdB's backward graph — cbsB⁻¹ ∘ GAP⁻¹ ∘ dense⁻¹. The EfficientNet peer of
MNv4's head.
Equations
- Proofs.StableHLO.headBackBatchedGraph Wh bh εh γh βh Wfc _bfc x e = Proofs.StableHLO.cbsBackBatchedGraph Wh bh εh γh βh x (Proofs.StableHLO.SHlo.denseRowBack "%Wfc" Wfc e).gapBackBatched
Instances For
theorem
Proofs.StableHLO.headBackBatchedGraph_faithful
{N c oc h w nC : ℕ}
(Wh : Kernel4 oc c 1 1)
(bh : Vec oc)
(εh : ℝ)
(hεh : 0 < εh)
(γh βh : Vec oc)
(Wfc : Mat oc nC)
(bfc : Vec nC)
(x : Vec (N * (c * h * w)))
(e : SHlo (N * nC))
:
den (headBackBatchedGraph Wh bh εh γh βh Wfc bfc x e) = (headFwdBHasVJP N Wh bh εh hεh γh βh Wfc bfc).backward x (den e)