Train a Classifier, Then Verify Robustness

This is the complete high-level workflow: build and train a classifier, then verify that its class cannot change inside an L-infinity input ball. Graph lowering and Alpha-Beta-CROWN execution remain inside the normal trained.verify operation.

Training:

• build a two-layer ReLU classifier
• train it with one-hot cross-entropy

Verification:

• call trained.verify with norm := .inf
• run fixed-relaxation Alpha-Beta-CROWN over the trained parameters
• report typed output bounds, the worst-case class margin, and the certification result

Run: lake exe verify -- torchlean-mlp-workflow lake exe verify -- torchlean-mlp-workflow --arithmetic ieee

@[reducible, inline]

abbrev NN.Verification.Builtin.MlpTrainVerifyWorkflow.inDim : ℕ

Input dimension for the workflow model.

@[reducible, inline]

abbrev NN.Verification.Builtin.MlpTrainVerifyWorkflow.hiddenDim : ℕ

Hidden width for the workflow classifier.

@[reducible, inline]

abbrev NN.Verification.Builtin.MlpTrainVerifyWorkflow.outDim : ℕ

Number of output classes.

@[reducible, inline]

abbrev NN.Verification.Builtin.MlpTrainVerifyWorkflow.xShape : List ℕ

Input shape for the workflow model.

@[reducible, inline]

abbrev NN.Verification.Builtin.MlpTrainVerifyWorkflow.yShape : List ℕ

Output shape for the workflow model.

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.XFloat : TorchLean.Tensor Float (8 :: xShape)

Linearly separable two-dimensional training inputs.

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.YFloat : TorchLean.Tensor Float (8 :: yShape)

One-hot labels: positive first coordinate is class zero, negative is class one.

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.mkModel : TorchLean.nn.Builder (TorchLean.nn.Sequential xShape yShape)

TorchLean model used for training and verification.

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.model : TorchLean.nn.Sequential xShape yShape

Deterministically instantiate the workflow model from initialization seed zero.

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.runOnce {α : Type} [TorchLean.Storage α] [Context α] [ToString α] [TorchLean.Runtime.FromFloat α] (options : TorchLean.Runtime.Config) : IO Unit

Run training and verification under a chosen scalar backend α.

The trained result owns the trained parameters. The robustness call therefore checks the model that was actually trained.

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.runMain {α : Type} [TorchLean.Storage α] [Context α] [ToString α] [TorchLean.Runtime.FromFloat α] (options : TorchLean.Runtime.Config) (rest : List String) : IO Unit

Runtime-selected typed runner used by the CLI entrypoint.

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.main (args : List String) : IO Unit

CLI entry point for the native TorchLean MLP workflow.

This is wired into lake exe verify -- torchlean-mlp-workflow.