ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs

Das ProbInG-Projekt hat bedeutende Fortschritte in der formalen Analyse und Synthese probabilistischer Programme erzielt, insbesondere im Umgang mit Schleifen und neuronalen Netzwerken. Ein zentrales Ergebnis ist die Entwicklung von Polar, einem Framework zur automatisierten Analyse probabilistischer Schleifen auf Basis algebraischer Rekurrenzrelationen. Polar berechnet exakte geschlossene Formen für höhere Momente von Zufallsvariablen, Schleifeninvarianten und Sensitivitäten gegenüber Parametern. Es kann Schleifen mit Verzweigungen, polynomiellen Ausdrücken und gängigen Wahrscheinlichkeitsverteilungen analysieren und verbindet dabei Vollständigkeit mit praktischer Effizienz. Darauf aufbauend wurde ein Verfahren zur Synthese probabilistischer Programme entwickelt, das aus vorgegebenen Momenten der Ausgabeverteilung automatisch Schleifenprogramme erzeugt. Unterstützt werden dabei kontinuierliche (z.b. Gaußsche) ebenso wie diskrete Zufallsverteilungen. Dieser Ansatz erlaubt die gezielte Konstruktion nicht-terminierender Programme mit gewünschten statistischen Eigenschaften. Zur Rekonstruktion von Verteilungen aus einer endlichen Anzahl von Momenten wurde die sogenannte K-Serien-Methode eingeführt. Sie approximiert gemeinsame und marginale Dichten von Variablen in probabilistischen Schleifen symbolisch und iterativ als Funktion der Schleifeniteration. Die Methode ist genau, effizient und auf eine breite Klasse nichtlinearer und multivariater Systeme anwendbar. Ein weiterer Beitrag betrifft die Unsicherheitsquantifizierung in neuronalen Netzwerken. Hier wurden enge, konvergente Schranken für die kumulative Verteilungsfunktion (CDF) der Netzwerkausgabe unter verrauschten Eingaben hergeleitet. Der Ansatz bietet garantierte Fehlergrenzen für beliebige Architekturen mit monotonen Aktivierungsfunktionen, einschließlich ReLU- und CNNs. Diese Arbeiten ermöglichen eine präzise, verifizierbare und automatisierte Analyse probabilistischer Systeme in verschiedensten Anwendungsbereichen.