TorchLean IR to PyTorch

Tutorial: TorchLean → IR (NN.IR.Graph) → emitted PyTorch code.

Run: scripts/lake.sh exe torchlean torch_ir_pytorch --arch linear > exported_model.py scripts/lake.sh exe torchlean torch_ir_pytorch --arch mlp > exported_model.py scripts/lake.sh exe torchlean torch_ir_pytorch --arch sum > exported_model.py scripts/lake.sh exe torchlean torch_ir_pytorch --arch autoencoder > exported_model.py scripts/lake.sh exe torchlean torch_ir_pytorch --arch mha > exported_model.py scripts/lake.sh exe torchlean torch_ir_pytorch --arch mha-mask > exported_model.py scripts/lake.sh exe torchlean torch_ir_pytorch --arch transformer > exported_model.py Then: python3 exported_model.py

The command emits the selected architecture and initialized parameters; it does not train them. Python execution requires PyTorch. Exporting or running the file does not by itself prove TorchLean/PyTorch numerical parity.

def NN.Examples.DeepDives.TorchIRPyTorch.exeName : String

Command name used in diagnostics and by the top-level example runner.

Architectures

def NN.Examples.DeepDives.TorchIRPyTorch.linear : TorchLean.nn.Builder (TorchLean.nn.Sequential [2] [1])

def NN.Examples.DeepDives.TorchIRPyTorch.mlp : TorchLean.nn.Builder (TorchLean.nn.Sequential [2] [1])

A 2 -> 3 -> 1 MLP with ReLU, the smallest architecture with a nonlinearity.

def NN.Examples.DeepDives.TorchIRPyTorch.sum : TorchLean.nn.Builder (TorchLean.nn.Sequential [4] [])

A bare reduction, included because it exports to torch.sum rather than to a module.

def NN.Examples.DeepDives.TorchIRPyTorch.autoencoder : TorchLean.nn.Builder (TorchLean.nn.Sequential [3] [3])

A 3 -> 2 -> 3 autoencoder with a tanh bottleneck.

def NN.Examples.DeepDives.TorchIRPyTorch.attention (mask : Option (TorchLean.Tensor Bool [4, 4]) := none) : TorchLean.nn.Builder (TorchLean.nn.Sequential [1, 4, 8] [1, 4, 8])

Two-head self-attention over a length-four sequence of width eight, with an optional mask. For causal attention, pass some (Spec.causalMask 4); position i then attends only to j ≤ i.

def NN.Examples.DeepDives.TorchIRPyTorch.transformer : TorchLean.nn.Builder (TorchLean.nn.Sequential [1, 2, 2] [1, 2, 2])

A full encoder block: attention, residual, LayerNorm, ReLU feed-forward, residual, LayerNorm.

Deliberately tiny (one head of width two) so the emitted Python stays readable. We choose ReLU explicitly because the verifier IR does not yet lower GELU faithfully.

CLI parsing

def NN.Examples.DeepDives.TorchIRPyTorch.usage : String

Export driver

def NN.Examples.DeepDives.TorchIRPyTorch.emit {σ τ : Spec.Shape} (className : String) (model : TorchLean.nn.Sequential σ τ) : IO Unit

Lower a sequential model and its initial state, then write generated Python to stdout.

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

Entry point. Writes Python to stdout for redirection to a file and execution under PyTorch.