GraphSpec tutorial

GraphSpec is TorchLean's architecture-facing graph language. It is useful when you want a model to exist first as a typed graph that can later be interpreted in several ways:

• as a pure specification (Interp.spec) for theorem statements,
• as an executable TorchLean program (Compile.torchProgram) for direct execution,
• as a sequential nn.Sequential view when the graph is just a layer stack, and
• as a DAG model when the architecture has sharing, skip connections, or multi-input nodes.

That is why this folder is not a duplicate of NN.Spec.Models or NN.Examples.Models.

• NN.Spec.Models describes mathematical/reference model semantics.
• NN.GraphSpec.Models describes architecture graphs and their parameter ABI.
• NN.Examples.Models contains runnable training scripts.

This tutorial does two things:

1. It runs the smallest complete lowering path: GraphSpec.Models.mlp → ToTorchLean.toSeq → train.run.
2. It typechecks and explains the broader GraphSpec model ladder: MLP, CNN, residual linear block, and ResNet18.

Only the MLP is trained here because it is the compact check path for Seq lowering. The larger models are still GraphSpec models; they are deliberately kept as architecture terms so graph passes, exporters, and proofs can consume them without turning this tutorial into a slow vision benchmark.

Run:

lake exe torchlean graphspec --backend eager
lake exe torchlean graphspec --backend compiled

You can also pass the standard scalar/runtime flags accepted by train.run, such as --dtype ieee32.

Small architecture terms that should typecheck

def NN.Examples.Advanced.GraphSpec.Tutorial.tutorialMlp : GraphSpec.Graph [Shape.Mat 3 2, Shape.Vec 3, Shape.Mat 1 3, Shape.Vec 1] (Shape.Vec 2) (Shape.Vec 1)

The smallest sequential GraphSpec model.

Parameter ABI: [Mat 3 2, Vec 3, Mat 1 3, Vec 1].

def NN.Examples.Advanced.GraphSpec.Tutorial.tutorialCnn : GraphSpec.Graph [Shape.OIHW 2 1 3 3, Shape.Vec 2, Shape.OIHW 3 2 3 3, Shape.Vec 3, Shape.Mat 4 (GraphSpec.Models.featSize 3 8 8 3 3 1 1 1 1 2 2 2 2), Shape.Vec 4] (Shape.CHW 1 8 8) (Shape.Vec 4)

A small CNN graph, included here so the tutorial is visibly not “just MLP”.

This is still a sequential graph: convolution, ReLU, pooling, convolution, ReLU, pooling, flatten, linear head. The ugly-looking type is the point: the parameter shapes and intermediate spatial arithmetic are checked before the model can be used.

def NN.Examples.Advanced.GraphSpec.Tutorial.tutorialResidual : GraphSpec.DAG.Model (GraphSpec.Models.ResidualLinearParams 4) [Shape.Vec 4] (Shape.Vec 4)

The minimal DAG-native skip-connection example:

x ↦ relu((W x + b) + x).

This cannot be honestly represented as a plain chain without either duplicating the input path or hiding sharing in a special layer. That is the pedagogical reason GraphSpec.DAG exists.

def NN.Examples.Advanced.GraphSpec.Tutorial.tutorialResNet18 (inC h w numClasses : ℕ) (h_inC : inC > 0) (_h_h : h > 0) (_h_w : w > 0) (_h_cls : numClasses > 0) : GraphSpec.DAG.Model (GraphSpec.Models.ResNet18.params inC numClasses) [GraphSpec.Models.ResNet18.imgShape inC h w] (Shape.Vec numClasses)

The larger residual-family architecture available from the same model catalog.

We bind it here as a compile-time smoke check: users can inspect its type in the editor, while the runtime tutorial below stays small enough to run instantly.

def NN.Examples.Advanced.GraphSpec.Tutorial.printCatalog : IO Unit

Print the architecture ladder this tutorial is checking.

def NN.Examples.Advanced.GraphSpec.Tutorial.runMlpTrainingPath (args : List String) : IO Unit

Run the compact MLP lowering/training path.

def NN.Examples.Advanced.GraphSpec.Tutorial.main (args : List String) : IO Unit