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 (Chain.toProgram) 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 sequential-model path: GraphSpec.Models.mlp → ToSequential.toSeq → Trainer.new → trainer.train.
2. It typechecks the broader GraphSpec model ladder: MLP, CNN, and a residual linear block.

Only the MLP is trained here because it is the compact check path for Seq lowering. The CNN and residual block remain architecture terms that graph passes, exporters, and proofs can consume.

Run:

scripts/lake.sh exe torchlean graphspec

You can also pass the standard TorchLean runtime flags such as --arithmetic ieee or --device cuda.

def NN.Examples.DeepDives.GraphSpec.Tutorial.usage : String

Command-line help for the GraphSpec tutorial.

Small architecture terms that should typecheck

def NN.Examples.DeepDives.GraphSpec.Tutorial.mlp : GraphSpec.Chain [[3, 2], [3], [1, 3], [1]] [2] [1]

The smallest sequential GraphSpec model.

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

def NN.Examples.DeepDives.GraphSpec.Tutorial.cnn : GraphSpec.Chain ([Spec.Shape.ofList (2 :: 1 :: TorchLean.Tensor.to (TorchLean.Tensor.Internal.Rep.ofList [3, 3]) (List ℕ)), [2]] ++ ([] ++ ([] ++ ([Spec.Shape.ofList (3 :: 2 :: TorchLean.Tensor.to (TorchLean.Tensor.Internal.Rep.ofList [3, 3]) (List ℕ)), [3]] ++ ([] ++ [])))) ++ [[4, (Spec.Shape.ofList (3 :: (Spec.poolOutSpatialPad (TorchLean.Tensor.Internal.Rep.ofList [4, 4]) (TorchLean.Tensor.Internal.Rep.ofList [2, 2]) (TorchLean.Tensor.Internal.Rep.ofList [2, 2]) (TorchLean.Tensor.Internal.Rep.ofList [0, 0])).to (List ℕ))).size], [4]]) (Spec.Shape.ofList (1 :: TorchLean.Tensor.to (TorchLean.Tensor.Internal.Rep.ofList [8, 8]) (List ℕ))) [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 type records the parameter shapes and intermediate spatial arithmetic are checked before the model can be used.

def NN.Examples.DeepDives.GraphSpec.Tutorial.residual : GraphSpec.DAG.Model (GraphSpec.Models.residualLinearParams 4) [[4]] [4]

The minimal DAG-native skip-connection example:

$$ x\mapsto\operatorname{ReLU}(Wx+b+x). $$

This is not a plain chain: representing it that way would either duplicate the input path or hide sharing in a special layer. That is the pedagogical reason GraphSpec.DAG exists.

def NN.Examples.DeepDives.GraphSpec.Tutorial.dataset : TorchLean.Trainer.Dataset [2] [1]

Tiny one-sample dataset for the lowered GraphSpec MLP training path.

def NN.Examples.DeepDives.GraphSpec.Tutorial.run (args : List String) : IO Unit

Run the compact MLP lowering/training path.

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

Entry point: print the operation catalogue, then lower a GraphSpec MLP and train it for a few steps.