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 the bound pass 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 := linf
• run the default alphaCrown method over the trained parameters; on the rounded scalars this workflow uses, that is directed CROWN, and the report prints CROWN
• report typed output bounds, the worst-case class margin, and the certification result

Run: scripts/lake.sh exe verify -- torchlean-mlp-workflow scripts/lake.sh exe verify -- torchlean-mlp-workflow --arithmetic ieee

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.inputs : TorchLean.Tensor Float [8, 2]

Linearly separable two-dimensional training inputs.

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.labels : TorchLean.Tensor Float [8, 2]

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

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.model : TorchLean.nn.Sequential [2] [2]

Deterministically instantiate the workflow model from initialization seed zero.

def NN.Verification.Builtin.MlpTrainVerifyWorkflow.run {α : 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.main (args : List String) : IO Unit

CLI entry point for the native TorchLean MLP workflow.

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