Documentation

LeanMlir.VerifiedPgdGen

The PGD-step kernels — hand-typed StableHLO text #

genLinearPgdStep, genMlpPgdStep, genCnnPgdStep, genCifarPgdStep: one PGD step (forward, the softmax-CE input gradient, an L∞ or L2 step, projection onto the ε-ball, clip to [0,1]) as StableHLO text, for VerifiedAttack's attacks. ⚠ These are NOT rendered from a proven graph and no tie pins them: each follows the proven input-VJP's formula by hand (the formula is cited in its docstring), so they are unverified program code, like the reference MlirCodegen.

source
def genLinearPgdStep (bs d0 d1 : Nat) (eps alpha : Float) (linf : Bool) :
String

Phase-3 PGD-step kernel for the linear classifier (planning/archive/robustness.md). forward → softmax-CE input gradient dx = (softmax(xW+b) − onehot)·Wᵀ (the proven linear input-VJP, Proofs.mlpInputGrad's 1-layer case) → L∞ sign-step → project to the eps-ball around x0 → clip to [0,1]. Returns the advanced adversarial input x_adv. eps/alpha baked as constants (recompiled per sweep point). Invoked via the generic forwardF32 FFI with onehot+x0 in the params blob and nClasses := d0 (output size) — no new FFI/C shim. The whole PGD step runs on the GPU; the host just iterates.

Instances For
    source
    def genMlpPgdStep (bs d0 h d1 : Nat) (eps alpha : Float) (linf : Bool) :
    String

    Phase-3 PGD-step kernel for the 2-hidden-layer MLP (d0→h→h→d1, ReLU). Forward (saving the pre-activations z0,z1) → the proven mlpInputGrad VJP dx = ((g·W₂ᵀ ⊙ relu'(z₁))·W₁ᵀ ⊙ relu'(z₀))·W₀ᵀ (ReLU masks via compare GT/select, the codegen's idiom) → L∞/L2 step + projection. Returns x_adv.

    Instances For
      source
      def genCnnPgdStep (bs : Nat) (eps alpha : Float) (linf : Bool) :
      String

      Phase-3 PGD-step kernel for the verified MNIST CNN (conv 1→32 → relu → conv 32→32 → relu → maxpool 28→14 → flatten → dense 6272→512 → relu → 512→512 → relu → 512→10). Forward (saving every pre-activation + the maxpool input) → softmax-CE seed → the full input-VJP dx, mirroring verified_mlir/cnn_train_step.mlir's backward ops: dot_general adjoints + ReLU masks (compare GT/select), maxpool-back (select_and_scatter, scatter the pooled cotangent to the argmax cells), and the two conv input-VJPs (transpose-o,i + spatial reverse of the kernel, then the same padded conv). The train step stops at dz1 (it only needs weight grads); here we add the final conv1 input-VJP to reach dx over the pixels. Then the L∞ sign-step / L2 projected step + ε-ball project + [0,1] clip. Architecture is fixed; only bs/eps/alpha vary.

      Instances For
        source
        def genCifarPgdStep (bs : Nat) (eps alpha : Float) (linf : Bool) :
        String

        Phase-3 PGD-step kernel for the verified CIFAR-10 CNN — the deeper sibling of genCnnPgdStep (conv 3→32 → relu → conv 32→32 → relu → maxpool → conv 32→64 → relu → conv 64→64 → relu → maxpool → flatten(4096) → 512 → 512 → 10). Same recipe — forward (saving every pre-activation + both maxpool inputs) → softmax-CE seed → the full input-VJP dx, mirroring verified_mlir/cifar_train_step.mlir's backward (4 conv input-VJPs, 2 select_and_scatter maxpool-backs, ReLU masks, dense adjoints) + the final conv1 input-VJP the train step omits — then the L∞/L2 step + ε-ball project + [0,1] clip. 3-channel 32×32, bs/eps/alpha vary.

        Instances For