一句话：提出迹类型系统与指称语义，使可编程推断程序在构造上保证可靠性，覆盖变分、SMC、MCMC 等。
现代概率编程语言提供可编程推断构造，让开发者能为特定模型或数据定制推断算法，但这些构造容易被误用，从而写出看似正确、结果却不可靠的程序。论文为高阶概率语言中的可编程推断建立指称语义，并设计类型系统，使良类型的推断程序天然可靠。核心思想是让概率表达式的类型不仅跟踪返回值类型，还跟踪其可能执行迹的空间，因为推断算法常操纵这些迹。作者用该语义与类型系统证明了使用变分推断、序贯蒙特卡洛、重要性采样和马尔可夫链蒙特卡洛构造的自定义推断程序的可靠性。
Modern probabilistic programming languages aim to formalize and automate key aspects of probabilistic modeling and inference. Many languages provide constructs for programmable inference that enable developers to improve inference speed and accuracy by tailoring an algorithm for use with a particular model or dataset. Unfortunately, it is easy to use these constructs to write unsound programs that appear to run correctly but produce incorrect results. To address this problem, we present a denotational semantics for programmable inference in higher-order probabilistic programming languages, along with a type system that ensures that well-typed inference programs are sound by construction. A central insight is that the type of a probabilistic expression can track the space of its possible execution traces, not just the type of value that it returns, as these traces are often the objects that inference algorithms manipulate. We use our semantics and type system to establish soundness properties of custom inference programs that use constructs for variational, sequential Monte Carlo, importance sampling, and Markov chain Monte Carlo inference.
@article{paperbot567,
title = {Trace types and denotational semantics for sound programmable inference in probabilistic languages},
author = {Alexander K. Lew and Marco F. Cusumano-Towner and Benjamin Sherman and Michael Carbin and Vikash K. Mansinghka},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371087}
}