TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

Posterior of a finite masking chain

Statement

Let $V$ be a finite nonempty vocabulary, let $m \notin V$ , let $L, N \geq 1$ , and let $1 = α_{0} > α_{1} > \dots > α_{N} = 0$ be the survival schedule of the finite masking chain. Fix a clean sequence $x \in V^{L}$ and grid indices $0 \leq s < t \leq N$ . For every state $z_{t} \in (V \cup {m})^{L}$ with $\Pr (Z_{t} = z_{t} ∣ X = x) > 0$ , the conditional law of $Z_{s}$ given $X = x, Z_{t} = z_{t}$ is a product over coordinates. At coordinate $i$ , if $z_{t, i} \in V$ , then $Z_{s, i} = z_{t, i}$ with probability one. If $z_{t, i} = m$ , then, with $c_{s, t} = (α_{s} - α_{t}) / (1 - α_{t})$ , the only possible values are $x_{i}$ and $m$ , with probabilities $\Pr (Z_{s, i} = x_{i} ∣ X = x, Z_{t, i} = m) = c_{s, t}, \Pr (Z_{s, i} = m ∣ X = x, Z_{t, i} = m) = \frac{1 - α_{s}}{1 - α_{t}} .$ The denominator is positive because $t \geq 1$ implies $α_{t} < 1$ ; at $s = 0$ the mask posterior has zero mass.

Statement references

Finite masking diffusion chain: conditional on $X = x$ , coordinates and masking draws are independent, clean tokens never change, and $m$ is absorbing.

Facts & Assumptions

Given: The finite masking chain, a fixed clean string $x$ , grid indices $0 \leq s < t \leq N$ , and a state $z_{t}$ with positive conditional probability given $X = x$ . Prove the displayed product posterior.

[F1]

Finite masking diffusion chain: at step $j$ , a clean token survives with probability $r_{j} = α_{j} / α_{j - 1}$ , the mask is absorbing, and corruption factors over positions conditional on the clean string.

[F2]

Finite masking-chain transitions define a probability law: the finite path mass is a normalized probability law.

Proof

1.1givenF1F2algebra

For one coordinate, the probability of surviving all steps through $s$ is $\prod_{j = 1}^{s} r_{j} = α_{s}$ , with the empty product equal to one when $s = 0$ . Survival through $t$ has probability $α_{t}$ . Since the mask is absorbing, the event “clean at $s$ and masked at $t$ ” has probability $α_{s} - α_{t}$ , while “masked at $t$ ” has probability $1 - α_{t}$ . The latter is positive for $t \geq 1$ . Dividing these finite event probabilities gives the two displayed conditional masses, which sum to one.

2.1F1F2step 1.1algebra

If $z_{t, i} \in V$ , positive conditional probability forces $z_{t, i} = x_{i}$ ; the token could not have changed or been unmasked after masking, so its earlier value is the same. If $z_{t, i} = m$ , step 1.1 gives the two possible earlier values and their probabilities. By [F1], conditional on $x$ the coordinate paths are independent; conditioning on the coordinatewise event $Z_{t} = z_{t}$ therefore leaves the coordinate posterior laws independent, and their product is the asserted full conditional law.

3.1givenF1step 1.1algebra∎

The strict schedule gives $0 < c_{s, t} \leq 1$ and $1 - c_{s, t} = (1 - α_{s}) / (1 - α_{t})$ . At $s = 0$ , $c_{s, t} = 1$ ; at $t = N$ , $α_{t} = 0$ and the denominator is one. Thus the formula covers both endpoints without conditioning on the zero-probability event $Z_{0} = m$ .

Depends on

Used by

A factorized reverse kernel fails for correlated tokens Counterexample
One-token posterior on a finite mask schedule Example
Finite masking path law factors backward by its posterior rows Lemma
Factorization and finite-endpoint warnings Remark
Masked-diffusion KL reduces to weighted cross-entropy Theorem

Dependency tree · two levels

3 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

Subham Sekhar Sahoo et al., Simple and Effective Masked Diffusion Language Models, arXiv v1 (standard reference, not scraped)
Jacob Austin et al., Structured Denoising Diffusion Models in Discrete State-Spaces (standard reference, not scraped)