一句话:提出语言无关的概率程序静态分析框架 LASAPP,支持五种概率语言并实现四类可证正确的分析。
概率编程让开发者专注于贝叶斯建模,但概率环境特有的编程错误往往需要深入了解底层系统才能修复。现有静态分析多针对特定语言,难以复用。本文提出 LASAPP——首个以语言无关方式表述概率程序静态分析的框架:所有分析只需添加易实现的 API 绑定即可应用于新语言,原型开箱支持五种主流概率编程语言。作者给出四种可证明正确的语言无关概率程序分析,分别针对文献中讨论的问题,并在 200 多个真实程序上评估,展示了框架的有效性与表达力。
Probabilistic programming allows developers to focus on the modeling aspect in the Bayesian workflow by abstracting away the posterior inference machinery. In practice, however, programming errors specific to the probabilistic environment are hard to fix without deep knowledge of the underlying systems. Like in classical software engineering, static program analysis methods could be employed to catch many of these errors. In this work, we present the first framework to formulate static analyses for probabilistic programs in a language-agnostic manner: LASAPP. While prior work focused on specific languages, all analyses written with our framework can be readily applied to new languages by adding easy-to-implement API bindings. Our prototype supports five popular probabilistic programming languages out-of-the-box. We demonstrate the effectiveness and expressiveness of the LASAPP framework by presenting four provably-correct language-agnostic probabilistic program analyses that address problems discussed in the literature and evaluate them on over 200 real-world programs.