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.
Predictor-corrector sampling for score SDEs
Definition
Assume the Axiom of Choice. Fix , , an integer , and an integer . Let be a continuous nonexplosive Markov diffusion on , where nonexplosive means its paths remain in on the whole interval, and Markov means its conditional future law given the past depends only on its current state. Write for its law on each Borel set . On a complete filtered probability space with the usual conditions, let be an adapted standard -dimensional Brownian motion whose increments are independent of the earlier filtration and have laws . Let and be Borel maps. The process is a continuous Brownian Itô process in the sense that, up to indistinguishability,
where the drift integrals are pathwise Lebesgue integrals and the coordinate stochastic integrals are localized Itô integrals; assume and almost surely, with . Assume also that is invertible with . Put . A transition density means that .
Assume the marginal densities and transition densities are positive, finite, and normalized with respect to Lebesgue measure; has one continuous time derivative and two continuous state derivatives. For , assume
For , define . Assume and classically. For every compactly supported smooth test, assume transition integrals and their time derivatives are absolutely integrable, differentiation under those integrals is valid, and integration by parts in space has no boundary term.
For , set and define the reverse score . With and , define the reverse drift supplied by the positive-density reversal interface:
Write for infinitely differentiable real functions with compact support. For , define . Assume that for every reverse initial law the martingale problem for has a unique nonexplosive continuous solution in law; this means that each compact-test compensated process is a local martingale and its law is unique. The current reversal supplier's proof uses AC through its Brownian-reconstruction lemma, so AC is an explicit algorithm assumption here.
Set , , , and for . Given step sizes , the predictor-corrector score-sampling algorithm takes an initial draw and mutually independent vectors , independent of . For , perform the following two operations:
-
Predictor. Compute one Euler–Maruyama step for the reverse equation:
-
Corrector. Let , so is the normalized target density . Apply one unadjusted Langevin update with step size :
Return , the finite-step state at forward time . The procedure requires an exact marginal score on and starts from the actual terminal law ; it does not replace by unless they are equal.
Definition references
The positive-density Bayes-kernel reversal theorem. Apply it with horizon to , , on the shifted filtration and with Brownian motion . Brownian increments remain independent of by the original increment hypothesis, and the shifted filtration retains the usual conditions. The shifted coefficients are and ; changing variables in the Lebesgue and elementary stochastic integrals, then passing to their localized limits, gives . Its marginal densities are and its transition densities are . Positivity, normalization, Markov identities, forward equations, uniform nonsingularity, integrability, and the assumed reverse martingale problem transfer by this deterministic time translation. Its reverse process is with natural reversed filtration , and its Bayes kernels become The supplier therefore gives precisely the displayed reverse coefficients and a Brownian driver in this reversed filtration, retaining Borel time dependence of .
The marginal score definition. It sets where the density is positive and differentiable.
The finite-dimensional Brownian convention.
The Brownian Itô-process convention. These conventions fix the increment, filtration, and localized integral assumptions used in the forward diffusion input.
The unadjusted Langevin algorithm. It supplies the one-step corrector used at each time level.
Song et al., Section 4.2 and Appendix G, Algorithm 1
Särkkä and Solin, Algorithm 8.1
Remarks
This definition supplies no sampler convergence rate, no solver error bound, and no exactness claim for the finite predictor or unadjusted Langevin corrector. The corrector need not preserve its target density at a fixed positive step size. Errors from estimated scores, choosing a positive cutoff, substituting a terminal law, discretizing the reverse equation, and numerical integration require separate bounds.
Depends on
Used by
Dependency tree · two levels
54 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
- Yang Song et al., Score-Based Generative Modeling through Stochastic Differential Equations, Section 4.2 and Appendix G (standard reference, not scraped)
- Simo Särkkä and Arno Solin, Applied Stochastic Differential Equations, Algorithm 8.1 (standard reference, not scraped)
- Alain Durmus and Éric Moulines, Non-asymptotic convergence analysis for the Unadjusted Langevin Algorithm, Section 1, equation (2) (standard reference, not scraped)
- Maxim Raginsky, Stochastic Differential Equations: A Systems-Theoretic Approach, Section 7.2 (standard reference, not scraped)