Uploaded July 2026 | Updated September 2026, 5 hours ago
Carl Friedrich von Weizsäcker Colloquium - July 15, 2026
In probabilistic programming users can delegate choices to be made during computation to external random events, like the rolling of a dice. In some situations, this leads to finding, quickly and with high probability, solutions that it would otherwise be very hard to find by a purely deterministic approach. At the same time, the analysis of probabilistic programs is often difficult, since one has to consider all possible computational trajectories, giving rise to complex combinatorial spaces. In particular, from a logical point of view, while properties of deterministic programs like termination are notoriously undecidable, verifying the corresponding properties of probabilistic programs is often an even "more undecidable" problem (i.e. placed strictly higher in the arithmetical hierarchy).
In this presentation we use ideas coming from combinatorics and linear logic to investigate the intrinsic complexity of verifying termination properties of probabilistic programs. We focus on three problems: determining if a program terminates with probability 1, if its expected running time is finite, and predicting its most likely execution paths. Notably, by relying on well-known classifications of generating functions in combinatorics, we introduce corresponding classifications of programs with respect to the (un)decidability of these three problems.
Carl Friedrich von Weizsäcker Colloquium - July 15, 2026
In probabilistic programming users can delegate choices to be made during computation to external random events, like the rolling of a dice. In some situations, this leads to finding, quickly and with high probability, solutions that it would otherwise be very hard to find by a purely deterministic approach. At the same time, the analysis of probabilistic programs is often difficult, since one has to consider all possible computational trajectories, giving rise to complex combinatorial spaces. In particular, from a logical point of view, while properties of deterministic programs like termination are notoriously undecidable, verifying the corresponding properties of probabilistic programs is often an even "more undecidable" problem (i.e. placed strictly higher in the arithmetical hierarchy).
In this presentation we use ideas coming from combinatorics and linear logic to investigate the intrinsic complexity of verifying termination properties of probabilistic programs. We focus on three problems: determining if a program terminates with probability 1, if its expected running time is finite, and predicting its most likely execution paths. Notably, by relying on well-known classifications of generating functions in combinatorics, we introduce corresponding classifications of programs with respect to the (un)decidability of these three problems.
