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:

It runs the smallest complete lowering path: GraphSpec.Models.mlp → ToTorchLean.toSeq → Trainer.new → trainer.train.
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:

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

You can also pass the standard TorchLean runtime flags such as --dtype ieee32, --backend eager, or --backend compiled.

source

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

String

Command-line help for the GraphSpec tutorial.

Instances For

Small architecture terms that should typecheck #

source

The smallest sequential GraphSpec model.

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

Instances For

source

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.

Instances For

source

def NN.Examples.DeepDives.GraphSpec.Tutorial.tutorialResidual :

GraphSpec.DAG.Model (GraphSpec.Models.ResidualLinearParams 4) [Spec.Shape.dim 4 Spec.Shape.scalar] (Spec.Shape.dim 4 Spec.Shape.scalar)

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.

Instances For

source

def NN.Examples.DeepDives.GraphSpec.Tutorial.printCatalog :

IO Unit

Print the architecture ladder this tutorial is checking.

Instances For

source

def NN.Examples.DeepDives.GraphSpec.Tutorial.tutorialDataset :

TorchLean.Trainer.Dataset (Spec.Shape.dim 2 Spec.Shape.scalar) (Spec.Shape.dim 1 Spec.Shape.scalar)

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

Instances For

source