Alphabeta Math
AlgorithmAlgorithm: Literature-sourcedProof: Not applicablePipeline-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.

Predictor-corrector sampling for score SDEs

Definition

Assume the Axiom of Choice. Fix T>0, 0<ϵ<T, an integer d≥1, and an integer N≥1. Let Xt∈Rd be a continuous nonexplosive Markov diffusion on [ϵ,T], where nonexplosive means its paths remain in Rd on the whole interval, and Markov means its conditional future law given the past depends only on its current state. Write Pt(A)=P(Xt∈A) for its law on each Borel set A. On a complete filtered probability space with the usual conditions, let W be an adapted standard d-dimensional Brownian motion whose increments are independent of the earlier filtration and have laws Nd(0,(t−s)Id). Let bt(x)∈Rd and σt(x)∈Rd×d be Borel maps. The process is a continuous Brownian Itô process in the sense that, up to indistinguishability,

Xt=Xϵ+∫ϵtbr(Xr) dr+(∑j=1d∫ϵtσij(r,Xr) dWrj)i=1d,

where the drift integrals are pathwise Lebesgue integrals and the coordinate stochastic integrals are localized Itô integrals; assume ∫ϵT∣br(Xr)∣ dr<∞ and ∫ϵT∥σr(Xr)∥F2 dr<∞ almost surely, with ∥M∥F2=∑i,j∣Mij∣2. Assume also that σt(x) is invertible with sup⁡t,x∥σt(x)−1∥<∞. Put at(x)=σt(x)σt(x)T. A transition density q(s,x;t,y) means that P(Xt∈dy∣Xs=x)=q(s,x;t,y) dy.

Assume the marginal densities pt and transition densities q(s,x;t,y) are positive, finite, and normalized with respect to Lebesgue measure; pt has one continuous time derivative and two continuous state derivatives. For ϵ≤s<t≤T, assume

pt(y)=∫Rdps(x)q(s,x;t,y) dx,q(s,x;t,y)=∫Rdq(s,x;r,z)q(r,z;t,y) dz(s<r<t).

For Ltϕ=bt⋅∇ϕ+12∑i,jat,ij∂i∂jϕ, define Lt∗r=−∑i∂i(bt,ir)+12∑i,j∂i∂j(at,ijr). Assume ∂tpt=Lt∗pt and ∂tq(s,x;t,y)=Lt∗,yq(s,x;t,y) 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 0≤u<T−ϵ, set s=T−u and define the reverse score ss(x)=∇xlog⁡ps(x). With a=σσT and (∇ ⁣⋅a)i=∑j∂jaij, define the reverse drift supplied by the positive-density reversal interface:

b~u(x)=−bT−u(x)+(∇ ⁣⋅aT−u)(x)+aT−u(x)sT−u(x),σ~u(x)=σT−u(x).

Write Cc∞(Rd) for infinitely differentiable real functions with compact support. For ϕ∈Cc∞(Rd), define L~uϕ=b~u⋅∇ϕ+12∑i,jaT−u,ij∂i∂jϕ. Assume that for every reverse initial law the martingale problem for L~u has a unique nonexplosive continuous solution in law; this means that each compact-test compensated process ϕ(Yu)−ϕ(Y0)−∫0uL~rϕ(Yr) dr 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 S=T−ϵ, h=S/N, uk=kh, and tk=T−uk for 0≤k≤N. Given step sizes ηk>0, the predictor-corrector score-sampling algorithm takes an initial draw Y0∼PT and mutually independent vectors Gk,ξk∼Nd(0,Id), independent of Y0. For k=0,…,N−1, perform the following two operations:

  1. Predictor. Compute one Euler–Maruyama step for the reverse equation: Y^k+1=Yk+hb~uk(Yk)+h σ~uk(Yk)Gk.

  2. Corrector. Let Uk+1(x)=−log⁡ptk+1(x), so e−Uk+1 is the normalized target density ptk+1. Apply one unadjusted Langevin update with step size ηk: Yk+1=Y^k+1−ηk∇Uk+1(Y^k+1)+2ηk ξk=Y^k+1+ηkstk+1(Y^k+1)+2ηk ξk.

Return YN, the finite-step state at forward time ϵ. The procedure requires an exact marginal score on [ϵ,T] and starts from the actual terminal law PT; it does not replace PT by Nd(0,Id) unless they are equal.

Definition references

The positive-density Bayes-kernel reversal theorem. Apply it with horizon S=T−ϵ to X‾r=Xϵ+r, 0≤r≤S, on the shifted filtration F‾r=Fϵ+r and with Brownian motion W‾r=Wϵ+r−Wϵ. Brownian increments remain independent of F‾r by the original increment hypothesis, and the shifted filtration retains the usual conditions. The shifted coefficients are b‾r(x)=bϵ+r(x) and σ‾r(x)=σϵ+r(x); changing variables in the Lebesgue and elementary stochastic integrals, then passing to their localized limits, gives dX‾r=b‾r(X‾r)dr+σ‾r(X‾r)dW‾r. Its marginal densities are p‾r=pϵ+r and its transition densities are q‾(r,x;s,y)=q(ϵ+r,x;ϵ+s,y). 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 X‾S−u=XT−u with natural reversed filtration Gu=σ(XT−v:0≤v≤u), and its Bayes kernels become K‾u,v(y,dx)=pT−v(x)q(T−v,x;T−u,y)pT−u(y)dx,0≤u<v≤S. 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 st(x)=∇xlog⁡pt(x) 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

Durmus and Moulines, Section 1, equation (2)

Raginsky, Section 7.2

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