TorchLean IR to PyTorch

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

Run: lake exe torchlean torch_ir_pytorch --arch linear > exported_model.py lake exe torchlean torch_ir_pytorch --arch mlp > exported_model.py lake exe torchlean torch_ir_pytorch --arch sum > exported_model.py lake exe torchlean torch_ir_pytorch --arch autoencoder > exported_model.py lake exe torchlean torch_ir_pytorch --arch mha > exported_model.py lake exe torchlean torch_ir_pytorch --arch mha-mask > exported_model.py lake 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.archLinear : TorchLean.nn.Builder (TorchLean.nn.Sequential [2] [1])

def NN.Examples.DeepDives.TorchIRPyTorch.archMLP : 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.archSumReduce : 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.archAutoencoder : TorchLean.nn.Builder (TorchLean.nn.Sequential [3] [3])

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

def NN.Examples.DeepDives.TorchIRPyTorch.archMHA : TorchLean.nn.Builder (TorchLean.nn.Sequential [1, 4, 8] [1, 4, 8])

Two-head self-attention over a length-four sequence of width eight.

def NN.Examples.DeepDives.TorchIRPyTorch.archMHAMask : TorchLean.Tensor Bool [4, 4]

A causal mask: position i may attend only to positions j ≤ i.

def NN.Examples.DeepDives.TorchIRPyTorch.archMHAMasked : TorchLean.nn.Builder (TorchLean.nn.Sequential [1, 4, 8] [1, 4, 8])

The same attention block with the causal mask applied, so the export can be compared against torch.nn.MultiheadAttention with attn_mask.

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

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

Deliberately tiny (one head of width two) so the emitted Python stays readable.

CLI parsing

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

Export driver

def NN.Examples.DeepDives.TorchIRPyTorch.emitSeq {σ τ : 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.