TorchLean Robustness Workflow

End-to-end robustness certification for a TorchLean model.

We build a compact 2-class classifier in TorchLean, compile it to the verifier IR, and certify a margin condition on an ℓ∞ input box using:

• IBP (runIBP)
• a simple CROWN/affine pass (runAffine + AffineVec.eval_on_box)

Spec we certify (binary logits): ∀ x ∈ [x0-ε, x0+ε], logit0(x) > logit1(x)

Run: lake exe verify -- torchlean-robustness lake exe verify -- torchlean-robustness --float32-mode ieee754exec

def NN.Verification.Robustness.TorchLean.inDim : ℕ

Input dimension for the TorchLean robustness example.

def NN.Verification.Robustness.TorchLean.hidDim : ℕ

Hidden width for the TorchLean robustness example.

def NN.Verification.Robustness.TorchLean.outDim : ℕ

Number of output logits/classes.

def NN.Verification.Robustness.TorchLean.W1Shape : Shape

First-layer weight shape.

def NN.Verification.Robustness.TorchLean.b1Shape : Shape

First-layer bias shape.

def NN.Verification.Robustness.TorchLean.W2Shape : Shape

Second-layer weight shape.

def NN.Verification.Robustness.TorchLean.b2Shape : Shape

Second-layer bias shape.

def NN.Verification.Robustness.TorchLean.xShape : Shape

Shape of one input vector supplied to the certified two-layer network.

def NN.Verification.Robustness.TorchLean.yShape : Shape

Output/logit shape.

def NN.Verification.Robustness.TorchLean.paramShapes : List Shape

Parameter shapes list used by the compiled TorchLean program ([W1,b1,W2,b2]).

def NN.Verification.Robustness.TorchLean.margin {α : Type} [Context α] (lo hi : Spec.Tensor α yShape) : α

Compute a (conservative) margin lower bound lo0 - hi1 from logit bounds.

def NN.Verification.Robustness.TorchLean.certifiedMargin {α : Type} [Context α] (lo hi : Spec.Tensor α yShape) : Bool

Decide if the output bounds certify logit0 > logit1.

def NN.Verification.Robustness.TorchLean.classifier {α : Type} [Context α] [DecidableEq Shape] : Runtime.Autograd.TorchLean.Program α (paramShapes ++ [xShape]) yShape

TorchLean program for a 2-layer ReLU MLP producing two logits.

def NN.Verification.Robustness.TorchLean.runOnce {α : Type} [TorchLean.Runtime.SemanticScalar α] [DecidableEq Shape] [ToString α] [TorchLean.Runtime.Scalar α] : IO Unit

Run the robustness check once under a chosen scalar backend α.

This compiles the TorchLean program to the verifier IR, then computes output bounds with IBP and an affine/CROWN-style pass.

def NN.Verification.Robustness.TorchLean.main (args : List String) : IO Unit

CLI entry point for the TorchLean robustness workflow.

This is wired into lake exe verify -- torchlean-robustness.