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".

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

Generator G_θ : z ↦ x_fake.

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

  Produce a synthetic observation from latent noise.

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

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

• forward : Spec.Tensor α obs → Spec.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) [Context α] : Type

GAN model pair.

• generator : Generator α latent obs

  Latent-to-observation generator.

• discriminator : Discriminator α obs

  Observation-to-score discriminator.

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

Generate a fake sample.

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

Discriminator score on a fake sample G(z).

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

Discriminator score on a real sample.

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

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

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

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

def Generative.GAN.discriminatorLoss {α : Type} [Context α] {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : α) => x1 > x2] [LE α] (model : Model α latent obs) (xReal : Spec.Tensor α obs) (z : Spec.Tensor α latent) : α

Least-squares discriminator loss:

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

def Generative.GAN.generatorLoss {α : Type} [Context α] {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : α) => x1 > x2] [LE α] (model : Model α latent obs) (z : Spec.Tensor α latent) : α

Least-squares generator loss:

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

@[simp]

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

Fake scoring expands to discriminator-after-generator.

@[simp]

theorem Generative.GAN.discriminatorLoss_eq {α : Type} [Context α] {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : α) => x1 > x2] [LE α] (model : Model α latent obs) (xReal : Spec.Tensor α obs) (z : Spec.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.