ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs

The ProbInG project has made significant advances in the formal analysis and synthesis of probabilistic programs, with a particular focus on loops and neural networks. A key outcome is the development of POLAR, a novel framework for fully automating the analysis of probabilistic loops through algebraic reasoning. POLAR precisely captures loop semantics using recurrence relations, enabling the computation of exact closed-form expressions for higher-order moments, loop invariants, and sensitivity to parameters. Building on this foundation, we developed a method for probabilistic program synthesis that automatically constructs looping programs based on target statistical properties, such as prescribed moments of the output distribution. This approach supports a rich class of probabilistic constructs, including Gaussian and discrete distributions, and enables controlled generation of non-terminating probabilistic processes. To recover underlying distributions from limited moment information, we introduced the K-series estimation method, which approximates the joint and marginal distributions of variables in probabilistic loops. The K-series provides symbolic, iteration-aware density estimates that are fast, accurate, and applicable to a wide range of systems, including those with non-linear and multivariate behaviors. Finally, we addressed the challenge of quantifying uncertainty in neural networks by obtaining tight converging bounds on the cumulative distribution function (CDF) of the output distribution when inputs are noisy. Our approach generalizes to various architectures, including ReLU and convolutional networks, and guarantees exact error bounds—offering a principled alternative to heuristic uncertainty estimation methods. Together, these contributions advance the automated and formal understanding of probabilistic systems, enabling verifiable, interpretable, and synthesizable models across diverse domains.