TheoremStatement: Literature-sourcedProof: 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.

Dominated pathwise differentiation for VAE training

Statement

Let $X = (x_{1}, \dots, x_{N})$ be a fixed nonempty finite data set, let $Λ$ be an open subset of a finite-dimensional Euclidean parameter space for $η = (θ, ϕ)$ , and fix $η_{0} = (θ_{0}, ϕ_{0}) \in Λ$ . For each $i$ , assume the VAE at $(η, x_{i})$ is admissible and has a pathwise representation $g_{ϕ} (ϵ, x_{i})$ under one parameter-independent probability law $ρ$ . Assume there is one $ρ$ -null set, common to every $i$ and $η \in Λ$ , outside which $0 < q_{ϕ} (g_{ϕ} (ϵ, x_{i}) ∣ x_{i}) < \infty$ and $0 < γ_{θ} (g_{ϕ} (ϵ, x_{i}); x_{i}) < \infty$ ; define the payoff below to be zero on that null set. Define $H_{i} (η, ϵ) : = \log γ_{θ} (g_{ϕ} (ϵ, x_{i}); x_{i}) - \log q_{ϕ} (g_{ϕ} (ϵ, x_{i}) ∣ x_{i}),$ with terms on a common $ρ$ -null set defined to be zero. Assume each $H_{i}$ is jointly measurable and integrable for every $η \in Λ$ . Outside one $ρ$ -null set, each $H_{i} (\cdot, ϵ)$ is continuously differentiable on $Λ$ with continuous gradient, and $\nabla_{η} H_{i} (η, \cdot)$ is measurable for every $η$ . For every compact neighborhood $K \subset Λ$ of $η_{0}$ , assume one nonnegative $M_{i, K} \in L^{1} (ρ)$ satisfies $∥ \nabla_{η} H_{i} (η, ϵ) ∥_{2} \leq M_{i, K} (ϵ)$ for every $η \in K$ outside one common null set, and assume $E_{ρ} ∥ \nabla_{η} H_{i} (η_{0}, ϵ) ∥_{2}^{2} < \infty$ .

Let $I$ be uniform on ${1, \dots, N}$ and independent of $ϵ \sim ρ$ . Then the finite-average objective $\overline{L} (η) : = \frac{1}{N} \sum_{i = 1}^{N} {ELBO}_{θ, ϕ} (x_{i})$ is differentiable at $η_{0}$ , and its one-example pathwise gradient estimate $G (η_{0}, I, ϵ) : = \nabla_{η} H_{I} (η_{0}, ϵ)$ satisfies $E [G (η_{0}, I, ϵ)] = \nabla_{η} \overline{L} (η_{0})$ and has finite coordinate variances. A parameter-independent Gaussian base law alone does not imply the differentiability, envelope, or second-moment hypotheses.

Statement references

The VAE ELBO and fixed-law encoder representation.

The published pathwise simulation-gradient theorem with a common integrable derivative envelope.

Dominated convergence used in the difference-quotient proof.

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

Blei, Kucukelbir, and McAuliffe, Variational Inference: A Review for Statisticians.

Zheng, Hu, and Deng, 10-708 Lecture 13: Variational Inference II.

Facts & Assumptions

Given: A finite nonempty data set, the admissible VAE densities and fixed-law pathwise representations at each data point, the stated local sample-path regularity and common integrable derivative envelopes, and square-integrable pathwise gradients at $η_{0}$ .

[F1]

Variational autoencoder model, encoder, and ELBO: the ELBO is the $q_{ϕ} (\cdot ∣ x)$ -expectation of $\log γ_{θ} (z; x) - \log q_{ϕ} (z ∣ x)$ , and the law of $g_{ϕ} (ϵ, x)$ under $ρ$ has density $q_{ϕ} (\cdot ∣ x)$ relative to $μ_{Z}$ .

[F2]

Simulation objectives and unbiased payoff oracles: a simulation payoff is jointly measurable and integrable at every parameter, and its objective is its expectation under the fixed probability law.

[F3]

Pathwise and reparameterized simulation-gradient estimators: for a fixed random input, the pathwise estimator is the pointwise derivative of the simulated payoff; this definition alone does not imply unbiasedness.

[F4]

A dominated pathwise simulation gradient is unbiased: for an integrable simulation payoff with almost-sure C1 sample paths, continuous measurable gradients, one common integrable gradient envelope on a neighborhood, and a square-integrable gradient at the base parameter, the objective is differentiable there and its gradient is the expectation of the pathwise gradient; each coordinate then has finite variance.

[F5]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : along a parameter segment, the assumed differentiability of the full payoff gives $\frac{d}{d t} H_{i} (η + t v, ϵ) = D_{η} H_{i} (η + t v, ϵ) [v]$ . No separate differentiability of the sampler or log-density factors is assumed.

[F6]

Dominated convergence: almost-everywhere convergence under one integrable majorant permits passage of the limit through the integral.

Proof

1.1givenF1F2F3

Fix $i$ . By [F3], $G_{i} (η, ϵ) : = \nabla_{η} H_{i} (η, ϵ)$ is the fixed-noise pathwise estimator. The pushforward condition in [F1] gives $E_{ρ} H_{i} (η, ϵ) = {ELBO}_{θ, ϕ} (x_{i})$ for every $η$ . The absolute log-integrability in the VAE definition makes $H_{i}$ integrable; its joint measurability and integrability therefore meet the payoff conditions in [F2].

2.1givenF4F5F6step 1.1

Since $Λ$ is open, choose a closed ball $K$ centered at $η_{0}$ with $K \subset Λ$ and nonempty interior. The common envelope assumed on $K$ is an integrable majorant on an open neighborhood of $η_{0}$ ; the C1, continuity, measurability and square-integrability hypotheses are exactly those of [F4]. The full proof of [F4] applies the chain rule along parameter segments and then [F6] to the first-order difference quotients under this majorant. It gives $\nabla_{η} {ELBO}_{θ, ϕ} (x_{i}) ∣_{η_{0}} = E_{ρ} \nabla_{η} H_{i} (η_{0}, ϵ)$ and finite coordinate variances.

3.1givenstep 2.1algebra∎

The finite sum defining $\overline{L}$ is differentiable at $η_{0}$ with gradient the average of these $N$ gradients. Independence and uniformity of $I$ give $E [G] = N^{- 1} \sum_{i = 1}^{N} E_{ρ} \nabla_{η} H_{i} (η_{0}, ϵ)$ , which is that average gradient. The finite mixture of the stated square-integrable gradients has finite second moment in each coordinate and therefore finite coordinate variance.

Depends on

Used by

Dependency tree · two levels

29 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

Diederik P. Kingma and Max Welling, Auto-Encoding Variational Bayes, arXiv:1312.6114v1 (standard reference, not scraped)
David M. Blei, Alp Kucukelbir, and Jon D. McAuliffe, Variational Inference: A Review for Statisticians (standard reference, not scraped)
Ronghuo Zheng, Zhiting Hu, and Yuntian Deng, 10-708 Probabilistic Graphical Models, Lecture 13: Variational Inference II (standard reference, not scraped)