β-VAE-Style CIFAR Example

Runnable compact VAE path over flattened CIFAR images.

The formal VAE objective and decomposition theorems live in NN.Spec.Models.Vae and NN.MLTheory.Generative.Latent.VAE. This executable uses a compact supervised runtime target: reconstruct the image while keeping latent mean/log-variance proxy channels near zero.

def NN.Examples.Models.Generative.Vae.exeName : String

CLI subcommand name used in terminal banners and error messages.

def NN.Examples.Models.Generative.Vae.defaultLogJson : System.FilePath

Default JSON loss-curve path for this command.

def NN.Examples.Models.Generative.Vae.cfg : TorchLean.nn.models.VectorGenerativeConfig

Shared vector-image configuration.

The runtime example uses the same flattened CIFAR data boundary as the other vector generative commands, while the VAE-specific output shape adds latent mean/log-variance proxy channels.

@[reducible, inline]

abbrev NN.Examples.Models.Generative.Vae.σ : Shape

Input shape: a batch of flattened CIFAR image vectors.

@[reducible, inline]

abbrev NN.Examples.Models.Generative.Vae.τ : Shape

Output shape: reconstruction plus latent regularization proxy channels.

def NN.Examples.Models.Generative.Vae.model : TorchLean.nn.M (TorchLean.nn.Sequential σ τ)

Trainable VAE-style vector model.

The executable target is still an MSE-style supervised sample; the imported spec/theory files state the theorem-facing VAE objective separately.

def NN.Examples.Models.Generative.Vae.data (flags : RealData.CifarModelTrainFlags) : TorchLean.Trainer.Dataset σ τ

Public singleton dataset for compact CIFAR reconstruction plus latent-stat targets.

def NN.Examples.Models.Generative.Vae.train (opts : TorchLean.Options) (flags : RealData.CifarModelTrainFlags) : IO (TorchLean.Trainer.TrainResult σ τ)

Train the compact VAE-style model with the public Trainer surface.

def NN.Examples.Models.Generative.Vae.main (args : List String) : IO UInt32

Executable entrypoint for the compact VAE-style run.

The command loads CIFAR vectors, constructs the reconstruction/latent-proxy target, trains with Adam, and writes the standard TorchLean training summary/log.