Documentation

LeanMlir.Proofs.Nets.EfficientNet.EfficientNetChainClose

EfficientNet's per-block batched VJPs #

The batched block forwards of B0 at the index N·(c·h·w) the forward graph (EfficientNetStagesPC) uses, each with a HasVJP composed by vjpComp from the batched stage VJPs (Batched.Stages: cbsBHasVJP, dwbsBHasVJP, dwbsSXlaBHasVJP, seBHasVJP, projBHasVJP, and batchMapHasVJP for the per-example ops), and a _differentiable lemma for each:

Batch BatchNorm (bnBatchLA) is the one batch-coupled op; it sits inside the stage VJPs. swish is smooth, so every block has a global HasVJP.

source
theorem Proofs.mbNoExpFwdB_differentiable (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) :
Differentiable ℝ (mbNoExpFwdB N Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

MBConv1 (no expand), dw-bn-swish → SE → project-bn, is differentiable.

source
noncomputable def Proofs.mbNoExpFwdBHasVJP (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) :
HasVJP (mbNoExpFwdB N Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

The VJP of MBConv1 (no expand): the three stages' VJPs composed.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Proofs.mbStridedFwdB_differentiable (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) :
    Differentiable ℝ (mbStridedFwdB N We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

    MBConv6 strided, expand-bn-swish → strided dw-bn-swish → SE → project-bn, is differentiable.

    source
    noncomputable def Proofs.mbStridedFwdBHasVJP (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) :
    HasVJP (mbStridedFwdB N We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

    The VJP of the strided MBConv6: the four stages' VJPs composed.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Proofs.mbExpFwdB (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) :
      Vec (N * (ic * h * w)) → Vec (N * (oc * h * w))

      MBConv6 expand, stride-1, NO residual (stages 5/7's first block, ic ≠ oc): project-bn ∘ SE ∘ dw-bn-swish ∘ expand-bn-swish (the mbResidFwdB body without the identity skip).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Proofs.mbExpFwdB_differentiable (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) :
        Differentiable ℝ (mbExpFwdB N We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

        The stride-1 MBConv6 without the skip is differentiable.

        source
        noncomputable def Proofs.mbExpFwdBHasVJP (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) :
        HasVJP (mbExpFwdB N We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

        The VJP of the stride-1 MBConv6 without the skip: the four stages' VJPs composed.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Proofs.mbResidFwdB_differentiable (N : ℕ) {c mid h w kHd kWd r : ℕ} (We : Kernel4 mid c 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp : Vec c) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec c) :
          Differentiable ℝ (mbResidFwdB N We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

          The residual MBConv6, x + (project-bn ∘ SE ∘ dw-bn-swish ∘ expand-bn-swish)(x), is differentiable.

          source
          noncomputable def Proofs.mbResidFwdBHasVJP (N : ℕ) {c mid h w kHd kWd r : ℕ} (We : Kernel4 mid c 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp : Vec c) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec c) :
          HasVJP (mbResidFwdB N We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

          The VJP of the residual MBConv6: residualHasVJP over mbExpFwdBHasVJP.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Proofs.headFwdB_differentiable (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) :
            Differentiable ℝ (headFwdB N Wh bh εh γh βh Wfc bfc)

            The head, 1×1 conv-bn-swish → GAP → dense, is differentiable.

            source
            noncomputable def Proofs.headFwdBHasVJP (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) :
            HasVJP (headFwdB N Wh bh εh γh βh Wfc bfc)

            The VJP of the head: the conv stage's, then the per-example GAP's and dense's.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For