Quickstart: Starter Workflow

The smallest useful TorchLean training setup is ordinary model code:

import NN
open TorchLean

def model :=
  nn.Sequential![
    nn.Linear 2 8,
    nn.ReLU,
    nn.Linear 8 1
  ]

No NN.* subsystem imports are needed here. The example exercises the first workflow directly: model construction, data construction, training, evaluation, and verification all come from import NN.

def NN.Examples.Quickstart.StarterWorkflow.model : TorchLean.nn.M (Runtime.Autograd.TorchLean.NN.Seq (TorchLean.Shape.scalar.appendDim 2) (TorchLean.Shape.scalar.appendDim 1))

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

Checks that KAN constructors are available from the public import NN surface.

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

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

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 (TorchLean.Shape.vec 2))

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

Tiny optimizer-choice example using only import NN.

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

Tiny adapter type example using only import NN.

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.eval for initial inference,
• call trainer.train,
• use the returned trained handle for prediction.
• call trained.verifyRobustLInf on a small ℓ∞ box.

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