一句话：提出以生成函数为编译目标的概率程序精确推断方法，形式化编译并证明其正确性，实现系统 Geni。
本文针对概率程序精确推断的可扩展性问题，提出一种新的编译思路：以生成函数（GF）作为编译目标。现有方法通常编译到二叉决策图（BDD）等表示并取得领先效果，作者表明面向 GF 的编译器在 BDD 方法表现良好的推断问题上同样具有竞争力，甚至在某些情况下可扩展性更强。文章给出了该编译器的形式化模型，首次为函数式概率语言定义了 GF 编译，并相对于指称语义证明了编译器的正确性。作者在名为 Geni 的概率编程系统中实现了该方法，并在多种推断问题上进行评估。结果确立了 GF 编译作为精确推断的一种有原则且强大的范式，兼具良好可扩展性、表达力与坚实的理论基础。
We present a new approach to scaling exact inference for probabilistic programs, using generating functions (GFs) as a compilation target. Existing methods that target representations like binary decision diagrams (BDDs) achieve strong state-of-the-art results. We show that a compiler targeting GFs can be similarly competitive—and, in some cases, more scalable—on a range of inference problems where BDD-based methods perform well. We present a formal model of this compiler, providing the first definition of GF compilation for a functional probabilistic language. We prove that this compiler is correct with respect to a denotational semantics. Our approach is implemented in a probabilistic programming system called Geni and evaluated on a range of inference problems. Our results establish GF compilation as a principled and powerful paradigm for exact inference: it offers strong scalability, good expressiveness, and a solid theoretical foundation.