Quickstart: Starter Workflow

The smallest useful TorchLean training setup is ordinary model code:

public import NN.API
open TorchLean

def model :=
  nn.Sequential![
    nn.linear 2 8,
    nn.relu,
    nn.linear 8 1
  ]

No subsystem-specific imports are needed here. Model construction, data, training, prediction, and the public robustness-checking entry point all come from import NN.API. Lower-level certificate formats and proof developments use the focused NN.Verification and NN.Proofs imports.

def NN.Examples.Quickstart.StarterWorkflow.model : TorchLean.nn.M (TorchLean.nn.Sequential (Spec.Shape.scalar.appendDim 2) (Spec.Shape.scalar.appendDim 1))

def NN.Examples.Quickstart.StarterWorkflow.kanModel : TorchLean.nn.M (TorchLean.nn.Sequential (Spec.Shape.dim 4 (Spec.Shape.dim 2 Spec.Shape.scalar)) (Spec.Shape.dim 4 (Spec.Shape.dim 1 Spec.Shape.scalar)))

Checks that KAN constructors are available from NN.API.

def NN.Examples.Quickstart.StarterWorkflow.target (x1 x2 : Float) : Float

def NN.Examples.Quickstart.StarterWorkflow.data : TorchLean.Trainer.Dataset (Spec.Shape.dim 2 Spec.Shape.scalar) (Spec.Shape.dim 1 Spec.Shape.scalar)

Tiny in-memory regression dataset.

The important bit is the last line: Data.tensorDataset xs ys turns ordinary Float tensors into a runtime-polymorphic dataset, so the trainer can still choose Float, executable IEEE32, CPU, CUDA, eager, or compiled execution later.

def NN.Examples.Quickstart.StarterWorkflow.probes : List (TorchLean.Trainer.Probe (Spec.Shape.dim 2 Spec.Shape.scalar))

def NN.Examples.Quickstart.StarterWorkflow.optimizerChoiceExample : Except String (String × TorchLean.optim.Optimizer)

Select an optimizer through the public API.

def NN.Examples.Quickstart.StarterWorkflow.loraParamsExample : Type

A LoRA parameter type exposed by the public adapter API.

def NN.Examples.Quickstart.StarterWorkflow.run (_args : List String := []) : IO Unit

Run the public API example from another command or from #eval while developing.

The shape below is the user-facing training path:

• build the trainer from the model,
• attach optimizer/backend choices once,
• call trainer.predict for initial prediction,
• call trainer.train,
• use the returned trained handle for prediction.
• call trained.verifyRobustLInf on a small $\ell_\infty$ box.

The quickstart build only checks that these declarations typecheck; it does not train during ordinary lake build, which keeps CI fast.