Documentation

LeanMlir.Proofs.Training.SgdDescent.MlpBias

Descent on the dense biases — the MLP rungs' bias columns #

SgdDescent.Linear and SgdDescent.Mlp state one-step descent for each dense WEIGHT matrix of the Chapter-2 MLP (dense → relu → dense → relu → dense). This file states it for each dense BIAS:

Each is its weight rung with the layer input replaced by the constant 1: the bias moves its pre-activation by exactly the step (dense_bias_drift, no input bound a), so the weight rung's a becomes 1 in the margins and the constants. The segment-Lipschitz step is MlpSlot.loss_grad_lipschitz at a bias map (σ = ρ = 1 for the hidden layer, σ = w₁, ρ = d₂·w₁ for the input layer), the gradient's row the channel indicator (pdiv_dense_b).

The rungs are generic in the layer's input, so the Chapter-3 CNN's dense-head biases are literal instances at the pooled activation, as its head weights are of the weight rungs (SgdDescent.Cnn). The oracle accuracy, the margins, the small-step and the two dominance conditions remain hypotheses; no binary32 twin is stated for the biases.

source
theorem Proofs.dense_bias_diff {m n : ℕ} (W : Mat m n) (x : Vec m) (b e : Vec n) (k : Fin n) :
dense W (b + e) x k - dense W b x k = e k

A bias step moves each pre-activation entry by exactly its own coordinate.

source
theorem Proofs.dense_bias_drift {m n : ℕ} (W : Mat m n) (x : Vec m) (b e : Vec n) (k : Fin n) :
|dense W (b + e) x k - dense W b x k| ≤ 1 * ∑ idx : Fin n, |e idx|

…so by at most the step's ℓ1 mass.

source
theorem Proofs.dense_bias_drift_sum {m n : ℕ} (W : Mat m n) (x : Vec m) (b e : Vec n) :
∑ k : Fin n, |dense W (b + e) x k - dense W b x k| ≤ 1 * ∑ idx : Fin n, |e idx|

…and the pre-activation's total ℓ1 drift is the step's ℓ1 mass.

source
theorem Proofs.gradAt_bias_eq_pdiv {m n : ℕ} (W : Mat m n) (x : Vec m) (G : Vec n → Vec 1) (b : Vec n) (hG : DifferentiableAt ℝ G (dense W b x)) (j : Fin n) :
gradAt (fun (b' : Vec n) => G (dense W b' x) 0) b j = pdiv G (dense W b x) j 0

The loss gradient in a bias is the loss's input gradient at that layer's pre-activation: the bias Jacobian is the identity (pdiv_dense_b).

source
noncomputable def Proofs.linearBiasLoss {m n : ℕ} (W : Mat m n) (x : Vec m) (label : Fin n) :
Vec n → ℝ

The linear classifier's loss as a function of its bias.

Equations
Instances For
    source
    theorem Proofs.linear_bias_loss_gradAt {m n : ℕ} (W : Mat m n) (x : Vec m) (label : Fin n) (b : Vec n) (j : Fin n) :
    gradAt (linearBiasLoss W x label) b j = softmax n (dense W b x) j - oneHot n label j

    Closed form of the output-bias loss gradient: ∂L/∂bⱼ = softmax(z)ⱼ − onehotⱼ.

    source
    theorem Proofs.linear_bias_loss_grad_lipschitz {m n : ℕ} (W : Mat m n) (x : Vec m) (label : Fin n) {D : ℝ} (v d : Vec n) (hd : ∑ idx : Fin n, |d idx| ≤ D) (hsmall : 2 * D < 1) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (j : Fin n) :
    |gradAt (linearBiasLoss W x label) (v + t • d) j - gradAt (linearBiasLoss W x label) v j| ≤ 2 / (1 - 2 * D) * (t * D)

    Segment-Lipschitz gradient for the output-bias loss: under 2D < 1 the gradient entries drift by at most (2/(1−2D))·(t·D) along [v, v+d].

    source
    theorem Proofs.linear_bias_sgd_descends {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (label : Fin n) (gh : Vec n) {lr η : ℝ} (hlr : 0 ≤ lr) (hη : 0 ≤ η) (hgh : ∀ (idx : Fin n), |gh idx - gradAt (linearBiasLoss W x label) b idx| ≤ η) (hsmall : 2 * stepRadius (linearBiasLoss W x label) b lr η < 1) (h1 : lr * η * ∑ idx : Fin n, |gradAt (linearBiasLoss W x label) b idx| ≤ (lr * ∑ idx : Fin n, gradAt (linearBiasLoss W x label) b idx ^ 2) / 4) (h2 : 2 / (1 - 2 * stepRadius (linearBiasLoss W x label) b lr η) * stepRadius (linearBiasLoss W x label) b lr η ^ 2 ≤ (lr * ∑ idx : Fin n, gradAt (linearBiasLoss W x label) b idx ^ 2) / 4) :
    linearBiasLoss W x label (b - lr • gh) ≤ linearBiasLoss W x label b - (lr * ∑ idx : Fin n, gradAt (linearBiasLoss W x label) b idx ^ 2) / 2

    One inexact SGD step on the output bias decreases one example's cross-entropy loss — linear_sgd_descends with the input replaced by 1: example (x, label), the bias moving, the weights fixed, constant C = 2/(1−2D) at step radius D = lr·(‖∇L‖₁ + n·η). The oracle accuracy, the small-step and the two dominance conditions remain hypotheses.

    source
    noncomputable def Proofs.mlpHiddenBiasLoss {d₁ d₂ d₃ : ℕ} (W₁ : Mat d₁ d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (a₀ : Vec d₁) (label : Fin d₃) :
    Vec d₂ → ℝ

    The MLP's loss as a function of the hidden bias b₁.

    Equations
    Instances For
      source
      theorem Proofs.mlp_hidden_bias_loss_differentiableAt {d₁ d₂ d₃ : ℕ} (W₁ : Mat d₁ d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (a₀ : Vec d₁) (label : Fin d₃) (b : Vec d₂) (hz : ∀ (k : Fin d₂), dense W₁ b a₀ k ≠ 0) :
      DifferentiableAt ℝ (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b

      The hidden-bias loss is differentiable wherever the hidden pre-activation is off the kinks.

      source
      theorem Proofs.mlp_hidden_bias_loss_gradAt {d₁ d₂ d₃ : ℕ} (W₁ : Mat d₁ d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (a₀ : Vec d₁) (label : Fin d₃) (b : Vec d₂) (hz : ∀ (k : Fin d₂), dense W₁ b a₀ k ≠ 0) (j : Fin d₂) :
      gradAt (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b j = (if dense W₁ b a₀ j > 0 then 1 else 0) * ∑ k : Fin d₃, W₂ j k * (softmax d₃ (dense W₂ b₂ (relu d₂ (dense W₁ b a₀))) k - oneHot d₃ label k)

      Closed form of the hidden-bias loss gradient at an off-kink point: ∂L/∂b₁ⱼ = relu'(z₁ⱼ)·∑ₖ W₂ⱼₖ·(softmax − onehot)ₖ.

      source
      theorem Proofs.mlp_hidden_bias_loss_grad_lipschitz {d₁ d₂ d₃ : ℕ} (W₁ : Mat d₁ d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (a₀ : Vec d₁) (label : Fin d₃) {w₂ D : ℝ} (hw₂ : 0 ≤ w₂) (hW₂ : ∀ (j : Fin d₂) (k : Fin d₃), |W₂ j k| ≤ w₂) (v d : Vec d₂) (hd : ∑ idx : Fin d₂, |d idx| ≤ D) (hmargin : ∀ (j : Fin d₂), D < |dense W₁ v a₀ j|) (hsmall : 2 * (w₂ * D) < 1) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (j : Fin d₂) :
      |gradAt (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) (v + t • d) j - gradAt (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) v j| ≤ 2 * ↑d₃ * w₂ ^ 2 / (1 - 2 * (w₂ * D)) * (t * D)

      Segment-Lipschitz gradient for the hidden-bias loss: MlpSlot.loss_grad_lipschitz at the bias map, σ = ρ = 1, the row the channel indicator. Constant 2·d₃·w₂²/(1−2·w₂·D).

      source
      theorem Proofs.mlp_hidden_bias_sgd_descends {d₁ d₂ d₃ : ℕ} (W₁ : Mat d₁ d₂) (b₁ : Vec d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (a₀ : Vec d₁) (label : Fin d₃) (gh : Vec d₂) {lr η w₂ : ℝ} (hw₂ : 0 ≤ w₂) (hW₂ : ∀ (j : Fin d₂) (k : Fin d₃), |W₂ j k| ≤ w₂) (hlr : 0 ≤ lr) (hη : 0 ≤ η) (hgh : ∀ (idx : Fin d₂), |gh idx - gradAt (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b₁ idx| ≤ η) (hmargin : ∀ (j : Fin d₂), stepRadius (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b₁ lr η < |dense W₁ b₁ a₀ j|) (hsmall : 2 * (w₂ * stepRadius (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b₁ lr η) < 1) (h1 : lr * η * ∑ idx : Fin d₂, |gradAt (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b₁ idx| ≤ (lr * ∑ idx : Fin d₂, gradAt (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b₁ idx ^ 2) / 4) (h2 : 2 * ↑d₃ * w₂ ^ 2 / (1 - 2 * (w₂ * stepRadius (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b₁ lr η)) * stepRadius (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b₁ lr η ^ 2 ≤ (lr * ∑ idx : Fin d₂, gradAt (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b₁ idx ^ 2) / 4) :
      mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label (b₁ - lr • gh) ≤ mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label b₁ - (lr * ∑ idx : Fin d₂, gradAt (mlpHiddenBiasLoss W₁ W₂ b₂ a₀ label) b₁ idx ^ 2) / 2

      One inexact SGD step on the MLP's hidden bias decreases one example's cross-entropy loss — mlp_hidden_sgd_descends with the layer input replaced by 1: the margin D < |z₁ⱼ| at the step radius D = lr·(‖∇L‖₁ + d₂·η) freezes the hidden mask, constant C = 2·d₃·w₂²/(1−2·w₂·D).

      source
      noncomputable def Proofs.mlpInputBiasLoss {d₀ d₁ d₂ d₃ : ℕ} (W₀ : Mat d₀ d₁) (W₁ : Mat d₁ d₂) (b₁ : Vec d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (x : Vec d₀) (label : Fin d₃) :
      Vec d₁ → ℝ

      The MLP's loss as a function of the input-layer bias b₀.

      Equations
      Instances For
        source
        theorem Proofs.mlp_input_bias_loss_differentiableAt {d₀ d₁ d₂ d₃ : ℕ} (W₀ : Mat d₀ d₁) (W₁ : Mat d₁ d₂) (b₁ : Vec d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (x : Vec d₀) (label : Fin d₃) (b : Vec d₁) (hz0 : ∀ (k : Fin d₁), dense W₀ b x k ≠ 0) (hz1 : ∀ (k : Fin d₂), dense W₁ b₁ (relu d₁ (dense W₀ b x)) k ≠ 0) :
        DifferentiableAt ℝ (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b

        The input-bias loss is differentiable wherever both pre-activations are off the kinks.

        source
        theorem Proofs.mlp_input_bias_loss_gradAt {d₀ d₁ d₂ d₃ : ℕ} (W₀ : Mat d₀ d₁) (W₁ : Mat d₁ d₂) (b₁ : Vec d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (x : Vec d₀) (label : Fin d₃) (b : Vec d₁) (hz0 : ∀ (k : Fin d₁), dense W₀ b x k ≠ 0) (hz1 : ∀ (k : Fin d₂), dense W₁ b₁ (relu d₁ (dense W₀ b x)) k ≠ 0) (j : Fin d₁) :
        gradAt (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b j = (if dense W₀ b x j > 0 then 1 else 0) * ∑ l : Fin d₂, W₁ j l * ((if dense W₁ b₁ (relu d₁ (dense W₀ b x)) l > 0 then 1 else 0) * ∑ k : Fin d₃, W₂ l k * (softmax d₃ (dense W₂ b₂ (relu d₂ (dense W₁ b₁ (relu d₁ (dense W₀ b x))))) k - oneHot d₃ label k))

        Closed form of the input-bias loss gradient at a two-margin point: ∂L/∂b₀ⱼ = relu'(z₀ⱼ)·∑ₗ W₁ⱼₗ·relu'(z₁ₗ)·∑ₖ W₂ₗₖ·(softmax − onehot)ₖ.

        source
        theorem Proofs.mlp_input_bias_mid_drift {d₀ d₁ d₂ : ℕ} (W₀ : Mat d₀ d₁) (W₁ : Mat d₁ d₂) (b₁ : Vec d₂) (x : Vec d₀) {w₁ : ℝ} (hw₁ : 0 ≤ w₁) (hW₁ : ∀ (j : Fin d₁) (l : Fin d₂), |W₁ j l| ≤ w₁) (v e : Vec d₁) (l : Fin d₂) :
        |dense W₁ b₁ (relu d₁ (dense W₀ (v + e) x)) l - dense W₁ b₁ (relu d₁ (dense W₀ v x)) l| ≤ w₁ * ∑ idx : Fin d₁, |e idx|

        The middle pre-activation moves by at most w₁·‖e‖₁ per entry under a step e of the input bias — one dense crossing after a 1-Lipschitz ReLU.

        source
        theorem Proofs.mlp_input_bias_loss_grad_lipschitz {d₀ d₁ d₂ d₃ : ℕ} (W₀ : Mat d₀ d₁) (W₁ : Mat d₁ d₂) (b₁ : Vec d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (x : Vec d₀) (label : Fin d₃) {w₁ w₂ D : ℝ} (hw₁ : 0 ≤ w₁) (hW₁ : ∀ (j : Fin d₁) (l : Fin d₂), |W₁ j l| ≤ w₁) (hw₂ : 0 ≤ w₂) (hW₂ : ∀ (l : Fin d₂) (k : Fin d₃), |W₂ l k| ≤ w₂) (v d : Vec d₁) (hd : ∑ idx : Fin d₁, |d idx| ≤ D) (hmargin0 : ∀ (j : Fin d₁), D < |dense W₀ v x j|) (hmargin1 : ∀ (l : Fin d₂), w₁ * D < |dense W₁ b₁ (relu d₁ (dense W₀ v x)) l|) (hsmall : 2 * (w₂ * (↑d₂ * (w₁ * D))) < 1) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (j : Fin d₁) :
        |gradAt (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) (v + t • d) j - gradAt (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) v j| ≤ 2 * ↑d₃ * ↑d₂ ^ 2 * w₁ ^ 2 * w₂ ^ 2 / (1 - 2 * (w₂ * (↑d₂ * (w₁ * D)))) * (t * D)

        Segment-Lipschitz gradient for the input-bias loss: MlpSlot.loss_grad_lipschitz at the middle pre-activation, σ = w₁, ρ = d₂·w₁, the row relu₀'s frozen mask times W₁'s row. Constant 2·d₃·d₂²·w₁²·w₂²/(1−2·w₂·d₂·w₁·D).

        source
        theorem Proofs.mlp_input_bias_sgd_descends {d₀ d₁ d₂ d₃ : ℕ} (W₀ : Mat d₀ d₁) (b₀ : Vec d₁) (W₁ : Mat d₁ d₂) (b₁ : Vec d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (x : Vec d₀) (label : Fin d₃) (gh : Vec d₁) {lr η w₁ w₂ : ℝ} (hw₁ : 0 ≤ w₁) (hW₁ : ∀ (j : Fin d₁) (l : Fin d₂), |W₁ j l| ≤ w₁) (hw₂ : 0 ≤ w₂) (hW₂ : ∀ (l : Fin d₂) (k : Fin d₃), |W₂ l k| ≤ w₂) (hlr : 0 ≤ lr) (hη : 0 ≤ η) (hgh : ∀ (idx : Fin d₁), |gh idx - gradAt (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ idx| ≤ η) (hmargin0 : ∀ (j : Fin d₁), stepRadius (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ lr η < |dense W₀ b₀ x j|) (hmargin1 : ∀ (l : Fin d₂), w₁ * stepRadius (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ lr η < |dense W₁ b₁ (relu d₁ (dense W₀ b₀ x)) l|) (hsmall : 2 * (w₂ * (↑d₂ * (w₁ * stepRadius (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ lr η))) < 1) (h1 : lr * η * ∑ idx : Fin d₁, |gradAt (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ idx| ≤ (lr * ∑ idx : Fin d₁, gradAt (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ idx ^ 2) / 4) (h2 : 2 * ↑d₃ * ↑d₂ ^ 2 * w₁ ^ 2 * w₂ ^ 2 / (1 - 2 * (w₂ * (↑d₂ * (w₁ * stepRadius (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ lr η)))) * stepRadius (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ lr η ^ 2 ≤ (lr * ∑ idx : Fin d₁, gradAt (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ idx ^ 2) / 4) :
        mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label (b₀ - lr • gh) ≤ mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label b₀ - (lr * ∑ idx : Fin d₁, gradAt (mlpInputBiasLoss W₀ W₁ b₁ W₂ b₂ x label) b₀ idx ^ 2) / 2

        One inexact SGD step on the MLP's input bias decreases one example's cross-entropy loss — mlp_input_sgd_descends with the layer input replaced by 1: the margins D < |z₀ⱼ| and w₁·D < |z₁ₗ| at the step radius D = lr·(‖∇L‖₁ + d₁·η) freeze both masks, constant C = 2·d₃·d₂²·w₁²·w₂²/(1−2·w₂·d₂·w₁·D). With this and the output and hidden bias rungs, each dense bias of the MLP has a single-layer, single-example descent statement.