Reference. Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming

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.

Cite

Cite as @moy-2025-roulette (helia, typst) · \cite{moy-2025-roulette} (LaTeX)
BibTeX
bibtex · 1 line
@article{moy-2025-roulette, title={Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming}, volume={9}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3729334}, DOI={10.1145/3729334}, number={PLDI}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Moy, Cameron and Czenszak, Jack and Li, John M. and Marshall, Brianna and Holtzen, Steven}, year={2025}, month=June, pages={2081–2105} }
hayagriva YAML (typst)
yaml · 19 lines
moy-2025-roulette:
  type: article
  title: 'Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming'
  author:
  - Moy, Cameron
  - Czenszak, Jack
  - Li, John
  - Marshall, Brianna
  - Holtzen, Steven
  date: 2025-06
  page-range: 2081-2105
  serial-number:
    doi: 10.1145/3729334
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: PLDI
    volume: 9
Cited by (2)

Type-Directed Discretization of Probabilistic Programs (Extended Version) wu-2026-type

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.
DOI · arXiv

Categorical Semantics of Probabilistic Symbolic Execution li-2026-categorical

Symbolic execution has emerged as a powerful technique for scaling exact probabilistic inference to languages with more expressive features. But, this expressivity comes at a price: probabilistic programming languages based on symbolic execution are difficult to debug, optimize, and prove correct due to the many intricacies inherent to high-performance symbolic execution strategies. We aim to make it easier to work with probabilistic symbolic executors by developing symbolic sets , a new semantic domain that cleanly captures the notion of computation underlying symbolic execution. Just as a symbolic executor replaces ordinary execution with a lifted semantics, symbolic set theory replaces ordinary set theory with a lifted mathematics : the category of symbolic sets is a Grothendieck topos, which allows type theory to be used as a metalanguage for working with symbolic sets and functions. We prove a metatheorem that shows how a large class of definitional interpreters written in the internal language of symbolic sets are automatically correct for their ordinary set-theoretic interpretations. Using this metatheorem, we give the first full correctness argument for a symbolic probabilistic language with higher-order functions, type-directed state merging, pattern matching, and structural recursion.
PDF · DOI · pldb
Cites 65 works (2 here)
With notes (2)

Super-naturals hinze-2022-super

PDF · DOI · pldb

Nominal Sets: Names and Symmetry in Computer Science pitts_nominal_sets

External (63)
moy-2025-roulette reference entries/refs/moy-2025-roulette/moy-2025-roulette.hel