一句话：形式化随机变分推断中 REINFORCE 的隐含假设，并实现 Pyro 静态分析验证 model-guide 支撑匹配。
深度概率编程语言（如 Pyro、Edward、ProbTorch）依赖基于随机变分推断的推理引擎，常用 score estimator/REINFORCE 将后验推断转化为优化问题。然而该算法对模型施加了隐含假设，违反时可能导致优化目标未定义或收敛保证失效。本文用指称语义和程序分析工具形式化 REINFORCE 在程序指称上的行为，揭示这些假设，并给出可自动化的证明规则；部分规则借助连续数学事实，把积分可积性要求替换为更易证明的可微性或有界性条件。作者为 Pyro 开发静态分析以验证 model-guide support match 假设，并在 Pyro 网页八个代表性模型-指南对上评估：发现一个 bug、一个非常规推理引擎用法，并确认其余六个满足假设。
Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, which led to the development of so called deep probabilistic programming languages, such as Pyro, Edward and ProbTorch. At the core of this development lie inference engines based on stochastic variational inference algorithms. When asked to find information about the posterior distribution of a model written in such a language, these algorithms convert this posterior-inference query into an optimisation problem and solve it approximately by a form of gradient ascent or descent. In this paper, we analyse one of the most fundamental and versatile variational inference algorithms, called score estimator or REINFORCE, using tools from denotational semantics and program analysis. We formally express what this algorithm does on models denoted by programs, and expose implicit assumptions made by the algorithm on the models. The violation of these assumptions may lead to an undefined optimisation objective or the loss of convergence guarantee of the optimisation process. We then describe rules for proving these assumptions, which can be automated by static program analyses. Some of our rules use nontrivial facts from continuous mathematics, and let us replace requirements about integrals in the assumptions, such as integrability of functions defined in terms of programs' denotations, by conditions involving differentiation or boundedness, which are much easier to prove automatically (and manually). Following our general methodology, we have developed a static program analysis for the Pyro programming language that aims at discharging the assumption about what we call model-guide support match. Our analysis is applied to the eight representative model-guide pairs from the Pyro webpage, which include sophisticated neural network models such as AIR. It finds a bug in one of these cases, reveals a non-standard use of an inference engine in another, and shows that the assumptions are met in the remaining six cases.
@article{paperbot532,
title = {Towards verified stochastic variational inference for probabilistic programs},
author = {Wonyeol Lee and Hangyeol Yu and Xavier Rival and Hongseok Yang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371084}
}