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, leading to the development of deep probabilistic
programming languages such as Pyro. 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 gradient ascent. In
this paper, we analyse one of the most fundamental and versatile variational
inference algorithms, called score estimator, 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. 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, by conditions involving differentiation or boundedness, which
are much easier to prove automatically. Following our general methodology, we
have developed a static program analysis for Pyro that aims at discharging the
assumption about what we call model-guide support match. Applied to the eight
representative model-guide pairs from the Pyro webpage, our analysis finds a
bug in one of these cases, reveals a non-standard use of an inference engine in
another, and shows the assumptions are met in the remaining cases.

本文分析了得分估计器作为最基础和多功能的变分推理算法，并利用语义学和程序分析中的工具来阐述这个算法在程序中的作用，揭示出算法所做假设的内在局限性，提出了证明这些假设的规则，并用非平凡的连续数学事实来代替假设中的积分要求，最终发展了一种运用静态程序分析来满足假设条件的方法，并应用于 Pyro 中的八个代表性模型中，表明这种方法是可行的。

朝向验证的概率规划随机变分推断

Towards Verified Stochastic Variational Inference for Probabilistic  Programs

In the internet era there has been an explosion in the amount of digital text
information available, leading to difficulties of scale for traditional
inference algorithms for topic models. Recent advances in stochastic
variational inference algorithms for latent Dirichlet allocation (LDA) have
made it feasible to learn topic models on large-scale corpora, but these
methods do not currently take full advantage of the collapsed representation of
the model. We propose a stochastic algorithm for collapsed variational Bayesian
inference for LDA, which is simpler and more efficient than the state of the
art method. We show connections between collapsed variational Bayesian
inference and MAP estimation for LDA, and leverage these connections to prove
convergence properties of the proposed algorithm. In experiments on large-scale
text corpora, the algorithm was found to converge faster and often to a better
solution than the previous method. Human-subject experiments also demonstrated
that the method can learn coherent topics in seconds on small corpora,
facilitating the use of topic models in interactive document analysis software.

该研究提出了一种基于折叠变分贝叶斯推断技术的随机算法，能快速准确地从大规模数字文本信息中学习话题模型并与人交互分析。