Analysis of probabilistic programs using generating functions

Klinkenberg, Lutz; Kovacs, Laura; Katoen, Joost-Pieter

doi:44622

Analysis of probabilistic programs using generating functions

Klinkenberg, Lutz^RWTH*

2025

Verantwortlichkeitsangabevorgelegt von Lutz Klinkenberg, M. Sc.

ImpressumAachen : RWTH Aachen University 2025

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2025

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Kovacs, Laura (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2025-06-20

Online
DOI: 10.18154/RWTH-2025-07571
URL: https://publications.rwth-aachen.de/record/1017915/files/1017915.pdf

Einrichtungen

Projekte

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Probabilistische Programmiersprachen haben sich als ein leistungsstarkes Werkzeug zur Modellierung komplexer und unsicherer Systeme etabliert. Sie finden breite Anwendung in Bereichen wie Künstliche Intelligenz, maschinelles Lernen und Robotik, aber auch in nicht-technischen Disziplinen wie etwa Gesundheits- wesen, Sozial- und Klimawissenschaften, Wirtschaft und Psychologie. Diese Sprachen ermöglichen es, probabilistische Prozesse präzise abzubilden, ein- schließlich solcher, die Schleifen, Rekursion und andere komplexe Strukturen enthalten. Allerdings stellt die Analyse derartiger Programme, insbesondere je- ne mit unendlichen Schleifen oder nicht-terminierendem Verhalten, erhebliche Herausforderungen dar. Diese Dissertation stellt einen neuartigen Ansatz zur Bewältigung dieser Herausforderungen vor, indem sie eine denotationelle Semantik mittels Wahrscheinlichkeit erzeugenden Funktionen (PGF) für diskrete probabilistische Programme mit Schleifen entwickelt. Diese Semantik bietet eine exakte und kompakte Darstellung von Programmverhalten und ermöglicht darüber hinaus exakte Bayesianische Inferenz, während bisherige Methoden oft auf Approximationen angewiesen waren. Ein zentraler Beitrag dieser Arbeit ist die Einführung invarianten-basierter Beweistechniken, die die systematische Ableitung von Posteriorverteilungen erleichtern und dadurch Eigenschaften wie Erwartungswerte und Momente höherer Ordnung auch für potenziell unbeschränkte Schleifen zugänglich machen. Darüber hinaus präsentieren wir eine syntaktische Charakterisierung einer Klasse von probabilistischen Programmen, für die die von ihnen beschriebenen Verteilungen als rationale geschlossene Formen von erzeugenden Funktionen ausgedrückt werden können. Diese Charakterisierung gewährleistet, dass exakte Inferenz innerhalb dieser Klasse erhalten bleibt, wodurch effiziente algebraische Manipulationen und direkte Berechnungen von Größen wie Schwanzabschätzungen und Momenten ermöglicht werden. Durch die Verknüpfung der Programmsyntax mit der algebraischen Zugänglichkeit ihrer Semantik etabliert diese Arbeit einen grundlegenden Rahmen für exakte Analysen von probabilistischen Programmen. Dieser Rahmen erweitert nicht nur die Möglichkeiten für exakte Bayesian Inferenz und unterstützt Entscheidungsfindung unter Unsicherheit, sondern erhöht auch die Anwendbarkeit probabilistischer Programmierung auf Bereiche, in denen formale Verifikation unverzichtbar ist. Er kombiniert theoretische Präzision mit praktischer Nutzbarkeit und bietet eine einheitliche Perspektive auf die Struktur und das Verhalten diskreter probabilistischer Programme.

Probabilistic programming languages have emerged as a powerful tool for modeling complex and uncertain systems. Widely applied in fields like artificial intelligence, machine learning, robotics but also in non-technical domains as, e.g., healthcare, social and climate sciences, economic and psychology, these languages allow us to succinctly represent probabilistic processes, including those involving loops, recursion, and other intricate structures. However, reasoning about such programs, particularly those with infinite loops or non- terminating behavior, poses significant challenges. This dissertation introduces a novel approach to address these challenges by developing a denotational probability generating function (PGF) semantics for discrete probabilistic programs with loops. This semantics provides an exact and compact representation of program behaviors, enabling exact Bayesian inference where prior methods often relied on approximations. A central contribution of this work is the introduction of invariant-based reasoning techniques, which facilitate the systematic derivation of posterior distributions and hence also properties like expectations and higher-order moments, even for possibly unbounded loops. Furthermore, we present a syntactic characterization of a class of probabilistic programs for which the distributions they describe can be expressed as rational closed form generating functions. This characterization ensures that exact inference is preserved within this class, allowing for efficient algebraic manipulation and direct computation of quantities such as tail bounds and moments. By linking program syntax to the algebraic tractability of their semantics, this work establishes a foundational framework for exact reasoning in probabilistic programming. This framework not only enhances the capacity for exact Bayesian inference enabling decision-making under uncertainty but also broadens the applicability of probabilistic programming to domains where formal verification is inevitable. It combines theoretical rigor with practical utility, offering a unified perspective on the structure and behavior of discrete probabilistic programs.

OpenAccess:
PDF
(additional files)