CoreDPPL: Towards a Sound Composition of Differentiation, ODE Solving, and Probabilistic Programming

TL;DR

CoreDPPL tackles safe composition of differentiation, ODE solving, and probabilistic programming by introducing a higher‑order core language with a static effect/coeffect type system and a dynamic semantics. It provides formal semantics, mechanized Agda proofs of type safety, and a practical implementation extended from CorePPL, complemented by three case studies (ODE sensitivities, Random ODEs, and Bayesian parameter estimation). The key contributions include distinguishing analytic versus PAP differentiation, tracking randomness, and ensuring that deterministically typed terms do not affect random state. The work demonstrates that complex models mixing ODEs, AD, and probabilistic inference can be safely composed and executed, with future directions toward DAEs and richer domain analyses.

Abstract

In recent years, there has been extensive research on how to extend general-purpose programming language semantics with domain-specific modeling constructs. Two areas of particular interest are (i) universal probabilistic programming where Bayesian probabilistic models are encoded as programs, and (ii) differentiable programming where differentiation operators are first class or differential equations are part of the language semantics. These kinds of languages and their language constructs are usually studied separately or composed in restrictive ways. In this paper, we study and formalize the combination of probabilistic programming constructs, first-class differentiation, and ordinary differential equations in a higher-order setting. We propose formal semantics for a core of such differentiable probabilistic programming language (DPPL), where the type system tracks random computations and rejects unsafe compositions during type checking. The semantics and its type system are formalized, mechanized, and proven sound in Agda with respect to abstract language constructs.

Figures (9)

• Figure 1: Overview of examples illustrating the compositions of $\mathbf{diff}_{}$, $\mathbf{solve}$, and the probabilistic constructs (prob): $\mathbf{infer}$, $\mathbf{assume}$, and $\mathbf{weight}$. The direction of the arrows gives a notion of nesting where the arrow points to the nested (inner) construct.
• Figure 2: Left: a probabilistic model in our CorePPL language, based on Miking CorePPL, that includes parameter estimation from noisy data for a dynamical system as well as ODE sensitivity computation by program differentiation. Right: a graph of the distribution of traces for the sensitivity of the density of prey (blue) and the trace of the sensitivity for the true value of $\theta=1.5$ (dashed white) over time ($x$). The shade of blue is proportional to the probability of a particular trace (darker means more probable).
• Figure 3: The syntax of CoreDPPL.
• Figure 4: Type environment, operations over effects and coeffects, and the sub-typing relation.
• Figure 5: Type rules for CoreDPPL.

Theorems & Definitions (11)

• Definition 4.1
• Definition 4.2
• Definition 4.3
• Theorem 5.1: Progress $\textsc{Det}{}$
• Theorem 5.2: Preservation $\textsc{Det}{}$
• Theorem 5.3: Progress $\textsc{Rnd}{}$
• Theorem 5.4: Preservation $\textsc{Rnd}{}$
• Theorem 5.5: Type Safety
• Theorem 5.6: Determinism $\textsc{Det}{}$
• Theorem 5.7: Determinism $\textsc{Rnd}{}$