Documentation

LeanMlir.Proofs.Nets.Small.LinearParamGrad

The linear classifier — both parameter gradient nodes ARE the loss's derivative #

LinearFold ties the Chapter-1 train step's two SGD updates to the certified per-layer Jacobian contracted with the emitted loss cotangent. Here that contraction, as the un-fused weightGrad / biasGrad node, is the gradient of the loss in the parameter: linear_net_lossGrad for any loss L of the logits with gradient g there, linear_net_lossGrad_CE at the softmax cross-entropy the render emits, with g the emitted loss cotangent. The fused weightSgd / biasSgd ops are θ − lr· these nodes (SmallParamGrad.weightSgd_eq_grad, SmallParamGrad.biasSgd_eq_grad).

Scope. One example (the emitted module batch-contracts; den is per-example).

source
def Proofs.LinFold.LinNetLossTied {m n : ℕ} (aN cotN : String) (W : Mat m n) (b : Vec n) (x : Vec m) (L : Vec n → Vec 1) (g : Vec n) :
Prop

Both linear-classifier parameter nodes are the gradient of L in that parameter, at the cotangent g the emitted chain starts from.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Proofs.LinFold.linear_net_lossGrad {m n : ℕ} (aN cotN : String) (W : Mat m n) (b : Vec n) (x : Vec m) {L : Vec n → Vec 1} {g : Vec n} (hL : HasGradAt L (mnistLinear W b x) g) :
    LinNetLossTied aN cotN W b x L g

    Every linear-classifier parameter node is the gradient of L whenever g is L's gradient at the logits. No smoothness hypothesis: the net is affine.

    source
    theorem Proofs.LinFold.linear_net_lossGrad_CE {m n : ℕ} (aN cotN nlogN ohN : String) (W : Mat m n) (b : Vec n) (x : Vec m) (label : Fin n) :
    LinNetLossTied aN cotN W b x (fun (z : Vec n) (x : Fin 1) => crossEntropy n z label) (StableHLO.den ((StableHLO.SHlo.operand nlogN (mnistLinear W b x)).expe.softmaxDiv.sub (StableHLO.SHlo.operand ohN (oneHot n label))))

    The artifact's loss: both nodes are the gradient of the softmax cross-entropy at label, g the emitted loss cotangent.