Autoencoder (spec model)

This file defines a small fully-connected autoencoder:

• encoder: h = act(W_enc x + b_enc)
• decoder: x̂ = W_dec h + b_dec

PyTorch analogue: nn.Sequential(nn.Linear(inputDim, hiddenDim), act, nn.Linear(hiddenDim, inputDim)) applied to a single vector (no batch dimension).

This is spec-level/reference code. It is written for auditability and differentiation, and it is intended to be instantiated over multiple scalar backends (Float, intervals, proof-level reals, ...).

The activation is represented by Activation.Kind, so a misspelled configuration cannot silently change the model into an identity activation.

Implementation status

nn.models.Generative.autoencoder (NN/API/Models/Generative.lean) builds a different architecture, x -> hidden -> latent -> hidden -> reconstruction, and is not derived from this record. NN/Spec/Module/Autoencoder.lean wraps this file as a Spec.Module. No theorem relates either to the other.

Parameters

We store the encoder and decoder weights explicitly.

Shapes:

• encoderWeight : (hiddenDim × inputDim)
• decoderWeight : (inputDim × hiddenDim)
• encoderBias : (hiddenDim)
• decoderBias : (inputDim)

structure Spec.AutoencoderSpec (α : Type) [TorchLean.Storage α] (inputDim hiddenDim : ℕ) : Type

Parameters for a 1-hidden-layer fully-connected autoencoder.

• encoderWeight : TorchLean.Tensor α [hiddenDim, inputDim]

  Encoder weights with shape (hiddenDim × inputDim).

• encoderBias : TorchLean.Tensor α [hiddenDim]

  Encoder bias with shape (hiddenDim).

• decoderWeight : TorchLean.Tensor α [inputDim, hiddenDim]

  Decoder weights with shape (inputDim × hiddenDim).

• decoderBias : TorchLean.Tensor α [inputDim]

  Decoder bias with shape (inputDim).

• activation : Activation.Kind

  Pointwise activation between the encoder and decoder.

Forward

def Spec.autoencoderEncodeSpec {α : Type} [TorchLean.Storage α] [Context α] {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (input : TorchLean.Tensor α [inputDim]) : TorchLean.Tensor α [hiddenDim]

Encode a vector into a hidden representation:

h = act(W_enc x + b_enc).

PyTorch analogy: act(linear(x)) for a single nn.linear.

def Spec.autoencoderDecodeSpec {α : Type} [TorchLean.Storage α] [Context α] {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (hidden : TorchLean.Tensor α [hiddenDim]) : TorchLean.Tensor α [inputDim]

Decode a hidden representation back to input space:

x̂ = W_dec h + b_dec.

PyTorch analogy: a second nn.Linear(hiddenDim, inputDim) without an activation.

def Spec.autoencoderForwardSpec {α : Type} [TorchLean.Storage α] [Context α] {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (input : TorchLean.Tensor α [inputDim]) : TorchLean.Tensor α [inputDim]

Full autoencoder forward pass: decode(encode(x)).

def Spec.autoencoderForwardLeadingSpec {α : Type} [TorchLean.Storage α] [Context α] (leading : Shape) {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (input : TorchLean.Tensor α (leading.concat [inputDim])) : TorchLean.Tensor α (leading.concat [inputDim])

Apply an autoencoder independently at every index of a leading shape.

Backward (manual VJP)

This file includes a small, explicit backward pass for the autoencoder.

PyTorch analogy: this is what autograd computes, but spelled out as pure functions. The key linear-algebra identities used are:

• If y = W x + b, then dW = dY ⊗ x, db = dY, and dX = Wᵀ dY.
• If h = act(z), then dZ = dH ⊙ act'(z).

def Spec.autoencoderEncoderWeightsDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (input gradOutput : TorchLean.Tensor α [inputDim]) : TorchLean.Tensor α [hiddenDim, inputDim]

Gradient w.r.t. encoder weights: dW_enc = dZ ⊗ x.

def Spec.autoencoderEncoderBiasDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (input gradOutput : TorchLean.Tensor α [inputDim]) : TorchLean.Tensor α [hiddenDim]

Gradient w.r.t. encoder bias: db_enc = dZ.

def Spec.autoencoderDecoderWeightsDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (input gradOutput : TorchLean.Tensor α [inputDim]) : TorchLean.Tensor α [inputDim, hiddenDim]

Gradient w.r.t. decoder weights: dW_dec = dOut ⊗ h.

def Spec.autoencoderDecoderBiasDerivSpec {α : Type} [TorchLean.Storage α] {inputDim hiddenDim : ℕ} (_m : AutoencoderSpec α inputDim hiddenDim) (gradOutput : TorchLean.Tensor α [inputDim]) : TorchLean.Tensor α [inputDim]

Gradient w.r.t. decoder bias: db_dec = dOut.

def Spec.autoencoderInputDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (input gradOutput : TorchLean.Tensor α [inputDim]) : TorchLean.Tensor α [inputDim]

Gradient w.r.t. input: dX = W_encᵀ dZ.

structure Spec.AutoencoderGradients (α : Type) [TorchLean.Storage α] (inputDim hiddenDim : ℕ) : Type

Gradients for a linear autoencoder: one bundle per half, plus the input gradient.

• encoder : LinearParameterGradients α inputDim hiddenDim

  Gradients for the encoder inputDim -> hiddenDim.

• decoder : LinearParameterGradients α hiddenDim inputDim

  Gradients for the decoder hiddenDim -> inputDim.

• inputGradient : TorchLean.Tensor α [inputDim]

  Gradient with respect to the reconstructed input.

def Spec.autoencoderBackwardSpec {α : Type} [TorchLean.Storage α] [Context α] {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (input gradOutput : TorchLean.Tensor α [inputDim]) : AutoencoderGradients α inputDim hiddenDim

Complete backward pass for an autoencoder.

def Spec.autoencoderReconstructionErrorSpec {α : Type} [TorchLean.Storage α] [Context α] {inputDim hiddenDim : ℕ} (m : AutoencoderSpec α inputDim hiddenDim) (input : TorchLean.Tensor α [inputDim]) (h : inputDim ≠ 0) : α

Mean-squared reconstruction error (single example).

PyTorch analogy: F.mse_loss(x_hat, x, reduction="mean").

def Spec.autoencoderCompressionRatioSpec {inputDim hiddenDim : ℕ} : Float

A compact helper used by examples: compression ratio as a Float.

Note: if hiddenDim = 0, this produces ∞/NaN depending on the Float backend. The rest of the spec never needs this number; it is purely for display.