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
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.
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.
Cites 65 works (2 here)
With notes (2)
Super-naturals hinze-2022-super
Nominal Sets: Names and Symmetry in Computer Science pitts_nominal_sets
External (63)
- Artifact: Roulette (2025)
- The Rust decision diagram library (RSDD) (2025)
- Compiled, Extensible, Multi-language DSLs (Functional Pearl) (2024)
- Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting (2024)
- Scaling Integer Arithmetic in Probabilistic Programs (2023)
- Bit Blasting Probabilistic Programs (2023)
- Knowledge Compilation and More with SharpSAT-TD (2023)
- Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions (2023)
- Exact Recursive Probabilistic Programming (2022)
- A formal foundation for symbolic evaluation with merging (2022)
- Symbolic execution for randomized programs (2022)
- λPSI: exact inference for higher-order probabilistic programs (2020)
- Scaling exact inference for discrete probabilistic programs (2020)
- Fixing Code that Explodes Under Symbolic Evaluation (2020)
- SPPL: probabilistic programming with fast exact symbolic inference (2020)
- Specification and verification in the field: applying formal methods to BPF just-in-time compilers in the Linux kernel (2020)
- Scalable verification of probabilistic networks (2019)
- Finding code that explodes under symbolic evaluation (2018)
- The reasoned schemer (2nd edition) (2018)
- An Exhaustive DPLL Algorithm for Model Counting (2018)
- Delayed sampling and automatic Rao-Blackwellization of probabilistic programs (2018)
- Contextual equivalence for a probabilistic language with continuous random variables and recursion (2018)
- Symbolic types for lenient symbolic execution (2017)
- Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring (2017)
- A Simple Complete Search for Logic Programming (2017)
- An Improved Decision-DNNF Compiler (2017)
- Cosette: an automated prover for SQL (2017)
- PSI: Exact Symbolic Inference for Probabilistic Programs (2016)
- Probabilistic Inference by Program Transformation in Hakaru (System Description) (2016)
- Functional Big-Step Semantics (2016)
- Scaling up Superoptimization (2016)
- Scalable verification of border gateway protocol configurations with an SMT solver (2016)
- Solving PPPP-complete problems using knowledge compilation (2016)
- A top-down compiler for sentential decision diagrams (2015)
- A lightweight symbolic virtual machine for solver-aided host languages (2014)
- Probabilistic Relational Reasoning for Differential Privacy (2013)
- Compiling Probabilistic Graphical Models Using Sentential Decision Diagrams (2013)
- Growing solver-aided languages with rosette (2013)
- μKanren: a minimal functional core for relational programming (2013)
- Probabilistic symbolic execution (2012)
- Dsharp: Fast d-DNNF Compilation with sharpSAT (2012)
- Reference: Racket (PLT-TR-2010-1) (2010)
- The art of computer programming, volume 4 (2009)
- Relational programming in miniKanren: techniques, applications, and implementations (2009)
- On probabilistic inference by weighted model counting (2008)
- Z3: An Efficient SMT Solver (2008)
- ProbLog: a probabilistic Prolog and its application in link discovery (2007)
- Performing Bayesian inference by weighted model counting (2005)
- A Knowledge Compilation Map (2002)
- A compiler for deterministic, decomposable negation normal form (2002)
- CUDD: CU decision diagram package (1998)
- Probabilistic Datalog—a logic for powerful retrieval methods (1995)
- On the Hardness of Approximate Reasoning (1993)
- A tutorial on hidden Markov models and selected applications in speech recognition (1989)
- What About the Natural Numbers? (1989)
- Natural Semantics (1987)
- Bayesian networks: a model of self-activated memory for evidential reasoning (1985)
- 10.5591/978-1-57735-516-8/ijcai11-143
- 10.1017/s1471068414000076
- 10.1145/3296979.3192400
- 10.1016/0890-5401(92)90061-j
- 10.1007/978-3-319-41540-6_2
- 10.1007/978-3-031-43835-6_23