PyTorch Round-Trip Driver

This module is the single source of truth for the state-dict round-trip examples.

It does not re-implement model math. Instead it wires together the existing:

• PyTorch exporters beside the reference examples (MLP/Export, CNN/Export, Transformer/Export)
• PyTorch JSON importers beside the reference examples (MLP/Import, CNN/Import, Transformer/Import)
• Spec models (NN/Spec/Models/*) for running a small forward pass in Lean

Run via the TorchLean example runner:

lake exe torchlean pytorch_roundtrip --model mlp|cnn|transformer --action export|import

Design goals:

• keep paths/dimensions centralized (no duplicated constants across examples),
• keep the example output deterministic and readable,
• keep this example import-safe (no root-level main that collides with other executables).

CLI model/action selection

Paths and fixed example dimensions

Small IO helpers

Export actions

Import actions (Lean forward pass)

Public entrypoint called from the examples zoo runner

def NN.Examples.Interop.PyTorch.Roundtrip.main (args : List String) : IO Unit