Documentation

LeanMlir.Proofs.Foundation.SgdNodes

The per-example fused-SGD nodes — one *_den per op kind, shared by every per-example chain #

The per-example train steps (the MNIST / CIFAR chapter nets, and the per-example tiers of ResNet-34, MobileNetV2, ConvNeXt and ViT) emit fused θ − lr·∂Loss/∂θ ops. Each lemma here says one such op denotes the certified SGD step at an arbitrary cotangent, so a net's fold is these at its layers. The batched, un-fused peers are in GradNodesB.

oplemmanamespace
dense weight / bias (weightSgd, biasSgd)denseW_den, denseB_denCifar8PoC
conv weight / bias (convWeightSgd, convBiasSgd)convW_den, convB_denCifarPoC
per-channel BN γ / β (bnGammaSgd, bnBetaSgd), and the pair as one clausebnGamma_den, bnBeta_den, BnSgdPairTiedCifarBnPoC

Namespaces are the net that first needed each op, kept so that every citation keeps its name.

source
theorem Proofs.Cifar8PoC.denseW_den {m n : ℕ} (aN wN lrStr cotN : String) (a : Vec m) (W : Mat m n) (b c : Vec n) (lr : ℝ) (i : Fin m) (j : Fin n) :
StableHLO.den (StableHLO.SHlo.weightSgd aN wN lrStr a W lr (StableHLO.SHlo.operand cotN c)) (finProdFinEquiv (i, j)) = W i j - lr * ∑ k : Fin n, pdiv (fun (v : Vec (m * n)) => dense (Mat.unflatten v) b a) W.flatten (finProdFinEquiv (i, j)) k * c k

Any emitted dense weight op = certified. Generic in the layer dims, the activation a, bias b and cotangent c: den (weightSgd a W (.operand _ c)) = W − lr·(certified ∂dense/∂W · c). Every small net's dense layers are instances.

source
theorem Proofs.Cifar8PoC.denseB_den {m n : ℕ} (bN lrStr cotN : String) (W : Mat m n) (a : Vec m) (b c : Vec n) (lr : ℝ) (i : Fin n) :
StableHLO.den (StableHLO.SHlo.biasSgd bN lrStr b lr (StableHLO.SHlo.operand cotN c)) i = b i - lr * ∑ j : Fin n, pdiv (fun (b' : Vec n) => dense W b' a) b i j * c j

Any emitted dense bias op = certified. Generic peer of denseW_den.

source
theorem Proofs.CifarPoC.convW_den {ic oc h w kH kW : ℕ} (xN wN lrStr cotN : String) (b : Vec oc) (x : Tensor3 ic h w) (W : Kernel4 oc ic kH kW) (c : Vec (oc * h * w)) (lr : ℝ) (idx : Fin (oc * ic * kH * kW)) :
StableHLO.den (StableHLO.SHlo.convWeightSgd xN wN lrStr b x W lr (StableHLO.SHlo.operand cotN c)) idx = W.flatten idx - lr * ∑ j : Fin (oc * h * w), pdiv (fun (v' : Vec (oc * ic * kH * kW)) => (conv2d (Kernel4.unflatten v') b x).flatten) W.flatten idx j * c j

Any emitted conv weight op = certified. Generic in the conv dims and the cotangent c: the convWeightSgd op denotes flatten W − lr·(certified ∂conv/∂W · c). Instantiated at each layer's (b,x,W,c) it certifies W₁…W₄.

source
theorem Proofs.CifarPoC.convB_den {ic oc h w kH kW : ℕ} (bN lrStr cotN : String) (W : Kernel4 oc ic kH kW) (x : Tensor3 ic h w) (b : Vec oc) (c : Vec (oc * h * w)) (lr : ℝ) (o : Fin oc) :
StableHLO.den (StableHLO.SHlo.convBiasSgd bN lrStr W x b lr (StableHLO.SHlo.operand cotN c)) o = b o - lr * ∑ j : Fin (oc * h * w), pdiv (fun (b' : Vec oc) => (conv2d W b' x).flatten) b o j * c j

Any emitted conv bias op = certified. Generic peer of convW_den.

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