MobileNetV2's data-parallel forward at SYNCHRONISED BatchNorm — replica r IS shard r #

MobileNetV2FullB.lean says the typed batch-BN graph denotes mobilenetv2ForwardBFull N w on one device. MobileNetV2RenderB's data-parallel step normalises with the GLOBAL batch's statistics at replicas > 1: every one of the 52 BatchNorm sites is the sync-BN composition — this replica's mean all-reduced, then Chan's σ²_r + (μ_r − μ)² all-reduced, packed, then bnSyncF. This file is the data-parallel twin of mobilenetv2FwdGraphBFull_faithful: that forward graph, stated as a family over the R replicas, denotes on replica r exactly batchShard r of the single-device forward at the global batch R·N.

den (mobilenetv2FwdGraphSyncFull R hR N epsStr w bf16 e r)
  = batchShard R N nCls (mobilenetv2ForwardBFull (R * N) w X) r

given that each replica's input is its shard of one global batch X. The spec does not move: the right-hand side is the committed mobilenetv2ForwardBFull, at N := R·N, and it does not move with the precision either: bf16 selects the conv and depthwise kinds at every site (.convAt / .convStridedXlaAt / .depthwiseAt / .depthwiseStridedXlaAt, as MobileNetV2FullB), bf16 := true being the kinds the *bf16 DP renders emit — mobilenetv2in_rmsdp64wxdols0eps0001bf16, the run the book reports, among them; each conv's shard step erases the switch through Bf16Erasure (Bf16Fold.denOp_convAt_id, …) and the rest of the proof is the f32 one. The *do* DP artifacts' forward — that run's — is mobilenetv2FwdGraphSyncFullDo: the same graph with replica r's dropoutB at its own mask %do between the GAP and the dense, and mobilenetv2FwdGraphSyncFullDo_shard says it denotes shard r of mobilenetv2ForwardBFullDo at the global batch and the global mask the replicas' masks are the shards of.

How it is proved #

As ResNet34SyncB.lean proves ResNet-34's: by induction on the chain, one block at a time, with the shard hypothesis ∀ r, den (e r) = batchShard R N _ X r carried from block to block.

• every conv, depthwise, GAP and dense node is a per-example lift (den_batchOp_shard), and so is the XLA-SAME strided conv and depthwise — the padding lives inside the per-example map;
• relu6 is pointwise, so it commutes with sharding (den_relu6_shard, the peer of den_relu_shard); the identity skip is den_addVB_shard;
• every BatchNorm site is bnSyncSiteLA, whose shard lemma den_bnSyncSiteLA is the sync-BN shard identity on the graph, read at the network index.

The graph reuses ResNet34SyncB's site verbatim — it is net-agnostic — and relu6's shard lemma is the kit's, so this file is MobileNetV2's six block shapes and their chain.

Names #

Parameter names are MobileNetV2FullB's (%b{k}{e,d,p}{W,g,bt}, %sW, %hW, …, the convBias := false zero-bias operands %zb{c}). A BatchNorm site with γ %b{k}dg gathers its statistics as %arsum / %armean of b{k}dgmu and b{k}dgvar, each over a [c] vector — the γ name without %, then mu / var.

What is NOT claimed here #

The backward and the parameter collectives are MobileNetV2SyncStepTieB.lean's. That the R replicas' inputs are the shards of one batch is the driver's, as in DataParallel.Sync. The rounding the bf16 kinds perform is not modelled, as f32 rounding is not: den is over ℝ at either value of the flag. The lowerer's all_reduce is trusted as every other op's lowering is.