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)
• CROWN output bounds (outputBoxCROWN?)
• objective-dependent backward CROWN (backwardObjectiveBox?)

The workflow gives compact runtime checks for:

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

On the CLI's rounded backends, both CROWN queries use directed backward propagation and may fall back to coarse IBP bounds. A successful run does not establish tighter bounds or a model theorem.

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

Run: scripts/lake.sh exe verify -- torchlean-crown-ops scripts/lake.sh exe verify -- torchlean-crown-ops --arithmetic ieee

def NN.Verification.Builtin.CrownOpsWorkflow.Softmax.model : TorchLean.nn.Sequential [2] [3]

TorchLean model: Linear -> Softmax.

def NN.Verification.Builtin.CrownOpsWorkflow.Softmax.print {α : Type} [TorchLean.Storage α] [Context α] [ToString α] [MLTheory.CROWN.BoundOps α] (tag : String) (box : MLTheory.CROWN.FlatBox α) : IO Unit

Print the softmax probability bounds of a verifier box under tag, together with the directed margin p₀ - p₁. Fails when the box does not have the softmax output dimension.

def NN.Verification.Builtin.CrownOpsWorkflow.Softmax.run {α : 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.Loss.model {α : Type} [TorchLean.Storage α] [Context α] : Runtime.Autograd.Model.Program α [[2, 2], [2], [2], [2]] []

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.Loss.run {α : 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.run {α : Type} [TorchLean.Storage α] [Context α] [ToString α] [TorchLean.Runtime.FromFloat α] [MLTheory.CROWN.BoundOps α] [MLTheory.CROWN.NonlinearBoundOps α] : IO Unit

Run both CROWN examples 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 scripts/lake.sh exe verify -- torchlean-crown-ops. Missing bounds or unexpected output dimensions fail the command.