Generative Model Helpers (API)

Small config-style constructors for runnable generative examples.

These are intentionally vector models: examples can flatten images, train the model, and later swap in convolutional encoders/decoders without changing the command-line/data-loading surface.

structure NN.API.nn.models.VectorGenerativeConfig : Type

Shared dimensions for vector generative examples.

• batch : ℕ
• dataDim : ℕ
• hiddenDim : ℕ
• latentDim : ℕ

@[implicit_reducible]

instance NN.API.nn.models.instReprVectorGenerativeConfig : Repr VectorGenerativeConfig

def NN.API.nn.models.instReprVectorGenerativeConfig.repr : VectorGenerativeConfig → ℕ → Std.Format

def NN.API.nn.models.vectorGenerativeConfig (batch dataDim hiddenDim latentDim : ℕ) : VectorGenerativeConfig

Convenience constructor for compact vector generative models.

def NN.API.nn.models.compactImageConfig (batch : ℕ := 4) (dataDim : ℕ := 128) (hiddenDim : ℕ := 64) (latentDim : ℕ := 32) : VectorGenerativeConfig

Small default config used by the runnable image-vector examples.

The input dimension is intentionally a prefix of a flattened image, not a full image decoder. That keeps examples fast while still exercising real data, batched training, and generative model constructors.

@[reducible, inline]

abbrev NN.API.nn.models.vectorDataShape (cfg : VectorGenerativeConfig) : Shape

@[reducible, inline]

abbrev NN.API.nn.models.vectorLatentShape (cfg : VectorGenerativeConfig) : Shape

@[reducible, inline]

abbrev NN.API.nn.models.vectorVaeOutShape (cfg : VectorGenerativeConfig) : Shape

β-VAE-style supervised output shape.

Rows contain:

• reconstruction, length dataDim;
• latent mean proxy, length latentDim;
• latent log-variance proxy, length latentDim.

The runnable example trains this compact target with MSE, which is a practical path for the runtime. The formal VAE ELBO/KL objective lives in NN.Spec.Models.Vae and NN.MLTheory.Generative.Latent.VAE.

def NN.API.nn.models.flattenBatchPrefix {α : Type} [Inhabited α] (cfg : VectorGenerativeConfig) {source : Shape} (hData : cfg.dataDim ≤ Shape.size source) (x : Spec.Tensor α (Spec.Shape.dim cfg.batch source)) : Spec.Tensor α (vectorDataShape cfg)

Flatten each sample in a batch and keep the first cfg.dataDim entries.

This is useful for quick image-vector experiments: a model can train on a small typed vector view of an image without every example needing to carry its own flattening proof adapters.

def NN.API.nn.models.reconstructionSample {α : Type} (cfg : VectorGenerativeConfig) (x : Spec.Tensor α (vectorDataShape cfg)) : sample.Supervised α (vectorDataShape cfg) (vectorDataShape cfg)

Supervised reconstruction sample: target equals input.

def NN.API.nn.models.zeroLatentStatsTarget (cfg : VectorGenerativeConfig) (x : Spec.Tensor Float (vectorDataShape cfg)) : Spec.Tensor Float (vectorVaeOutShape cfg)

Target for compact VAE-style examples.

Rows contain the reconstruction target followed by zero mean/log-variance proxy channels.

def NN.API.nn.models.vaeSample (cfg : VectorGenerativeConfig) (x : Spec.Tensor Float (vectorDataShape cfg)) : sample.Supervised Float (vectorDataShape cfg) (vectorVaeOutShape cfg)

Supervised compact VAE sample: image reconstruction plus zero latent-stat targets.

def NN.API.nn.models.vectorNoise (batch dim seed salt : ℕ) (lo hi : Float) : Spec.Tensor Float (Tensor.Shape.Mat batch dim)

Deterministic matrix-valued pseudo-random tensor in [lo, hi).

def NN.API.nn.models.latentNoise (cfg : VectorGenerativeConfig) (seed : ℕ) : Spec.Tensor Float (vectorLatentShape cfg)

Deterministic latent noise for generator examples.

def NN.API.nn.models.dataNoise (cfg : VectorGenerativeConfig) (seed : ℕ) : Spec.Tensor Float (vectorDataShape cfg)

Deterministic data-shaped noise for discriminator examples.

def NN.API.nn.models.scoreTarget (cfg : VectorGenerativeConfig) (value : Float) : Spec.Tensor Float (Tensor.Shape.Mat cfg.batch 1)

Constant discriminator/critic target.

def NN.API.nn.models.onesScore (cfg : VectorGenerativeConfig) : Spec.Tensor Float (Tensor.Shape.Mat cfg.batch 1)

Target score for real samples.

def NN.API.nn.models.zerosScore (cfg : VectorGenerativeConfig) : Spec.Tensor Float (Tensor.Shape.Mat cfg.batch 1)

Target score for generated or noise samples.

def NN.API.nn.models.vectorAutoencoder (cfg : VectorGenerativeConfig) : M (Sequential (vectorDataShape cfg) (vectorDataShape cfg))

Autoencoder: x -> hidden -> latent -> hidden -> reconstruction.

def NN.API.nn.models.vectorVae (cfg : VectorGenerativeConfig) : M (Sequential (vectorDataShape cfg) (vectorVaeOutShape cfg))

Compact β-VAE-style network producing reconstruction plus latent statistics.

def NN.API.nn.models.vectorVqVae (cfg : VectorGenerativeConfig) : M (Sequential (vectorDataShape cfg) (vectorDataShape cfg))

VQ-VAE-style encoder/decoder with a narrow discrete-code proxy bottleneck.

def NN.API.nn.models.vectorGanGenerator (cfg : VectorGenerativeConfig) : M (Sequential (vectorLatentShape cfg) (vectorDataShape cfg))

Generator z -> x.

def NN.API.nn.models.vectorGanDiscriminator (cfg : VectorGenerativeConfig) : M (Sequential (vectorDataShape cfg) (Tensor.Shape.Mat cfg.batch 1))

Discriminator/critic x -> score.