PyTorch Round-Trip Driver

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

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

• PyTorch exporters beside the demo fixtures (MLP/Export, CNN/Export, Transformer/Export)
• PyTorch JSON importers beside the demo fixtures (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 demos),
• keep the example output deterministic and readable,
• keep this demo import-safe (no root-level main that collides with other executables).

CLI model/action selection

Paths and fixed demo 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