Reference. Type-Directed Discretization of Probabilistic Programs (Extended Version)
We study exact discretization as a semantics-preserving transformation for recursive, higher-order probabilistic programs with continuous distributions. We target programs where continuous values are compared against finitely many constants, so exact inference reduces to a discrete problem. Our central technical contribution is a non-local, type-directed analysis that infers where continuous values can be partitioned into finitely many observationally relevant regions, then rewrites sampling and comparison behavior over those regions. We call this transformation Slice. Because this construction is global and type-directed, correctness requires reasoning beyond the local syntax: we formalize the transformation and prove soundness for boolean queries using a coupling-style logical relations argument over operational semantics. As an application, transformed programs can be executed by discrete engines such as Dice, Roulette, and Storm. Our empirical evaluation shows two complementary strengths of Slice when paired with discrete backends: it enables exact inference for challenging continuous programs that lie beyond the reach of previous exact systems, and, on benchmarks where direct comparison is possible, it is competitive with state-of-the-art exact inference systems for continuous programs.
Cite
Cites 52 works (1 here)
With notes (1)
Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming moy-2025-roulette
Exact probabilistic inference is a requirement for many applications of probabilistic programming languages (PPLs) such as in high-consequence settings or verification. However, designing and implementing a PPL with scalable high-performance exact inference is difficult: exact inference engines, much like SAT solvers, are intricate low-level programs that are hard to implement. Due to this implementation challenge, PPLs that support scalable exact inference are restrictive and lack many features of general-purpose languages. This paper presents Roulette, the first discrete probabilistic programming language that combines high-performance exact inference with general-purpose language features. Roulette supports a significant subset of Racket, including data structures, first-class functions, surely-terminating recursion, mutable state, modules, and macros, along with probabilistic features such as finitely supported discrete random variables, conditioning, and top-level inference. The key insight is that there is a close connection between exact probabilistic inference and the symbolic evaluation strategy of Rosette. Building on this connection, Roulette generalizes and extends the Rosette solver-aided programming system to reason about probabilistic rather than symbolic quantities. We prove Roulette sound by generalizing a proof of correctness for Rosette to handle probabilities, and demonstrate its scalability and expressivity on a number of examples.
External (51)
- Artifact: Type-Directed Discretization of Probabilistic Programs (2026)
- Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back (2025)
- Stochastic Lazy Knowledge Compilation for Inference in Discrete Probabilistic Programs (2025)
- Compiling with Generating Functions (2025)
- Bit Blasting Probabilistic Programs (2024)
- Exact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions (2024)
- Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving (2024)
- Exact Recursive Probabilistic Programming (2023)
- A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version) (2023)
- Exact Bayesian Inference on Discrete Models via Probability Generating Functions: A Probabilistic Programming Approach (2023)
- Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming (2022)
- Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion (2022)
- AQUA: Automated Quantized Inference for Probabilistic Programs (2021)
- Paradoxes of Probabilistic Programming: And How to Condition on Events of Measure Zero with Infinitesimal Probabilities (2021)
- SPPL: Probabilistic Programming with Fast Exact Symbolic Inference (2021)
- 𝜆PSI: Exact Inference for Higher-Order Probabilistic Programs (2020)
- Scaling Exact Inference for Discrete Probabilistic Programs (2020)
- Continualization of Probabilistic Programs With Correction (2020)
- Bean Machine: A Declarative Probabilistic Programming Language for Efficient Programmable Inference (2020)
- Pyro: Deep Universal Probabilistic Programming (2019)
- Gen: A General-Purpose Probabilistic Programming System with Programmable Inference (2019)
- Exact and Approximate Weighted Model Integration with Probability Density Functions Using Knowledge Compilation (2019)
- Turing: A Language for Flexible Probabilistic Inference (2018)
- Sound Abstraction and Decomposition of Probabilistic Programs (2018)
- Infer.NET 0.3 (2018)
- Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion (2018)
- Discrete-Continuous Mixtures in Probabilistic Programming: Generalized Semantics and Inference Algorithms (2018)
- FairSquare: Probabilistic Verification of Program Fairness (2017)
- Stan: A Probabilistic Programming Language (2017)
- Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring (2017)
- A Storm is Coming: A Modern Probabilistic Model Checker (2017)
- PSI: Exact Symbolic Inference for Probabilistic Programs (2016)
- Bounded Model Checking for Probabilistic Programs (2016)
- Probabilistic Inference by Program Transformation in Hakaru (System Description) (2016)
- Probabilistic Programming in Python Using PyMC3 (2016)
- Design and Implementation of Probabilistic Programming Language Anglican (2016)
- Edward: A Library for Probabilistic Modeling, Inference, and Criticism (2016)
- Probabilistic Inference in Hybrid Domains by Weighted Model Integration (2015)
- Step-Indexed Logical Relations for Probability (2015)
- The Design and Implementation of Probabilistic Programming Languages (2014)
- Bayesian Inference Using Data Flow Analysis (2013)
- An Introduction to Measure Theory (1st ed.) (2011)
- GNU Scientific Library Reference Manual (3rd ed.) (2009)
- Figaro: An Object-Oriented Probabilistic Programming Language (2009)
- Church: A Language for Generative Models (2008)
- ProbLog: A Probabilistic Prolog and Its Application in Link Discovery (2007)
- Real Analysis: Measure Theory, Integration, and Hilbert Spaces (1st ed.) (2005)
- Topology (2nd ed.) (2000)
- Type Inference with Constrained Types (1999)
- Foundations of Modern Probability (1997)
- Space/Time Trade-offs in Hash Coding with Allowable Errors (1970)