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 $\ell^\infty$ input box using:

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

Spec we certify (binary logits):

$$ \forall x\in[x_0-\varepsilon,x_0+\varepsilon],\quad \operatorname{logit}_0(x)>\operatorname{logit}_1(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.hiddenWeightShape : Spec.Shape

First-layer weight shape.

def NN.Verification.Robustness.TorchLean.hiddenBiasShape : Spec.Shape

First-layer bias shape.

def NN.Verification.Robustness.TorchLean.outputWeightShape : Spec.Shape

Second-layer weight shape.

def NN.Verification.Robustness.TorchLean.outputBiasShape : Spec.Shape

Second-layer bias shape.

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

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

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

Output/logit shape.

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

Parameter shapes list used by the compiled TorchLean program ([hiddenWeight,hiddenBias,outputWeight,outputBias]).

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

Compute a conservative margin lower bound $\mathrm{lo}_0-\mathrm{hi}_1$ from logit bounds.

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

Decide if the output bounds certify $\operatorname{logit}_0>\operatorname{logit}_1$.

def NN.Verification.Robustness.TorchLean.classifier {α : Type} [Context α] [DecidableEq Spec.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} [Context α] [DecidableEq Spec.Shape] [ToString α] [TorchLean.Runtime.FromFloat α] [MLTheory.CROWN.BoundOps α] : 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.