In probabilistic programming, the inference problem asks to determine a program's posterior distribution conditioned on its "observe" instructions. Inference is challenging, especially when exact rather than approximate results are required. Inspired by recent work on probability generating functions (PGFs), we propose encoding distributions on $\mathbb{N}^k$ as weighted automata over a commutative alphabet with $k$ symbols. Based on this, we map the semantics of various imperative programming statements to automata-theoretic constructions. For a rich class of programs, this results in an effective translation from prior to posterior distribution, both encoded as automata. We prove that our approach is sound with respect to a standard operational program semantics.

翻译：在概率编程中，推理问题要求确定程序在其"观测"指令条件下的后验分布。推理具有挑战性，尤其是在需要精确结果而非近似结果时。受近期概率生成函数研究的启发，我们提出将$\mathbb{N}^k$上的分布编码为具有$k$个符号的交换字母表上的加权自动机。基于此，我们将各种命令式编程语句的语义映射到自动机理论构造。对于一类丰富的程序，这实现了从先验分布到后验分布的有效转换，两者均以自动机形式编码。我们证明该方法相对于标准操作程序语义具有可靠性。