MobileNetV4-Conv-M at inference — eval forward + graph + faithfulness, at any resolution #
The eval twin of MobileNetV4FullB.lean. That file states Conv-M at TRAINING BatchNorm
(bnBatchLA) at 224×224; this one states the same 21-row table at INFERENCE BatchNorm — frozen
running statistics at all 77 sites, one shared ε — and proves its typed SHlo graph denotes
it (mnv4FwdGraphBFullEval_faithful). That is the graph of mnv4_fwd_eval.mlir,
mnv4in_fwd_eval.mlir and mnv4in_fwd_eval_s256.mlir.
One statement, every input size. The net is stated at a binder f, the final feature side:
the input is 32f, the stem out 16f, the fused stage 8f, and the three stride-2 rows take it to
4f, 2f, f. The committed evals are f = 7 (224) and f = 8 (256, timm's test size for
mobilenetv4_conv_medium.e500_r224_in1k) — mnv4FwdChainB's own f. The ladder is written as
nested doublings (2 * (2 * f), not 4 * f) so a strided row's input side is its output side's
2 * h by the types alone.
Why no CertLayer and no resolution groups. Nothing differentiates the eval forward, so the
blocks are plain functions; and at a variable f den stays stuck, so the single rewrite chain
that times out at the training file's literal resolutions is small here.
Families by dispatch, as the render does it. A row's two depthwise positions are ifs on
s.preDWk / s.postDWk in the graph (mnv4PreDWGraphBEval, mnv4PostDWGraphBEval), exactly the
ifs uibFwdSkipB / uibFwdStridedB branch on, so one body graph covers ExtraDW, ConvNeXt-like,
FFN (and IB, which Conv-M does not use) and one theorem proves it. The table picks the family.
What it is tied to. %x + 233 parameters + 154 statistic slots = 388 inputs. The SSA names
are the eval render's: each BN's statistics are %{site}mu / %{site}var with the site the
render's mnv4Bn statP (stn, f0cn, u{p}qn, …, hn). FwdGraphTextTies checks every
block, the stem, the fused stage and the head against the render at .eval, at both f = 7 and
f = 8.
Batched k×k conv (any stride-1 extent) → inference BN → relu.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Batched stride-2 conv, SYMMETRIC padding (the stem and the fused stage) → inference BN → relu.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Batched 1×1 project → inference BN, no activation (the linear bottleneck).
Equations
- Proofs.StableHLO.mnv4ProjBEval N W b ε γ β μ v = Proofs.StableHLO.batchMap N (Proofs.bnPerChannelEvalTensor3 oc h w ε γ β μ v) ∘ Proofs.StableHLO.batchMap N (Proofs.flatConv W b)
Instances For
Batched depthwise → inference BN, no activation (timm's dw_start, the pre-DW).
Equations
- Proofs.StableHLO.mnv4DWBEval N W b ε γ β μ v = Proofs.StableHLO.batchMap N (Proofs.bnPerChannelEvalTensor3 c h w ε γ β μ v) ∘ Proofs.StableHLO.batchMap N (Proofs.depthwiseFlat W b)
Instances For
Batched depthwise → inference BN → relu (the stride-1 post-DW).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Batched stride-2 depthwise, symmetric → inference BN → relu (the strided post-DW).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A depthwise slot at inference: nothing at k = 0, a Mnv4DWEval otherwise — DWSlot's
eval twin.
Equations
Instances For
The slot's parameters at any k: the stored ones at k > 0, a zero placeholder at k = 0
that the absent slot never reads.
Instances For
One UIB block's inference parameters, typed by its table row — UibParams's eval twin:
each BN carries its frozen μ, σ² and no ε (the net shares one). The row's h appears in
no field, which is what lets one record serve every input size.
- pre : Mnv4DWEvalSlot s.ic s.preDWk
- post : Mnv4DWEvalSlot (s.ic * s.expand) s.postDWk
Instances For
Every MobileNetV4-Conv-M inference parameter, generic in the class count: the 233
parameters of Mnv4BWeights without its per-site εs, plus the 77 BN sites' μ, σ². Field
names follow the render's SSA prefixes.
- sW : Kernel4 32 3 3 3
- sb : Vec 32
- sg : Vec 32
- sbt : Vec 32
- smu : Vec 32
- sv : Vec 32
- f0cW : Kernel4 128 32 3 3
- f0cb : Vec 128
- f0cg : Vec 128
- f0cbt : Vec 128
- f0cmu : Vec 128
- f0cv : Vec 128
- f0pW : Kernel4 48 128 1 1
- f0pb : Vec 48
- f0pg : Vec 48
- f0pbt : Vec 48
- f0pmu : Vec 48
- f0pv : Vec 48
- b1 : UibEvalParams mnv4Row1
- b2 : UibEvalParams mnv4Row2
- b3 : UibEvalParams mnv4Row3
- b4 : UibEvalParams mnv4Row4
- b5 : UibEvalParams mnv4Row5
- b6 : UibEvalParams mnv4Row6
- b7 : UibEvalParams mnv4Row7
- b8 : UibEvalParams mnv4Row8
- b9 : UibEvalParams mnv4Row9
- b10 : UibEvalParams mnv4Row10
- b11 : UibEvalParams mnv4Row11
- b12 : UibEvalParams mnv4Row12
- b13 : UibEvalParams mnv4Row13
- b14 : UibEvalParams mnv4Row14
- b15 : UibEvalParams mnv4Row15
- b16 : UibEvalParams mnv4Row16
- b17 : UibEvalParams mnv4Row17
- b18 : UibEvalParams mnv4Row18
- b19 : UibEvalParams mnv4Row19
- b20 : UibEvalParams mnv4Row20
- b21 : UibEvalParams mnv4Row21
- h1W : Kernel4 960 256 1 1
- h1b : Vec 960
- h1g : Vec 960
- h1bt : Vec 960
- h1mu : Vec 960
- h1v : Vec 960
- hW : Kernel4 1280 960 1 1
- hb : Vec 1280
- hg : Vec 1280
- hbt : Vec 1280
- hmu : Vec 1280
- hv : Vec 1280
- Wd : Mat 1280 nCls
- bd : Vec nCls
Instances For
The pre-DW slot at inference: identity at k = 0, depthwise → BN otherwise.
Equations
Instances For
The stride-1 post-DW slot at inference: identity at k = 0, depthwise → BN → relu
otherwise.
Equations
Instances For
A stride-1 UIB body at inference, read off its row: pre-DW? → expand-BN-relu → post-DW? →
project-BN, at side h. The skip is added by the caller.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-2 UIB block at inference: the pre-DW slot and the expand at the input side 2h,
the post-DW carrying the stride to h (timm's dw_mid), the project at h. No skip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The fused stage at inference: stride-2 k×k conv-BN-relu, then the 1×1 project-BN.
Equations
- Proofs.StableHLO.mnv4FusedBEval N h ε Wc bc γc βc μc vc Wp bp γp βp μp vp = Proofs.StableHLO.mnv4ProjBEval N Wp bp ε γp βp μp vp ∘ Proofs.StableHLO.mnv4CbReluSBEval N Wc bc ε γc βc μc vc
Instances For
The head at inference, timm's order: 1×1 conv-BN-relu at h, GAP, conv_head 1×1
conv-BN-relu on the pooled [N, mid, 1, 1], dense — with mnv4Head's two relabellings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inference MobileNetV4-Conv-M at final feature side f,
N·(3·32f·32f) → N·nCls: stem, fused stage, the 21 table rows (the eighteen stride-1 ones
under residual), head. Every BN reads frozen statistics, so the whole net is per-example:
each stage is batchMap N of a per-example map or a pointwise map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One inference BN node, named as mnv4Bn names it at .eval: γ, β by their parameter names,
μ, σ² as %{site}mu / %{site}var.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pre-DW slot's graph: no tokens at k = 0, depthwise → BN otherwise — uibFwdSkipB's
and uibFwdStridedB's if preDWk > 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stride-1 post-DW slot's graph: no tokens at k = 0, depthwise → BN → relu otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-1 UIB body's inference graph at side h, every name read off the row.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-2 UIB block's inference graph: pre-DW slot and expand at 2h, the strided
post-DW (.depthwiseStrided, symmetric) to h, project at h.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Stem inference graph: 3×3/s2 symmetric conv → BN (stn) → relu. Generic in the widths, for
the reason mnv4StemGraphB records.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fused-stage inference graph: 3×3/s2 conv → BN (f0cn) → relu → 1×1 project → BN (f0pn).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Head inference graph, mnv4HeadGraphB's tokens with the two BNs at frozen statistics (h1n,
hn).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The MobileNetV4-Conv-M inference forward graph at final feature side f, at
mnv4FwdChainB's .eval tokens and names: mnv4_fwd_eval.mlir and mnv4in_fwd_eval.mlir
at f = 7, mnv4in_fwd_eval_s256.mlir at f = 8.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The MobileNetV4-Conv-M inference graph denotes the inference forward, at every final
feature side f. One rewrite per stage, outside-in; the eighteen skip rows each go through
mnv4SkipGraphBEval_faithful with the body theorem, so the term stays linear in the depth.