Documentation

LeanMlir.Proofs.Nets.Small.CifarBnFold

PoC: the per-channel BatchNorm γ/β ops, proof-tied #

The per-channel-BatchNorm peer of CifarFold's conv and dense folds, used by the cifar8-BN tie (Cifar8BnStepTie), ResNet34Fold and MobileNetV2FoldPaperG.

The BN scale/shift ops. The per-channel γ/β updates use the core ops bnGammaSgd/bnBetaSgd, whose den is γ − lr·bnPerChannel_grad_gamma / β − lr·bnPerChannel_grad_beta (the certs work in the oc·m flat-spatial layout; the op's den bridges its oc·h·w activation layout via reassocFwd, exactly as the BN forward/back ops bnPerChannelF/bnPerChannelBack do — bnPerChannelTensor3 = reassocBack ∘ bnPerChannelFlat ∘ reassocFwd). The two theorems below close them via cifar_bn_render_{gamma,beta}_certified (CifarBnClose.lean) — den reduces (rfl) to each cert's LHS.

Honest residual #

Same as the non-BN fold (conv cotangents are free vars; cotangent-subgraph⇄SHlo pin; per-op pretty lexing; ℝ→Float32), plus the BN input-grad 0<ε smoothness hypothesis (inherited — γ/β grads themselves are affine and need no 0<ε).

source
theorem Proofs.CifarBnPoC.bnGamma_den {oc h w : ℕ} (gN vN epsStr lrStr cotN : String) (ε : ℝ) (γ β : Vec oc) (v c : Vec (oc * h * w)) (lr : ℝ) (idx : Fin oc) :
StableHLO.den (StableHLO.SHlo.bnGammaSgd gN vN epsStr lrStr ε γ v lr (StableHLO.SHlo.operand cotN c)) idx = γ idx - lr * ∑ j : Fin (oc * (h * w)), pdiv (fun (γ' : Vec oc) => bnPerChannelFlat oc (h * w) ε γ' β (reassocFwd oc h w v)) γ idx j * reassocFwd oc h w c j

Per-channel BN γ op = certified. The emitted bnGammaSgd, fed the BN-output cotangent c and the saved conv output v, denotes γ − lr·(certified ∂(per-channel BN)/∂γ · c) — via reassocFwd into the oc·m cert layout.

source
theorem Proofs.CifarBnPoC.bnBeta_den {oc h w : ℕ} (bN lrStr cotN : String) (ε : ℝ) (γ β : Vec oc) (v c : Vec (oc * h * w)) (lr : ℝ) (idx : Fin oc) :
StableHLO.den (StableHLO.SHlo.bnBetaSgd bN lrStr β lr (StableHLO.SHlo.operand cotN c)) idx = β idx - lr * ∑ j : Fin (oc * (h * w)), pdiv (fun (β' : Vec oc) => bnPerChannelFlat oc (h * w) ε γ β' (reassocFwd oc h w v)) β idx j * reassocFwd oc h w c j

Per-channel BN β op = certified. Likewise β − lr·(certified ∂BN/∂β · c).

source
def Proofs.CifarBnPoC.BnSgdPairTied {oc h w : ℕ} (gN vN bN epsStr lrStr cotN : String) (ε : ℝ) (γ β : Vec oc) (v c : Vec (oc * h * w)) (lr : ℝ) :
Prop

The emitted bnGammaSgd and bnBetaSgd ops of one per-channel BN layer, fed its BN-output cotangent c at the saved conv output v, are the certified SGD steps on γ and β — the statements of bnGamma_den and bnBeta_den under ∀. The per-example peer of EnetPoC.BnSgdPairTiedB.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Proofs.CifarBnPoC.bnSgdPairTied_holds {oc h w : ℕ} (gN vN bN epsStr lrStr cotN : String) (ε : ℝ) (γ β : Vec oc) (v c : Vec (oc * h * w)) (lr : ℝ) :
    BnSgdPairTied gN vN bN epsStr lrStr cotN ε γ β v c lr