Exact inference for probabilistic loops

Abstract

Die probabilistische Programmierung erleichtert die Entwicklung und Analyse von statistischen Modellen erheblich. Lediglich mithilfe einer Beschreibung des statistischen Prozesses können algorithmische Ansätze oft vollautomatisch tiefgehende Einblicke in den modellierten Vorgang geben und ermöglichen es somit dem Benutzer Inferenzen durchzuführen, d. h. Schlussfolgerungen aus beobachteten Daten zu ziehen. Allerdings ist exakte Programmanalyse in der Gegenwart von Schleifen schon bei herkömmlichen deterministischen Programmen eine notorisch schwierige Aufgabe. Um dennoch rigorose Analyseergebnisse zu gewährleisten, ist es notwendig, maßgeschneiderte Ansätze für strukturell eingeschränkte Programme und Schleifen zu entwickeln. In dieser Arbeit entwickeln wir mehrere Techniken, für die automatischen Analyse von probabilistischen Schleifen. Um Inferenz in probabilistischen Programmen durchzuführen, ist es notwendig, Informationen über die Wahrscheinlichkeitsverteilung, die durch das Programm spezifiziert wird, zu extrahieren. Um die modellierte Verteilung zu berechnen, stellen wir eine korrekte und vollständige Methode für Programme und Schleifen über endlichen Zustandsräumen vor und ermöglichen eine vollständige Automatisierung in unserem neuen Tool Blizzard. Für probabilistische Programme über unendlichen Zustandsräumen stellen wir eine Methode vor, mit der eine beschränkte Klasse von Programmen durch äquivalente, schleifenfreie Programme ersetzt werden kann. Darüber hinaus stellen wir maßgeschneiderte Techniken vor, die auf erzeugenden Funktionen basieren, und zeigen, dass Typsysteme geeignet sind, um die Verteilungen von Variablen in probabilistischen Schleifen zu identifizieren. Dennoch sind einige Probleme bei der Analyse probabilistischer Programme nachweislich nicht entscheidbar. In dieser Arbeit untersuchen wir die Grenze der Entscheidbarkeit, indem wir das Problem der Invarianten-Synthese für probabilistische Programme untersuchen. Wir stellen bestehende, nicht-probabilistische Ergebnisse vor und geben korrespondierende Beweise für probabilistische Programme. Unter anderem präsentieren wir eine bisher unbekannte Beziehung zwischen dem Problem der Invarianten-Synthese und dem Skolem-Problem, einem schwierigen ungelösten Problem der Zahlentheorie. Mit den vorgestellten Techniken bringen wir den Stand der Technik in der probabilistischen Schleifenanalyse voran und ermöglichen exakte Analyse und Inferenz für eine neue Klasse von probabilistischen Programmen und Schleifen.

Probabilistic programming greatly facilitates the development and analysis of statistical models. By providing merely a description of the process, algorithmic approaches can often fully automatically derive deep insights into the modelled process and allow the user to perform inference, that is, to draw conclusions from observed data. However, performing exact program analysis in the presence of loops is a notoriously hard task, already for traditional deterministic programs. To still provide rigorous analysis results, it is necessary to provide tailored approaches for structurally restricted programs and loops. In this thesis, we develop several techniques that tackle the problem of automatically inferring properties of probabilistic loops. To perform inference on probabilistic programs, it is necessary to obtain information about the probability distribution that is specified by the program. To extract the modelled distribution, we present a sound and complete method for programs and loops over a finite state-space and provide full automation in our new tool Blizzard. For infinite-state probabilistic programs, we present an approach that is able to replace a restricted class of programs with equivalent, loop-free programs. Moreover, we present tailored techniques based on generating functions and show that type systems are well-suited to identify the distributions of variables in probabilistic loops. Nevertheless, some problems in the analysis of probabilistic programs provably cannot be answered. In this thesis, we investigate the boundary of decidability by studying the problem of invariant synthesis for probabilistic programs. We present existing, non-probabilistic results and give corresponding proofs for probabilistic programs. Among others, we present a hitherto unknown relation between the problem of invariant synthesis and the Skolem problem, a difficult open problem in number theory. With the presented techniques, we advance the state-of-the-art in probabilistic loop analysis and enable exact analysis and inference for new classes of probabilistic programs and loops.