Automated Analysis of Probabilistic Loops

From classical randomized algorithms to modern generative machine learning components, probabilistic programs are becoming ubiquitous in many different applications, including security/privacy protocols (e.g., differential privacy), synthetic data generation for scenario-based testing (e.g., Scenic), and large language models (e.g., ChatGPT).
Probabilistic programming languages provide a unifying framework where random sampling from different probability distributions, taking random choices, and performing inference tasks become easy coding activities. On the other side, the automated analysis of these probabilistic programs, especially of probabilistic loops with potentially infinite state space, is generally infeasible. In this talk, we present the recent results of ProbInG, an ICT project funded by the Vienna Science and Technology Fund “that aims at developing novel and fully automated approaches to generate invariants over higher-order moments and the value distribution of program variables, without any user guidance”.