Documentation

LeanMlir.Proofs.Foundation.SmoothedLossCot

The label-smoothed loss cotangent, at a GENERAL target #

Every whole-net T3 tie in the repo pins its top-of-chain cotangent to softmax(logits) − oneHot label — the gradient of plain cross-entropy at a hard label. That is what the SGD-inline per-example renders emit, and it is not what the batched ImageNet renders emit.

ResNet34RenderB.lean composes the head cotangent from six kit ops:

%sm  = softmaxRow(logits)          %d0 = %sm − %onehot        %lsa = α · %onehot
%d1  = %d0 + %lsa                  %d2 = %d1 − α/K            %dy  = %d2 / B

so dy = (softmax(z) − t + α·t − α/K) / B, with α = 0.1 baked (the ls0 variants set it to 0) and t arriving as the graph INPUT %onehot — which under mixup or cutmix is a soft vector drawn on the host, not a one-hot. ConvNeXtRenderB and ViTRenderB compose the same six ops. This file is the cotangent lemma those ties need: at a general target and at the smoothed form.

What is proved #

What is NOT claimed #

⚠ The / B is the batch mean, and it is a convention, not a theorem here. smoothedLossCotGraph_row states the row IS (1/B)·∂softCE/∂z at that example's logits; that the sum of B such rows is the gradient of the mean loss is the linearity step, and a tie against a *dp* artifact needs the replica mean on top of it (planning/archive/proofs_tier_to_paper_nets.md 4d).

⚠ α is a free real. The committed renders bake 0.1, and the ls0 twins bake 0; both are instances. ⚠ Nothing here says t is a probability vector — only Σ t = 1 is ever used, which is what mixup's convex combination of two one-hots satisfies.

source
noncomputable def Proofs.softCE (K : ℕ) (t z : Vec K) :
ℝ

Soft-target cross-entropy −Σ_k t_k log softmax(z)_k, written as the t-weighted sum of the per-class crossEntropy. At t = oneHot label it IS crossEntropy K z label (softCE_oneHot).

Equations
Instances For
    source
    theorem Proofs.softCE_oneHot (K : ℕ) (z : Vec K) (label : Fin K) :
    softCE K (oneHot K label) z = crossEntropy K z label

    At a one-hot target, soft-target CE is the ordinary cross-entropy.

    source
    theorem Proofs.softCE_grad (K : ℕ) (t z : Vec K) (j : Fin K) :
    pdiv (fun (z' : Vec K) (x : Fin 1) => softCE K t z') z j 0 = (∑ k : Fin K, t k) * softmax K z j - t j

    The soft-target CE gradient, with NO hypothesis on t: ∂/∂z_j (−Σ_k t_k log p_k) = (Σ_k t_k)·p_j − t_j. Each summand is softmaxCE_grad; the sum comes out by pdiv_finset_sum, and each t_k factor by pdiv_mul against a constant.

    source
    noncomputable def Proofs.smoothTarget (K : ℕ) (α : ℝ) (t : Vec K) :
    Vec K

    Label smoothing: t ↦ (1−α)·t + α/K, the target the smoothed loss is against.

    Equations
    Instances For
      source
      theorem Proofs.smoothTarget_sum (K : ℕ) (hK : 0 < K) (α : ℝ) (t : Vec K) (ht : ∑ k : Fin K, t k = 1) :
      ∑ k : Fin K, smoothTarget K α t k = 1

      Smoothing preserves total mass. The one place 0 < K is needed — with K = 0 the α/K term is α/0 = 0 and the identity fails for α ≠ 0.

      source
      theorem Proofs.smoothedCE_grad (K : ℕ) (hK : 0 < K) (α : ℝ) (t z : Vec K) (ht : ∑ k : Fin K, t k = 1) (j : Fin K) :
      pdiv (fun (z' : Vec K) (x : Fin 1) => softCE K (smoothTarget K α t) z') z j 0 = softmax K z j - t j + α * t j - α / ↑K

      ⭐ The emitted expression IS the smoothed loss's gradient. ∂/∂z_j of soft-target CE at the SMOOTHED target (1−α)t + α/K equals softmax(z)_j − t_j + α·t_j − α/K, which is exactly what the render's softmaxRow → subB → scaleB → addVB → shiftB chain computes, before the batch divide.

      source
      noncomputable def Proofs.smoothedLossCotGraph (N K : ℕ) (α B : ℝ) (aStr negAK bStr logN ohN : String) (logits t : Vec (N * (1 * K))) :
      StableHLO.SHlo (N * (1 * K))

      The six-op label-smoothed cotangent chain the batched renders emit, at one row per example (m = 1, n = K) and batch N. logits is the head's output and t the graph input %onehot; α is the smoothing and B the batch divisor (the render bakes B = N).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Proofs.smoothedLossCotGraph_den (N K : ℕ) (α B : ℝ) (aStr negAK bStr logN ohN : String) (logits t : Vec (N * (1 * K))) (i : Fin (N * (1 * K))) :
        StableHLO.den (smoothedLossCotGraph N K α B aStr negAK bStr logN ohN logits t) i = (StableHLO.batchMap N (StableHLO.rowSoftmaxFlat 1 K) logits i - t i + t i * α + -(α / ↑K)) / B

        What the chain denotes, coordinatewise: (rowSoftmax(logits) − t + α·t − α/K) / B.

        source
        theorem Proofs.smoothedLossCotGraph_row (N K : ℕ) (hK : 0 < K) (α B : ℝ) (aStr negAK bStr logN ohN : String) (logits t : Vec (N * (1 * K))) (n : Fin N) (j : Fin K) (ht : ∑ k : Fin K, Mat.unflatten (StableHLO.batchSlice N (1 * K) t n) 0 k = 1) :
        StableHLO.den (smoothedLossCotGraph N K α B aStr negAK bStr logN ohN logits t) (finProdFinEquiv (n, finProdFinEquiv (0, j))) = pdiv (fun (z' : Vec K) (x : Fin 1) => softCE K (smoothTarget K α (Mat.unflatten (StableHLO.batchSlice N (1 * K) t n) 0)) z') (Mat.unflatten (StableHLO.batchSlice N (1 * K) logits n) 0) j 0 / B

        ⭐ Each row of the emitted cotangent is the smoothed loss's gradient at that example's logits, divided by the batch. Mat.unflatten splits the flat N·(1·K) activation into its N per-example rows; smoothedCE_grad supplies the gradient. The hypothesis is only that the example's target sums to 1 — a one-hot, a mixup convex combination, or any distribution.

        source
        noncomputable def Proofs.smoothedLossCotGraphDiv (N K : ℕ) (α B : ℝ) (aStr negAK bStr logN ohN : String) (logits t : Vec (N * K)) :
        StableHLO.SHlo (N * K)

        The six-op chain as ConvNeXtRenderB and ViTRenderB emit it. Those two renders spell the row softmax as batchOp expe then batchOp softmaxDiv — the per-example softmaxDiv (expe ·) pair the SGD-inline files tie (cnxLossCot_den), lifted — and run the whole chain at the plain width N·K rather than N·(1·K), so there is no row index and no rowB/unrowB cast at the head. Same six functions, different AST; smoothedLossCotGraphDiv_den says the denotation is smoothedLossCotGraph's, and smoothedLossCotGraphDiv_row is the per-example statement at batchSlice.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Proofs.smoothedLossCotGraphDiv_den (N K : ℕ) (α B : ℝ) (aStr negAK bStr logN ohN : String) (logits t : Vec (N * K)) (i : Fin (N * K)) :
          StableHLO.den (smoothedLossCotGraphDiv N K α B aStr negAK bStr logN ohN logits t) i = (StableHLO.batchMap N (softmax K) logits i - t i + t i * α + -(α / ↑K)) / B

          What the chain denotes, coordinatewise: (softmax(logits_n) − t + α·t − α/K) / B, the per-example softmax lifted by batchMap — the same function smoothedLossCotGraph_den reads off the softmaxRow spelling.

          source
          theorem Proofs.smoothedLossCotGraphDiv_row (N K : ℕ) (hK : 0 < K) (α B : ℝ) (aStr negAK bStr logN ohN : String) (logits t : Vec (N * K)) (n : Fin N) (j : Fin K) (ht : ∑ k : Fin K, StableHLO.batchSlice N K t n k = 1) :
          StableHLO.den (smoothedLossCotGraphDiv N K α B aStr negAK bStr logN ohN logits t) (finProdFinEquiv (n, j)) = pdiv (fun (z' : Vec K) (x : Fin 1) => softCE K (smoothTarget K α (StableHLO.batchSlice N K t n)) z') (StableHLO.batchSlice N K logits n) j 0 / B

          ⭐ Each example's row of the emitted cotangent is the smoothed loss's gradient at that example's logits, divided by the batch — smoothedLossCotGraph_row at the softmaxDiv spelling and the plain N·K index, where the example is batchSlice N K · n with no Mat.unflatten. The hypothesis is only that the example's target sums to 1.