TorchLean CROWN Ops Workflow

Running CROWN end-to-end on small TorchLean graphs.

We lower TorchLean programs to the verifier IR (NN.IR.Graph), then run:

• IBP (runIBP)
• basic CROWN forward bounds (runCROWN)
• objective-dependent backward/dual CROWN (runCROWNBackwardObjective)

The workflow gives compact, fast coverage for nonlinear ops added to CROWN:

• softmax (vector)
• mse_loss (vector → scalar)

For attention + layer_norm, see NN/Verification/Builtin/TransformerIBPWorkflow.lean.

Run: lake exe verify -- torchlean-crown-ops lake exe verify -- torchlean-crown-ops --arithmetic ieee

def NN.Verification.Builtin.CrownOpsWorkflow.softmaxInDim : ℕ

Input dimension for the softmax workflow model.

def NN.Verification.Builtin.CrownOpsWorkflow.softmaxOutDim : ℕ

Output dimension for the softmax workflow model.

def NN.Verification.Builtin.CrownOpsWorkflow.softmaxXShape : Spec.Shape

Input shape for the softmax workflow model.

def NN.Verification.Builtin.CrownOpsWorkflow.softmaxYShape : Spec.Shape

Output shape for the softmax workflow model.

def NN.Verification.Builtin.CrownOpsWorkflow.softmaxModel : TorchLean.nn.Sequential [softmaxInDim] [softmaxOutDim]

TorchLean model: Linear -> Softmax.

def NN.Verification.Builtin.CrownOpsWorkflow.softmaxParamShapes : List Spec.Shape

Parameter shapes for softmaxModel.

def NN.Verification.Builtin.CrownOpsWorkflow.softmaxMargin {α : Type} [TorchLean.Storage α] [Context α] (lo hi : TorchLean.Tensor α softmaxYShape) : α

Example margin functional on softmax outputs ($\mathrm{lo}_0-\mathrm{hi}_1$).

def NN.Verification.Builtin.CrownOpsWorkflow.runSoftmax {α : Type} [TorchLean.Storage α] [Context α] [ToString α] [TorchLean.Runtime.FromFloat α] [MLTheory.CROWN.BoundOps α] [MLTheory.CROWN.NonlinearBoundOps α] : IO Unit

Run the softmax workflow under a chosen scalar backend α.

This lowers the TorchLean model to verifier IR and prints IBP/CROWN bounds.

def NN.Verification.Builtin.CrownOpsWorkflow.mseInDim : ℕ

Input dimension for the MSE-loss workflow model.

def NN.Verification.Builtin.CrownOpsWorkflow.mseOutDim : ℕ

Output dimension for the MSE-loss workflow model.

def NN.Verification.Builtin.CrownOpsWorkflow.mseWShape : Spec.Shape

Weight shape for the MSE-loss workflow's linear layer.

def NN.Verification.Builtin.CrownOpsWorkflow.mseBShape : Spec.Shape

Bias shape for the MSE-loss workflow's linear layer.

def NN.Verification.Builtin.CrownOpsWorkflow.mseXShape : Spec.Shape

Input shape for the MSE-loss workflow.

def NN.Verification.Builtin.CrownOpsWorkflow.mseYShape : Spec.Shape

Output shape for the MSE-loss workflow.

def NN.Verification.Builtin.CrownOpsWorkflow.mseParamShapes : List Spec.Shape

Parameter shapes for the MSE-loss workflow ([W,b,target]).

def NN.Verification.Builtin.CrownOpsWorkflow.mseLossModel {α : Type} [TorchLean.Storage α] [Context α] : Runtime.Autograd.Model.Program α (mseParamShapes ++ [mseXShape]) []

TorchLean forward program computing $\widehat{y}=\operatorname{linear}(x)$ and $\operatorname{mse\_loss}(\widehat{y},\mathrm{target})$, returning a scalar.

def NN.Verification.Builtin.CrownOpsWorkflow.runMSE {α : Type} [TorchLean.Storage α] [Context α] [ToString α] [TorchLean.Runtime.FromFloat α] [MLTheory.CROWN.BoundOps α] [MLTheory.CROWN.NonlinearBoundOps α] : IO Unit

Run the MSE-loss workflow under a chosen scalar backend α.

This lowers the TorchLean forward computation to verifier IR and prints IBP/CROWN bounds for the scalar loss.

def NN.Verification.Builtin.CrownOpsWorkflow.runOnce {α : Type} [TorchLean.Storage α] [Context α] [ToString α] [TorchLean.Runtime.FromFloat α] [MLTheory.CROWN.BoundOps α] [MLTheory.CROWN.NonlinearBoundOps α] : IO Unit

Run all CROWN-ops workflows (softmax + mse_loss) under a chosen scalar backend α.

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

CLI entry point for the CROWN-ops workflow.

This is wired into lake exe verify -- torchlean-crown-ops.