Convolutional Network Specifications

This module defines a two-block convolutional network over an arbitrary number of spatial axes. Its spatial parameters are vectors, so the same model definition applies to sequence, image, volume, and higher-rank data. Both the compositional module description and the explicit reverse-mode specification use the generic convolution and pooling operations.

Implementation status

nn.models.cnn (NN/API/Models/Cnn.lean) builds a one-block classifier convolution -> activation -> max pool -> flatten -> linear, whereas this file specifies a two-block network; no theorem relates them. This specification is imported by NN/Runtime/PyTorch/Export/CNN.lean.

def Models.Cnn.blockOutSpatial {d : ℕ} (spatial kernel convStride convPadding poolKernel poolStride poolPadding : TorchLean.Tensor ℕ [d]) : TorchLean.Tensor ℕ [d]

Spatial shape after one convolution followed by one pooling operation.

def Models.Cnn.outputSpatial {d : ℕ} (spatial kernel convStride₁ convPadding₁ convStride₂ convPadding₂ poolKernel poolStride₁ poolPadding₁ poolStride₂ poolPadding₂ : TorchLean.Tensor ℕ [d]) : TorchLean.Tensor ℕ [d]

Spatial shape after two convolution-pooling blocks.

def Models.Cnn.featureShape {d : ℕ} (channels : ℕ) (spatial kernel convStride₁ convPadding₁ convStride₂ convPadding₂ poolKernel poolStride₁ poolPadding₁ poolStride₂ poolPadding₂ : TorchLean.Tensor ℕ [d]) : Spec.Shape

Feature-map shape after the second pooling operation.

def Models.Cnn.featureSize {d : ℕ} (channels : ℕ) (spatial kernel convStride₁ convPadding₁ convStride₂ convPadding₂ poolKernel poolStride₁ poolPadding₁ poolStride₂ poolPadding₂ : TorchLean.Tensor ℕ [d]) : ℕ

Number of scalar features presented to the linear head.

def Models.Cnn.spec {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {d inChannels hiddenChannels outputSize : ℕ} {spatial kernel convStride₁ convPadding₁ convStride₂ convPadding₂ poolKernel poolStride₁ poolPadding₁ poolStride₂ poolPadding₂ : TorchLean.Tensor ℕ [d]} {hPoolKernel : ∀ (i : Fin d), poolKernel.getScalar i ≠ 0} {hPoolStride₁ : ∀ (i : Fin d), poolStride₁.getScalar i ≠ 0} {hPoolStride₂ : ∀ (i : Fin d), poolStride₂.getScalar i ≠ 0} (conv₁ : Spec.ConvSpec d inChannels hiddenChannels kernel convStride₁ convPadding₁ α) (conv₂ : Spec.ConvSpec d hiddenChannels hiddenChannels kernel convStride₂ convPadding₂ α) (pool₁ : Spec.MaxPoolSpec d poolKernel poolStride₁ poolPadding₁ hPoolKernel hPoolStride₁) (pool₂ : Spec.MaxPoolSpec d poolKernel poolStride₂ poolPadding₂ hPoolKernel hPoolStride₂) (head : Spec.LinearSpec α (featureSize hiddenChannels spatial kernel convStride₁ convPadding₁ convStride₂ convPadding₂ poolKernel poolStride₁ poolPadding₁ poolStride₂ poolPadding₂) outputSize) : Spec.Module.Chain α (Spec.Shape.ofList (inChannels :: spatial.to (List ℕ))) (Spec.Shape.dim outputSize Spec.Shape.scalar)

Two convolution-pooling blocks followed by a linear head.

def Models.Cnn.withReluSpec {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {d inChannels hiddenChannels outputSize : ℕ} {spatial kernel convStride₁ convPadding₁ convStride₂ convPadding₂ poolKernel poolStride₁ poolPadding₁ poolStride₂ poolPadding₂ : TorchLean.Tensor ℕ [d]} {hPoolKernel : ∀ (i : Fin d), poolKernel.getScalar i ≠ 0} {hPoolStride₁ : ∀ (i : Fin d), poolStride₁.getScalar i ≠ 0} {hPoolStride₂ : ∀ (i : Fin d), poolStride₂.getScalar i ≠ 0} (conv₁ : Spec.ConvSpec d inChannels hiddenChannels kernel convStride₁ convPadding₁ α) (conv₂ : Spec.ConvSpec d hiddenChannels hiddenChannels kernel convStride₂ convPadding₂ α) (pool₁ : Spec.MaxPoolSpec d poolKernel poolStride₁ poolPadding₁ hPoolKernel hPoolStride₁) (pool₂ : Spec.MaxPoolSpec d poolKernel poolStride₂ poolPadding₂ hPoolKernel hPoolStride₂) (head : Spec.LinearSpec α (featureSize hiddenChannels spatial kernel convStride₁ convPadding₁ convStride₂ convPadding₂ poolKernel poolStride₁ poolPadding₁ poolStride₂ poolPadding₂) outputSize) : Spec.Module.Chain α (Spec.Shape.ofList (inChannels :: spatial.to (List ℕ))) (Spec.Shape.dim outputSize Spec.Shape.scalar)

The same network with ReLU after each convolution.

def Models.Cnn.forward {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {d inChannels hiddenChannels outputSize : ℕ} {spatial kernel convStride₁ convPadding₁ convStride₂ convPadding₂ poolKernel poolStride₁ poolPadding₁ poolStride₂ poolPadding₂ : TorchLean.Tensor ℕ [d]} {hPoolKernel : ∀ (i : Fin d), poolKernel.getScalar i ≠ 0} {hPoolStride₁ : ∀ (i : Fin d), poolStride₁.getScalar i ≠ 0} {hPoolStride₂ : ∀ (i : Fin d), poolStride₂.getScalar i ≠ 0} (conv₁ : Spec.ConvSpec d inChannels hiddenChannels kernel convStride₁ convPadding₁ α) (conv₂ : Spec.ConvSpec d hiddenChannels hiddenChannels kernel convStride₂ convPadding₂ α) (pool₁ : Spec.MaxPoolSpec d poolKernel poolStride₁ poolPadding₁ hPoolKernel hPoolStride₁) (pool₂ : Spec.MaxPoolSpec d poolKernel poolStride₂ poolPadding₂ hPoolKernel hPoolStride₂) (head : Spec.LinearSpec α (featureSize hiddenChannels spatial kernel convStride₁ convPadding₁ convStride₂ convPadding₂ poolKernel poolStride₁ poolPadding₁ poolStride₂ poolPadding₂) outputSize) (x : TorchLean.Tensor α (Spec.Shape.ofList (inChannels :: spatial.to (List ℕ)))) : TorchLean.Tensor α [outputSize]

Evaluate a convolutional chain on one input tensor.

structure Models.TwoBlockCnn.Config (d : ℕ) : Type

Hyperparameters for a two-block convolutional network of spatial rank d.

• conv1Channels : ℕ
• conv2Channels : ℕ
• outputSize : ℕ
• kernel : TorchLean.Tensor ℕ [d]
• conv1Stride : TorchLean.Tensor ℕ [d]
• conv1Padding : TorchLean.Tensor ℕ [d]
• conv2Stride : TorchLean.Tensor ℕ [d]
• conv2Padding : TorchLean.Tensor ℕ [d]
• poolKernel : TorchLean.Tensor ℕ [d]
• poolStride1 : TorchLean.Tensor ℕ [d]
• poolPadding1 : TorchLean.Tensor ℕ [d]
• poolStride2 : TorchLean.Tensor ℕ [d]
• poolPadding2 : TorchLean.Tensor ℕ [d]

structure Models.TwoBlockCnn.Config.WF {d : ℕ} (config : Config d) : Prop

Conditions needed by convolutional and pooling implementations.

• conv1Channels_ne_zero : config.conv1Channels ≠ 0
• conv2Channels_ne_zero : config.conv2Channels ≠ 0
• outputSize_ne_zero : config.outputSize ≠ 0
• kernel_ne_zero (i : Fin d) : config.kernel.getScalar i ≠ 0
• conv1Stride_ne_zero (i : Fin d) : config.conv1Stride.getScalar i ≠ 0
• conv2Stride_ne_zero (i : Fin d) : config.conv2Stride.getScalar i ≠ 0
• poolKernel_ne_zero (i : Fin d) : config.poolKernel.getScalar i ≠ 0
• poolStride1_ne_zero (i : Fin d) : config.poolStride1.getScalar i ≠ 0
• poolStride2_ne_zero (i : Fin d) : config.poolStride2.getScalar i ≠ 0

def Models.TwoBlockCnn.defaultConfig (d : ℕ) : Config d

The default configuration at any spatial rank.

theorem Models.TwoBlockCnn.defaultConfig_wf (d : ℕ) : (defaultConfig d).WF

The default configuration is well formed.

structure Models.TwoBlockCnn.Model {d : ℕ} (config : Config d) (inChannels : ℕ) (spatial : TorchLean.Tensor ℕ [d]) (α : Type) [TorchLean.Storage α] (hCfg : config.WF) : Type

A generic two-block convolutional network with an explicit linear head.

• conv1 : Spec.ConvSpec d inChannels config.conv1Channels config.kernel config.conv1Stride config.conv1Padding α
• conv2 : Spec.ConvSpec d config.conv1Channels config.conv2Channels config.kernel config.conv2Stride config.conv2Padding α
• pool1 : Spec.MaxPoolSpec d config.poolKernel config.poolStride1 config.poolPadding1 ⋯ ⋯
• pool2 : Spec.MaxPoolSpec d config.poolKernel config.poolStride2 config.poolPadding2 ⋯ ⋯
• head : Spec.LinearSpec α (Cnn.featureSize config.conv2Channels spatial config.kernel config.conv1Stride config.conv1Padding config.conv2Stride config.conv2Padding config.poolKernel config.poolStride1 config.poolPadding1 config.poolStride2 config.poolPadding2) config.outputSize

structure Models.TwoBlockCnn.Grads {d : ℕ} (config : Config d) (inChannels : ℕ) (spatial : TorchLean.Tensor ℕ [d]) (α : Type) [TorchLean.Storage α] : Type

Parameter gradients for Model.

• conv1Kernel : TorchLean.Tensor α (Spec.Shape.ofList (config.conv1Channels :: inChannels :: config.kernel.to (List ℕ)))
• conv1Bias : TorchLean.Tensor α [config.conv1Channels]
• conv2Kernel : TorchLean.Tensor α (Spec.Shape.ofList (config.conv2Channels :: config.conv1Channels :: config.kernel.to (List ℕ)))
• conv2Bias : TorchLean.Tensor α [config.conv2Channels]
• headWeight : TorchLean.Tensor α [config.outputSize, Cnn.featureSize config.conv2Channels spatial config.kernel config.conv1Stride config.conv1Padding config.conv2Stride config.conv2Padding config.poolKernel config.poolStride1 config.poolPadding1 config.poolStride2 config.poolPadding2]
• headBias : TorchLean.Tensor α [config.outputSize]

def Models.TwoBlockCnn.Model.forward {α : Type} [TorchLean.Storage α] [Context α] {d : ℕ} {config : Config d} {inChannels : ℕ} {spatial : TorchLean.Tensor ℕ [d]} {hCfg : config.WF} (m : Model config inChannels spatial α hCfg) (x : TorchLean.Tensor α (Spec.Shape.ofList (inChannels :: spatial.to (List ℕ)))) : TorchLean.Tensor α [config.outputSize]

Forward pass for Model.

def Models.TwoBlockCnn.Model.backward {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {d : ℕ} {config : Config d} {inChannels : ℕ} {spatial : TorchLean.Tensor ℕ [d]} {hCfg : config.WF} (m : Model config inChannels spatial α hCfg) (x : TorchLean.Tensor α (Spec.Shape.ofList (inChannels :: spatial.to (List ℕ)))) (gradOutput : TorchLean.Tensor α [config.outputSize]) : Grads config inChannels spatial α × TorchLean.Tensor α (Spec.Shape.ofList (inChannels :: spatial.to (List ℕ)))

Reverse-mode parameter and input derivatives for Model.