一句话：提出将前期望语义翻译为一阶约束的项表示，实现递归概率程序期望值的全自动推断。
本文研究含过程、局部变量与递归等自然语言构造的概率程序中，期望结果值的全自动推断。这类构造对分析至关重要，却使自动化变得十分困难。作者提出一种项表示 infer[.]，将前期望（pre-expectation）语义翻译为一阶约束，从而可借助标准求解方法实现自动分析。受递归程序 Hoare 逻辑工作启发，该方法引入逻辑变量处理递归，并且不局限于可由迭代替代的尾递归。作者在原型工具 ev-imp 中实现了该分析，并通过大量实验展示了其算法表达能力。
In this work, we study the fully automated inference of expected result values of probabilistic programs in the presence of natural programming constructs such as procedures, local variables and recursion. While crucial, capturing these constructs becomes highly non-trivial. The key contribution is the definition of a term representation, denoted as infer[.], translating a pre-expectation semantics into first-order constraints, susceptible to automation via standard methods. A crucial step is the use of logical variables, inspired by previous work on Hoare logics for recursive programs. Noteworthy, our methodology is not restricted to tail-recursion, which could unarguably be replaced by iteration and wouldn't need additional insights. We have implemented this analysis in our prototype ev-imp. We provide ample experimental evidence of the prototype's algorithmic expressibility.
@article{paperbot1987,
title = {Automated Expected Value Analysis of Recursive Programs},
author = {Martin Avanzini and Georg Moser and Michael Schaper},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591263}
}