Documentation

LeanMlir.Proofs.Training.SgdDescent.Cifar

CIFAR-8 last-conv SGD descent #

Does the segment-Lipschitz SGD-descent argument (proven for the MNIST CNN, SgdDescent.Cnn) reach a CIFAR net? At the last conv layer, yes.

CIFAR-8's tail — its last conv W₈ (c4→c4) → relu → maxpool → three denses → CE — is byte-for-byte the program cnn_conv2_sgd_descends proves descent for. So descent at the LAST conv layer is an instance of the MNIST lemma at the frozen earlier-layer features, with the same hypotheses (oracle accuracy, the relu and post-ReLU pool margins, small-step and dominance conditions) stated at x₁. Made rigorous in two steps:

Scope. Descent through the depth of all eight conv layers is not proved here. cnn_conv2_sgd_descends's small-step condition hsmall is a PRODUCT of the per-layer operator-norm factors (the three dense bounds × spatial); each additional conv layer would multiply another (spatial · weight-bound) factor into that product, so the admissible lr shrinks geometrically with depth.

source
noncomputable def Proofs.cifar8Head {c4 h w d1 nClasses : ℕ} (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) :
Vec (c4 * (2 * h) * (2 * w)) → Vec nClasses

The CIFAR-8 classifier head (everything after the last conv's relu): maxpool → 3 denses.

Equations
Instances For
    source
    noncomputable def Proofs.cifar8Prefix7 {ic c1 c2 c3 c4 h w kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) :
    Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w))))) → Vec (c4 * (2 * h) * (2 * w))

    The CIFAR-8 first-7-conv feature extractor (everything before the last conv W₈).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Proofs.cifarCnn8Forward_factor {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) :
      cifarCnn8Forward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ W₈ b₈ W₉ b₉ Wa ba Wb bb = cifar8Head W₉ b₉ Wa ba Wb bb ∘ (relu (c4 * (2 * h) * (2 * w)) ∘ flatConv W₈ b₈) ∘ cifar8Prefix7 W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇

      CIFAR-8 factors at the last conv — cifarCnn8Forward = head ∘ (relu ∘ flatConv W₈) ∘ prefix7. Pure rfl (same ∘-chain, regrouped; Function.comp is definitionally associative).

      source
      noncomputable def Proofs.cifar8LastConvLoss {c4 h w d1 nClasses kH kW : ℕ} (b₈ : Vec c4) (x₁ : Tensor3 c4 (2 * h) (2 * w)) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (label : Fin nClasses) :
      Vec (c4 * c4 * kH * kW) → ℝ

      The loss as a function of the flattened last-conv kernel.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Proofs.cifar8_lastConv_sgd_descends {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (image : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) (x₁ : Tensor3 c4 (2 * h) (2 * w)) (label : Fin nClasses) (gh : Vec (c4 * c4 * kH * kW)) (hx₁ : x₁ = Tensor3.unflatten (cifar8Prefix7 W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ image)) (hc4 : 0 < c4) (hh : 0 < h) (hw : 0 < w) {lr η a w₉ wa wb : ℝ} (ha : 0 ≤ a) (hx : ∀ (cc : Fin c4) (i : Fin (2 * h)) (j : Fin (2 * w)), |x₁ cc i j| ≤ a) (hw₉ : 0 ≤ w₉) (hW₉ : ∀ (i : Fin (c4 * h * w)) (j : Fin d1), |W₉ i j| ≤ w₉) (hwa : 0 ≤ wa) (hWa : ∀ (i j : Fin d1), |Wa i j| ≤ wa) (hwb : 0 ≤ wb) (hWb : ∀ (i : Fin d1) (j : Fin nClasses), |Wb i j| ≤ wb) (hlr : 0 ≤ lr) (hη : 0 ≤ η) (hgh : ∀ (idx : Fin (c4 * c4 * kH * kW)), |gh idx - gradAt (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten idx| ≤ η) (hm2 : ∀ (k : Fin (c4 * (2 * h) * (2 * w))), a * stepRadius (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten lr η < |(conv2d W₈ b₈ x₁).flatten k|) (hmq : MaxPool2MarginQ (a * stepRadius (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten lr η) (Tensor3.unflatten (relu (c4 * (2 * h) * (2 * w)) (conv2d W₈ b₈ x₁).flatten))) (hm3 : ∀ (l : Fin d1), w₉ * (↑(2 * h * (2 * w)) * (a * stepRadius (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten lr η)) < |dense W₉ b₉ (maxPoolFlat c4 h w (relu (c4 * (2 * h) * (2 * w)) (conv2d W₈ b₈ x₁).flatten)) l|) (hm4 : ∀ (q : Fin d1), wa * (↑d1 * (w₉ * (↑(2 * h * (2 * w)) * (a * stepRadius (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten lr η)))) < |dense Wa ba (relu d1 (dense W₉ b₉ (maxPoolFlat c4 h w (relu (c4 * (2 * h) * (2 * w)) (conv2d W₈ b₈ x₁).flatten)))) q|) (hsmall : 2 * (wb * (↑d1 * (wa * (↑d1 * (w₉ * (↑(2 * h * (2 * w)) * (a * stepRadius (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten lr η))))))) < 1) (h1 : lr * η * ∑ idx : Fin (c4 * c4 * kH * kW), |gradAt (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten idx| ≤ (lr * ∑ idx : Fin (c4 * c4 * kH * kW), gradAt (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten idx ^ 2) / 4) (h2 : 2 * ↑nClasses * ↑(2 * h * (2 * w)) ^ 2 * ↑d1 ^ 2 * ↑d1 ^ 2 * w₉ ^ 2 * wa ^ 2 * wb ^ 2 * a ^ 2 / (1 - 2 * (wb * (↑d1 * (wa * (↑d1 * (w₉ * (↑(2 * h * (2 * w)) * (a * stepRadius (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten lr η)))))))) * stepRadius (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten lr η ^ 2 ≤ (lr * ∑ idx : Fin (c4 * c4 * kH * kW), gradAt (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten idx ^ 2) / 4) :
        crossEntropy nClasses (cifarCnn8Forward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ (Kernel4.unflatten (W₈.flatten - lr • gh)) b₈ W₉ b₉ Wa ba Wb bb image) label ≤ crossEntropy nClasses (cifarCnn8Forward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ (Kernel4.unflatten W₈.flatten) b₈ W₉ b₉ Wa ba Wb bb image) label - (lr * ∑ idx : Fin (c4 * c4 * kH * kW), gradAt (cifar8LastConvLoss b₈ x₁ W₉ b₉ Wa ba Wb bb label) W₈.flatten idx ^ 2) / 2

        CIFAR-8 last-conv SGD descent. One SGD step on the LAST conv W₈ of the actual cifarCnn8Forward net (the earlier seven conv layers held fixed — their output on image is the frozen feature map x₁) decreases the cross-entropy loss of the example (image, label) by at least lr·‖∇‖²/2, under the segment-margin conditions that freeze the ReLU/MaxPool routing along the step. Because CIFAR-8's tail (W₈ → relu → maxpool → 3 denses) is byte-for-byte the architecture cnn_conv2_sgd_descends proves descent for, this is an INSTANCE of that lemma at the frozen features x₁, via cifarCnn8Forward_factor, with that lemma's hypotheses (oracle accuracy hgh, the margins hm2/hmq/hm3/hm4, hsmall, h1, h2) stated at x₁. Descent through the depth of all eight conv layers is not proved: each extra layer would multiply another operator-norm factor into hsmall's admissible-lr product.