TorchLean IBP Workflow

Small end-to-end workflow:

TorchLean forward model → lower to NN.IR.Graph → run Lean IBP (runIBP).

Run: lake exe verify -- torchlean-ibp lake exe verify -- torchlean-ibp --arithmetic ieee

def NN.Verification.Builtin.IBPWorkflow.inDim : ℕ

Input dimension for the small MLP in this workflow.

def NN.Verification.Builtin.IBPWorkflow.hidDim : ℕ

Hidden width for the small MLP in this workflow.

def NN.Verification.Builtin.IBPWorkflow.outDim : ℕ

Output dimension for the small MLP in this workflow.

def NN.Verification.Builtin.IBPWorkflow.xShape : Spec.Shape

Input shape for the workflow model.

def NN.Verification.Builtin.IBPWorkflow.yShape : Spec.Shape

Output shape for the workflow model.

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

TorchLean model used in the workflow (a 2-layer ReLU MLP).

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

Deterministically instantiate mkModel from initialization seed zero.

def NN.Verification.Builtin.IBPWorkflow.paramShapes : List Spec.Shape

Parameter shapes for model.

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

Runtime-selected typed runner used by the CLI entrypoint.

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

CLI entry point for the TorchLean → IR → IBP workflow.

This is wired into lake exe verify -- torchlean-ibp.