Convolutional PyTorch Reference Export

PyTorch exporter for the two-block convolutional round-trip reference model.

The Lean configuration is rank-parametric. PyTorch itself exposes separate Conv1d, Conv2d, and Conv3d classes, so that distinction is introduced only while rendering the external Python code.

The generated model has two convolution, ReLU, and max-pool blocks followed by Flatten and one Linear head.

structure Export.PyTorch.CNN.ConvolutionConfig (spatialRank : ℕ) : Type

Rank-parametric configuration for a PyTorch convolution layer.

• inputChannels : ℕ

  Input channels (in_channels).

• outputChannels : ℕ

  Output channels (out_channels).

• kernel : TorchLean.Tensor ℕ [spatialRank]

  Kernel extent along each spatial axis.

• stride : TorchLean.Tensor ℕ [spatialRank]

  Stride along each spatial axis.

• padding : TorchLean.Tensor ℕ [spatialRank]

  Zero-padding along each spatial axis.

structure Export.PyTorch.CNN.PoolingConfig (spatialRank : ℕ) : Type

Rank-parametric configuration for a PyTorch max-pooling layer.

• kernel : TorchLean.Tensor ℕ [spatialRank]

  Pooling-window extent along each spatial axis.

• stride : TorchLean.Tensor ℕ [spatialRank]

  Stride along each spatial axis.

• padding : TorchLean.Tensor ℕ [spatialRank]

  Zero-padding along each spatial axis.

structure Export.PyTorch.CNN.Config (spatialRank : ℕ) : Type

Configuration for the 2-block CNN exporter.

• className : String

  Class name to use in the generated Python.

• inputChannels : ℕ

  Input channels.

• inputSpatial : TorchLean.Tensor ℕ [spatialRank]

  Input extent along each spatial axis.

• firstConvolution : ConvolutionConfig spatialRank

  First convolution.

• firstPooling : PoolingConfig spatialRank

  First pooling layer.

• secondConvolution : ConvolutionConfig spatialRank

  Second convolution.

• secondPooling : PoolingConfig spatialRank

  Second pooling layer.

• flattenedWidth : ℕ

  Flattened feature count consumed by the linear head.

• outputWidth : ℕ

  Output width of the linear head.

def Export.PyTorch.CNN.dimensionsToPythonTuple (shape : Spec.Shape) : String

Render a tensor shape as a Python tuple.

def Export.PyTorch.CNN.spatialClassName (base : String) (spatialRank : ℕ) : Except String String

Select the rank-specific class name required by PyTorch's public API.

def Export.PyTorch.CNN.classSource {spatialRank : ℕ} (config : Config spatialRank) : Except String String

Render the two-block CNN as a Python nn.Module class definition.

def Export.PyTorch.CNN.withParameters {spatialRank : ℕ} (config : Config spatialRank) (firstConvolutionWeight firstConvolutionBias secondConvolutionWeight secondConvolutionBias classifierWeight classifierBias : String) : Except String String

Generate a Python CNN module plus a helper that loads explicit weights from string literals.

This is mainly used for examples: you can paste JSON/Lean-rendered weight arrays into Python and run the model without writing an extra serializer.