Backward-graph faithfulness for the batched MobileNetV2 inverted-residual block #
The MobileNetV2 peer of EfficientNetBackB0.lean: a backward StableHLO graph
that denotes the proven VJP of the batched MobileNetV2 inverted-residual block —
project ∘ depthwise-bn-relu6 ∘ expand-bn-relu6 with the linear-bottleneck skip.
The block is the EfficientNet MBConv body minus the squeeze-excite stage, with
relu6 in place of swish and the same linear-bottleneck projB (1×1 conv →
bn, no activation). The stages come from Batched.StageLayers (cbrB, dwbrB,
dwbrBstrided and their CertLayers cbrLayer, dwbrLayer, dwbrStridedLayer, projLayer)
and Batched.Stages (projB); the residual fan-in's backward graph is
residualBackGraph (Batched.BackLinks). The project stage and the fan-in need no
smoothness hypothesis.
The relu6 wrinkle #
Unlike swish (smooth everywhere, GLOBAL swishHasVJP), relu6 has a TWO-SIDED kink
(at 0 and at 6), so its VJP is only the pointwise relu6HasVJPAt, conditioned
on the smoothness hypothesis ∀ k, x k ≠ 0 ∧ x k ≠ 6 at the pre-activation. Its
per-op backward token is .selectMid (the mask if 0<x<6 then dy else 0), whose
denotation faithfulness is the already-proven (rfl) StableHLO.selectMid_faithful.
Because relu6's VJP is _at, the whole MobileNetV2 stage/body VJP and its backward-
graph faithfulness are stated in the _at / hypothesis-threaded form (via
vjpCompAt, lifting the global bnBatchLA/batchMap/conv/depthwise VJPs through
HasVJP.toHasVJPAt), NOT the EfficientNet global form. The relu6 smoothness
hypothesis at the pre-relu6 activation bnBatchLA(…)(batchMap(conv)(x)) is threaded
through; the bn/conv/depthwise pieces stay activation-independent (linear) or global.
Structure #
mnv2BodyLayer/mnv2DownBodyLayer— the stride-1 and stride-2 bodies asCertLayers, composed from the stage layers withCertLayer.comp; each body VJP, differentiability lemma and graph_faithfulbelow is that layer'svjp/diff/faithful.mnv2BodyBHasVJPAt— the SE-less bodyprojB ∘ dwbrB ∘ cbrBat the relu6 smoothness families, with its backward graphmnv2BodyBackBatchedGraph+…_faithful. It takesicandocseparately, so it also covers the stride-1 bodies withic ≠ oc(b11, 64 → 96, andb17, 160 → 320;MobileNetV2FullB.lean'smnv2ExpOnlyB).mnv2ResidBlockBackBatchedGraph_faithful— the whole batched MobileNetV2 inverted-residual block backward graph (body + identity skip) denotes the provenresidualHasVJPAtof the SE-less body. Mirrors the EfficientNetmbResidBlockBackBatchedGraph_faithfulwithout theseBfactor, threaded through the relu6 smoothness hypotheses;CertLayer.residual mnv2BodyLayer'sfaithful.
The SE-less body as a CertLayer: cbrLayer ; dwbrLayer ; projLayer, left-nested so its
fwd is projB ∘ (dwbrB ∘ cbrB), the association the stated types use. Its ok is the
expand and depthwise relu6 clauses; projLayer contributes True.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched MobileNetV2 inverted-residual body's VJP at a smooth point —
projB ∘ dwbrB ∘ cbrB (the EfficientNet MBConv body MINUS seB, with relu6
for swish), mnv2BodyLayer's VJP.
h_se is the expand relu6 smoothness (at the cbrB pre-relu6 activation);
h_sd is the depthwise relu6 smoothness (at the dwbrB pre-relu6 activation,
fed the cbrB output).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched MobileNetV2 body backward graph: the three stage graphs chained at
their cumulative forward activations (cbrB⁻¹ ∘ dwbrB⁻¹ ∘ projB⁻¹).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The downsample body as a CertLayer: cbrLayer at 2h × 2w, then dwbrStridedLayer and
projLayer at h × w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched MobileNetV2 DOWNSAMPLE inverted-residual body's VJP at a smooth
point — projB ∘ dwbrBstrided ∘ cbrB, the stride-2 analogue of
mnv2BodyBHasVJPAt (swaps the stride-1 dwbrB depthwise stage for the
STRIDED dwbrBstrided). The expand cbrB runs at the larger 2h×2w (1×1
conv keeps spatial), the strided depthwise then halves spatial to h×w; project
runs at h×w. NO residual (spatial/channels change), so this is the body alone:
mnv2DownBodyLayer's VJP.
h_se is the expand relu6 smoothness (at the cbrB pre-relu6 activation, at
2h×2w); h_sd is the strided-depthwise relu6 smoothness (at the dwbrBstrided
pre-relu6 activation, fed the cbrB output).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The batched MobileNetV2 downsample body backward graph: the three stage graphs
chained at their cumulative forward activations
(cbrB⁻¹ ∘ dwbrBstrided⁻¹ ∘ projB⁻¹). Stride-2 analogue of
mnv2BodyBackBatchedGraph (strided depthwise stage graph, no residual).
Equations
- One or more equations did not get rendered due to their size.
Instances For
CAPSTONE — the batched MobileNetV2 DOWNSAMPLE inverted-residual body: backward
graph ↔ the proven mnv2DownBodyBHasVJPAt. The three batched stage backward
graphs (cbrB/dwbrBstrided/projB) chained at their forward activations,
proven equal to the downsample-body VJP. The stride-2 analogue of
mnv2BodyBackBatchedGraph_faithful (no residual skip — the downsample block
changes spatial/channels, so the body alone is the block), threaded through the
two relu6 smoothness hypotheses (relu6's VJP is only _at). The MobileNetV2
relu6 peer of the EfficientNet mbDownBodyBackBatchedGraph_faithful; it is
mnv2DownBodyLayer's faithful.
The whole batched MobileNetV2 inverted-residual block backward graph (body + identity skip).
Equations
- One or more equations did not get rendered due to their size.
Instances For
CAPSTONE — the whole batched MobileNetV2 inverted-residual block: backward
graph ↔ the proven VJP. The three batched stage backward graphs
(cbrB/dwbrB/projB) chained at their forward activations + the identity
skip, proven equal to residualHasVJPAt of the SE-less body
projB ∘ dwbrB ∘ cbrB. The MobileNetV2 analogue of the EfficientNet
mbResidBlockBackBatchedGraph_faithful, without the seB factor, threaded
through the relu6 smoothness hypotheses (relu6's VJP is only _at).
It is CertLayer.residual mnv2BodyLayer's faithful: the residual fan-in backward
(body cotangent + the identity skip's verbatim %dy).