MobileNetV2 — the inference (frozen-statistics) stage vocabulary #

The eval twins of MobileNetV2RenderPC.lean's per-channel stage abbreviations: ivExpandPCEval / ivDepthwisePCEval / ivDepthwiseStridedPCEval / ivProjectPCEval and the two bodies (invresBodyPCEval, invresBodyStridedPCEval), every BN site at bnPerChannelEvalTensor3 (frozen running mean and variance). MobileNetV2FullPaperEval builds the shipped seventeen-block eval forward and its graph from them. 3-axiom clean.

source

@[reducible]

noncomputable def Proofs.ivExpandPCEval {ic mid h w kHe kWe : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe μe ve : Vec mid) :

Vec (ic * h * w) → Vec (mid * h * w)

Expand stage at inference: relu6 ∘ bnEval ∘ conv(1×1).

Equations

Proofs.ivExpandPCEval We be εe γe βe μe ve = Proofs.relu6 (mid * h * w) ∘ Proofs.bnPerChannelEvalTensor3 mid h w εe γe βe μe ve ∘ Proofs.flatConv We be

Instances For

source

@[reducible]

noncomputable def Proofs.ivDepthwisePCEval {mid h w kHd kWd : ℕ} (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd μd vd : Vec mid) :

Vec (mid * h * w) → Vec (mid * h * w)

Depthwise stage (stride-1) at inference.

Equations

Proofs.ivDepthwisePCEval Wd bd εd γd βd μd vd = Proofs.relu6 (mid * h * w) ∘ Proofs.bnPerChannelEvalTensor3 mid h w εd γd βd μd vd ∘ Proofs.depthwiseFlat Wd bd

Instances For

source

@[reducible]

noncomputable def Proofs.ivDepthwiseStridedPCEval {mid h w kHd kWd : ℕ} (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd μd vd : Vec mid) :

Vec (mid * (2 * h) * (2 * w)) → Vec (mid * h * w)

Depthwise stage (stride-2 downsample) at inference.

Equations

Proofs.ivDepthwiseStridedPCEval Wd bd εd γd βd μd vd = Proofs.relu6 (mid * h * w) ∘ Proofs.bnPerChannelEvalTensor3 mid h w εd γd βd μd vd ∘ Proofs.depthwiseStride2FlatXla Wd bd

Instances For

source

@[reducible]

noncomputable def Proofs.ivProjectPCEval {mid oc h w kHp kWp : ℕ} (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp μp vp : Vec oc) :

Vec (mid * h * w) → Vec (oc * h * w)

Project (linear bottleneck) stage at inference — no relu6.

Equations

Proofs.ivProjectPCEval Wp bp εp γp βp μp vp = Proofs.bnPerChannelEvalTensor3 oc h w εp γp βp μp vp ∘ Proofs.flatConv Wp bp

Instances For

source

@[reducible]

noncomputable def Proofs.invresBodyPCEval {ic mid oc h w : ℕ} (ε : ℝ) (We : Kernel4 mid ic 1 1) (be γe βe μe ve : Vec mid) (Wd : DepthwiseKernel mid 3 3) (bd γd βd μd vd : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp γp βp μp vp : Vec oc) :

Vec (ic * h * w) → Vec (oc * h * w)

Inverted-residual body (stride-1) at inference, at one shared ε.

Equations

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

Instances For

source

@[reducible]

noncomputable def Proofs.invresBodyStridedPCEval {ic mid oc h w : ℕ} (ε : ℝ) (We : Kernel4 mid ic 1 1) (be γe βe μe ve : Vec mid) (Wd : DepthwiseKernel mid 3 3) (bd γd βd μd vd : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp γp βp μp vp : Vec oc) :

Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

Inverted-residual body (stride-2 downsample) at inference: expand at 2h×2w, then the strided depthwise, then project.

Equations

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

Instances For

Documentation

LeanMlir.Proofs.Codegen.MobileNetV2RenderPCEval

MobileNetV2 — the inference (frozen-statistics) stage vocabulary #