ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A Gaussian model with a positive inference gap and a collapsed latent

Example

Assume AC and use Lebesgue measure for the latent densities. In the first model, a scalar latent variable $Z$ has prior $N (0, 4)$ , and conditional on $Z = z$ the observation is $X = (Y_{1}, Y_{2})$ with $Y_{1}, Y_{2}$ IID $N (z, 1)$ . At the observed value $x = (2, 4)$ , the evidence is finite and positive and the posterior is $N (8 / 3, 4 / 9)$ . Restrict the encoder family to $q_{m} (z ∣ x) = N (m, 4 / 9)$ for $m \in [- 1, 1]$ and choose $m = 0$ . This encoder is admissible and its reverse-KL gap, with $D_{K L} (q ∥ π) : = \int q (z) \log (q (z) / π (z)) d z$ , is $D_{K L} (q_{0} (\cdot ∣ x) ∥ π (\cdot ∣ x)) = 8 > 0$ , so its ELBO is exactly $8$ below the log evidence.

In a second model, let $Z \sim N (0, 1)$ and use the standard normal density $h (x) = (2 π)^{- 1 / 2} e^{- x^{2} / 2}$ for $p (x ∣ z) = h (x)$ , independent of $z$ . For every observation $x \in R$ , the evidence is $0 < h (x) < \infty$ and the posterior equals the prior. Choose the constant encoder $q (z ∣ x) = N (0, 1)$ for every $x$ . Its reverse-KL gap is zero and its ELBO equals the log evidence on every fibre. Thus $q (z ∣ x) = p_{θ} (z ∣ x) = p (z)$ for all $x$ , a posterior-collapse configuration in which the decoder ignores the latent variable; this is one model configuration, not a claim that VAE training always collapses.

Example references

The VAE densities, posterior and ELBO conventions.

The evidence–ELBO–reverse-KL identity under AC.

The exact Normal-Normal posterior and positive evidence.

The directional reverse-KL convention.

Johnson, Ott, and Dogucu, Bayes Rules!, Chapter 5.

Kingma and Welling, Auto-Encoding Variational Bayes, arXiv v1.

He, Spokoyny, Neubig, and Berg-Kirkpatrick, Lagging Inference Networks and Posterior Collapse in Variational Autoencoders.

Facts & Assumptions

Given: AC; the two stated latent-variable models and observations; the restricted encoder family in the first model; and the definitions of evidence, posterior, admissibility and ELBO.

[A1]

The Axiom of Choice: every family of nonempty sets has a choice function; AC is used by the Gaussian density suppliers and the library KL branch.

[F1]

Variational autoencoder model, encoder, and ELBO: for positive finite evidence, $π = γ / Z$ ; an encoder is admissible when it is a probability density supported where $π$ is positive with the stated absolute log-integrability; its ELBO is the integral of $\log γ - \log q$ under $q$ .

[F2]

Known-variance Normal-Normal conjugate update: with prior $N (μ_{0}, τ_{0}^{2})$ , positive known variance $σ^{2}$ , and $n \geq 1$ IID observations from $N (μ, σ^{2})$ , the evidence is finite and positive and the posterior has variance $(τ_{0}^{- 2} + n σ^{- 2})^{- 1}$ and mean equal to that variance times $μ_{0} / τ_{0}^{2} + n \overset{ˉ}{y} / σ^{2}$ .

[F3]

Standard normal and normal laws and A positive-variance normal law has its location-scale density: $N (0, 1)$ is a probability law with density $e^{- z^{2} / 2} / \sqrt{2 π}$ , and for $σ > 0$ , $N (m, σ^{2})$ has density $(2 π σ^{2})^{- 1 / 2} \exp (- (z - m)^{2} / (2 σ^{2}))$ .

[F4]

Location-scale normal laws have their stated mean and variance: a variable with law $N (m, σ^{2})$ has mean $m$ and finite variance $σ^{2}$ .

[F5]

Kullback–Leibler divergence: for probability measures with densities $q$ and $π$ relative to one reference measure and $q μ ≪ π μ$ , the reverse divergence is $\int q \log (q / π) d μ$ .

[F6]

The VAE evidence equals the ELBO plus reverse KL: for each admissible fixed observation under AC, log evidence equals ELBO plus the library reverse-KL divergence.

Verification

Given: The hypotheses in the Example and Facts & Assumptions.

1.1A1F2givenalgebra

In the first model set $μ_{0} = 0$ , $τ_{0}^{2} = 4$ , $σ^{2} = 1$ , $n = 2$ , and $\overset{ˉ}{y} = (2 + 4) / 2 = 3$ . By [F2], the posterior variance is $(1 / 4 + 2)^{- 1} = 4 / 9$ and its mean is $(4 / 9) (0 + 2 \cdot 3) = 8 / 3$ ; the evidence is finite and positive.

1.2A1F1F3F4F5step 1.1algebra

The chosen $q_{0} = N (0, 4 / 9)$ lies in the family because $0 \in [- 1, 1]$ , while the posterior mean $8 / 3$ is outside that interval. Both Gaussian densities are strictly positive, so $q_{0}$ is supported where the posterior is positive. Their logarithms are quadratic and $q_{0}$ has finite second moment by [F4], so the absolute log-integrability required in [F1] holds. Using the common-variance density formula [F3], $\log ⁣ (\frac{q_{0} (z ∣ x)}{π (z ∣ x)}) = \frac{(z - 8 / 3)^{2} - z^{2}}{2 (4 / 9)} = - 6 z + 8.$ Taking $q_{0}$ -expectations and using [F4] gives $D_{K L} (q_{0} ∥ π) = 8$ by the directional convention [F5].

2.1A1F6step 1.2algebra

Applying [F6] to the first model, the log-evidence minus ELBO is exactly this reverse-KL value $8$ , which is strictly positive.

3.1A1F1F3F4F6algebra∎

In the second model, write $h (x) = (2 π)^{- 1 / 2} e^{- x^{2} / 2}$ and let $r$ be the $N (0, 1)$ prior density. For every $x \in R$ , [F3] gives $0 < h (x) < \infty$ and $\int r (z) d z = 1$ , so $γ (z; x) = r (z) h (x)$ has evidence $Z (x) = h (x)$ and posterior $π (z ∣ x) = r (z)$ . The constant encoder $q (z ∣ x) = r (z)$ has full support and finite second moment by [F4]; its log density and $\log γ (z; x) = \log r (z) + \log h (x)$ are integrable under $q$ by [F1]. Thus its reverse-KL is zero and [F6] gives ELBO equal to log evidence on every fibre. The decoder density is independent of $z$ , so $q (z ∣ x) = p_{θ} (z ∣ x) = p (z)$ for all $x$ , which is posterior collapse.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

66 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Alicia A. Johnson, Miles Q. Ott, and Mine Dogucu, Bayes Rules!, Chapter 5 (standard reference, not scraped)
Diederik P. Kingma and Max Welling, Auto-Encoding Variational Bayes, arXiv:1312.6114v1 (standard reference, not scraped)
Junxian He, Daniel Spokoyny, Graham Neubig, and Taylor Berg-Kirkpatrick, Lagging Inference Networks and Posterior Collapse in Variational Autoencoders (standard reference, not scraped)