Documentation

LeanMlir.Proofs.Training.TrainedMlpWitness

Trained-weight whole-network VJP witness (MLP rung) #

REDUCED CERTIFICATE MODEL — this file's concrete net is the 4×4-pooled 49-dim MNIST family (width-8 hidden, /128–/256 rational weights), NOT the canonical 784→512→512→10 mlpVerified; chosen so every margin/norm/SOS check is exact rational arithmetic in-kernel. Canonical surface: Proofs/MlpCanonical.lean.

The audit's "live witnesses use synthetic weights" gap, closed at the MLP rung: the SAME trained, /128-rationalized 49→8→10 pooled-MNIST network certified in LipschitzCertInstance.lean (test acc 89.8%) instantiates the conditional VJP framework at a REAL input — test digit #1895 — with every ReLU smoothness hypothesis discharged from the exact rational pre-activations (7 units strictly on, 1 strictly off; nothing sits on a kink), rather than engineered by synthetic β-shifts as in ResNet34FullBSeal/Mnv2FullBSeal. Levels:

Weights/input are imported from LipschitzCertInstance (generator: scripts/lipschitz_cert_rationalize.py); the dense convention is transposed (Mat is input×output) and biases are zero.

source
noncomputable def Proofs.TrainedMlp.W1V :
Mat 49 8

Hidden weights in the Mat (input×output) convention: W1V i k = W1t k i.

Equations
Instances For
    source
    noncomputable def Proofs.TrainedMlp.W2V :
    Mat 8 10
    Equations
    Instances For
      source
      noncomputable def Proofs.TrainedMlp.b8 :
      Vec 8
      Equations
      Instances For
        source
        noncomputable def Proofs.TrainedMlp.b10 :
        Vec 10
        Equations
        Instances For
          source
          noncomputable def Proofs.TrainedMlp.xtV :
          Vec 49

          The pooled test digit as a Vec (coordinates of xt).

          Equations
          Instances For
            source
            noncomputable def Proofs.TrainedMlp.fwd :
            Vec 49 → Vec 10

            The trained forward in the VJP framework's vocabulary.

            Equations
            Instances For
              source
              theorem Proofs.TrainedMlp.preact_eq (k : Fin 8) :
              dense W1V b8 xtV k = LipschitzCertDemo.hpreVals k

              The hidden pre-activations transfer from the certificate file's exact evaluation (hpre_eval): same sums, transposed convention.

              source
              theorem Proofs.TrainedMlp.preact_ne (k : Fin 8) :
              dense W1V b8 xtV k ≠ 0

              Smoothness at the trained witness: no hidden unit sits on the ReLU kink — the exact pre-activations are all nonzero (7 positive, 1 negative). The condition the synthetic live witnesses had to engineer, here inherited from training.

              source
              noncomputable def Proofs.TrainedMlp.trainedMlp_has_vjp_at :
              HasVJPAt fwd xtV

              Level 1: the trained-weight whole-net VJP witness — HasVJPAt fwd xtV, every hypothesis discharged (dense layers globally smooth, ReLU off-kink by preact_ne). The 2-layer analogue of mlp_has_vjp_at, at trained weights and a real input.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Proofs.TrainedMlp.trainedMlp_has_vjp_correct (dy : Vec 10) (i : Fin 49) :
                trainedMlp_has_vjp_at.backward dy i = ∑ j : Fin 10, pdiv fwd xtV i j * dy j

                The witness's contract, exposed: backward = the pdiv-contracted Jacobian.

                source
                theorem Proofs.TrainedMlp.pdiv_fwd (j : Fin 49) (c : Fin 10) :
                pdiv fwd xtV j c = ∑ k : Fin 8, W1V j k * ((if LipschitzCertDemo.hpreVals k > 0 then 1 else 0) * W2V k c)

                The whole-net Jacobian in closed form at the witness: dense → masked-ReLU → dense collapses to Σ_k W1[k,j]·mask_k·W2[c,k] (chain rule through the two proven layer Jacobians, both kinks avoided).

                source
                theorem Proofs.TrainedMlp.pdiv_fwd_val :
                pdiv fwd xtV 23 1 = -85017 / 8192

                The Jacobian entry (∂ logit_1 / ∂ x_23) at the witness, exactly.

                source
                theorem Proofs.TrainedMlp.pdiv_fwd_ne :
                pdiv fwd xtV 23 1 ≠ 0
                source
                theorem Proofs.TrainedMlp.trainedMlp_backward_nontrivial :
                trainedMlp_has_vjp_at.backward (basisVec 1) 23 ≠ 0

                Level 3: the trained-weight backward is not the zero map — the seal the synthetic witnesses carry, at trained weights.

                source
                theorem Proofs.TrainedMlp.trainedMlp_jacobian_nonzero :
                fderiv ℝ fwd xtV ≠ 0

                The fderiv form: the whole-net Jacobian at the trained witness is nonzero.

                source
                theorem Proofs.TrainedMlp.trainedMlp_not_constant :
                ¬∀ (u v : Vec 49), fwd u = fwd v

                The trained network is not a constant function.