Report title: Static Analysis of Posterior Inference in Bayesian Probability

Report time: June 2nd, 10:00-11:00

Offline report location: B1002, Science Building

Host: Professor Zhang Min

Abstract:

In Bayesian probabilistic programming, a central problem is to estimate the normalised posterior distribution (NPD) of a probabilistic program with score statements. Prominent approximate approaches to address this problem cannot generate guaranteed outcomes within a finite time limit, and previous formal approaches w.r.t. exact inference for NPD are restricted to programs with bounded loops/recursion. A recent work (Beutner et al., PLDI 2022) proposed an automated approach that derives guaranteed bounds for NPD over programs with unbounded recursion. However, as this approach requires recursion unrolling, it suffers from the path explosion problem. Moreover, existing approaches do not consider score-recursive probabilistic programs that allow score statements inside loops, which is non-trivial and requires careful treatment to ensure the integrability of the normalising constant.

In this work, we propose a novel automated approach to derive bounds for NPD via polynomial templates, fixed-point theorems and Optional Stopping Theorem (OST). Our approach can handle probabilistic programs with unbounded while-loops and continuous distributions with infinite supports. Our novelties are three-fold: First, the use of polynomial templates circumvents the path explosion problem from recursion unrolling; Second, we derive a novel variant of OST that addresses the integrability issues in score-recursive programs; Third, to increase the accuracy of the derived bounds, our approach adopts a novel technique of truncation onto a bounded range of program values. Experiments over a wide range of benchmarks demonstrate that our approach is time-efficient and can derive bounds on NPD that can be tighter than (or comparable with) the recursion-unrolling approach (Beutner et al., PLDI 2022).

Introduction of Lectuer:

Peixin Wang is a postdoctoral research associate at the Department of Computer Science, University of Oxford, advised by Prof. Luke Ong. Previously, he received his Ph.D. degree under the supervision of Prof. Yuxi Fu and Dr. Hongfei Fu at Shanghai Jiao Tong University. Prior to that, he obtained the bachelor’s degree at East China Normal University. Peixin's research interests lie in the intersection of programming languages and machine learning. He is dedicated to exploring the application of formal methods to enhance the reliability and trustworthiness of probabilistic systems. Currently, his work focuses on probabilistic programming, Bayesian inference, and developing robust AI solutions.