Probabilistic programming languages aim at designing and implementing algorithms that compute over probability distributions rather than states. They feature dedicated primitives for sampling and conditioning. Moreover, the evaluation of probabilistic programs relies on general purpose inference engines. In the last few years, several languages such as Pyro, Edward or Stan have been developed. They have been used in order to describe physical phenomena or machine learning applications.
In this talk, I will introduce probabilistic programming languages, their main features and their semantics. Then, I will present one class of engine relying on so-called stochastic variational inference algorithms (SVI). I will also show that the correctness SVI can be easily violated. Finally, I will present a series of semantic assumptions about programs that ensure the correctness of SVI and discuss how these assumptions can be discharged by abstract interpretation based static analysis.
