Generative adversarial network (GAN) spec

This module gives TorchLean a small, total GAN interface:

• Generator maps latent noise to synthetic observations;
• Discriminator maps observations to scalar "realness" scores; and
• the default objective is least-squares GAN (LSGAN), written with existing MSE specs.

We choose LSGAN as the baseline spec because it is total, compact, and verifier-friendly. Classical logistic GAN losses can be built on top of the same Generator/Discriminator records, but they need additional domain discipline around log.

References:

• Goodfellow et al. (2014), "Generative Adversarial Nets".
• Mao et al. (2017), "Least Squares Generative Adversarial Networks".

Implementation status

nn.models.Generative.generator and nn.models.Generative.discriminator (NN/API/Models/Generative.lean) are independent executable builders; they are not constructed from these records and no theorem relates them to this file. The theorems that exist are about these definitions alone: the loss decompositions and zero-loss characterizations in NN/MLTheory/Generative/Latent/GAN.lean.

structure Generative.GAN.Generator (α : Type) (latent obs : Spec.Shape) [TorchLean.Storage α] : Type

Generator G_θ : z ↦ x_fake.

• forward : TorchLean.Tensor α latent → TorchLean.Tensor α obs

  Produce a synthetic observation from latent noise.

structure Generative.GAN.Discriminator (α : Type) (obs : Spec.Shape) [TorchLean.Storage α] : Type

Discriminator/critic D_φ : x ↦ score, represented as a scalar tensor.

• forward : TorchLean.Tensor α obs → TorchLean.Tensor α Spec.Shape.scalar

  Score an observation. For LSGAN, scores are regressed toward 0 or 1.

structure Generative.GAN.Model (α : Type) (latent obs : Spec.Shape) [TorchLean.Storage α] : Type

Pair of generator and discriminator components forming a GAN-style model.

• generator : Generator α latent obs

  Latent-to-observation generator.

• discriminator : Discriminator α obs

  Observation-to-score discriminator.

def Generative.GAN.generate {α : Type} [TorchLean.Storage α] {latent obs : Spec.Shape} (model : Model α latent obs) (z : TorchLean.Tensor α latent) : TorchLean.Tensor α obs

Run the generator on latent noise to produce a synthesized observation.

def Generative.GAN.fakeScore {α : Type} [TorchLean.Storage α] {latent obs : Spec.Shape} (model : Model α latent obs) (z : TorchLean.Tensor α latent) : TorchLean.Tensor α Spec.Shape.scalar

Discriminator score on a fake sample G(z).

def Generative.GAN.realScore {α : Type} [TorchLean.Storage α] {latent obs : Spec.Shape} (model : Model α latent obs) (x : TorchLean.Tensor α obs) : TorchLean.Tensor α Spec.Shape.scalar

Discriminator score on a real sample.

def Generative.GAN.realTarget {α : Type} [TorchLean.Storage α] [One α] : TorchLean.Tensor α Spec.Shape.scalar

Scalar tensor filled with 1, the LSGAN "real" target.

def Generative.GAN.fakeTarget {α : Type} [TorchLean.Storage α] [Zero α] : TorchLean.Tensor α Spec.Shape.scalar

Scalar tensor filled with 0, the LSGAN "fake" target.

@[simp]

theorem Generative.GAN.fakeScore_eq_discriminator_generate {α : Type} [TorchLean.Storage α] {latent obs : Spec.Shape} (model : Model α latent obs) (z : TorchLean.Tensor α latent) : fakeScore model z = model.discriminator.forward (model.generator.forward z)

Fake scoring expands to discriminator-after-generator.

def Generative.GAN.discriminatorLoss {α : Type} [TorchLean.Storage α] {latent obs : Spec.Shape} [Context α] (model : Model α latent obs) (xReal : TorchLean.Tensor α obs) (z : TorchLean.Tensor α latent) : α

Least-squares discriminator loss:

MSE(D(x_real), 1) + MSE(D(G(z)), 0).

def Generative.GAN.generatorLoss {α : Type} [TorchLean.Storage α] {latent obs : Spec.Shape} [Context α] (model : Model α latent obs) (z : TorchLean.Tensor α latent) : α

Least-squares generator loss:

MSE(D(G(z)), 1).

@[simp]

theorem Generative.GAN.discriminatorLoss_eq {α : Type} [TorchLean.Storage α] {latent obs : Spec.Shape} [Context α] (model : Model α latent obs) (xReal : TorchLean.Tensor α obs) (z : TorchLean.Tensor α latent) : discriminatorLoss model xReal z = Spec.mseSpec (realScore model xReal) realTarget + Spec.mseSpec (fakeScore model z) fakeTarget

The LSGAN discriminator objective is the sum of real and fake score-regression terms.

The first term pushes $D(x_{\mathrm{real}})$ toward $1$, the second pushes $D(G(z))$ toward $0$. Naming the decomposition here gives examples and proof files one stable reference point for the game semantics, so nothing downstream has to unfold discriminatorLoss by hand.