一句话：将概率程序编译为密度函数并增量计算，加速多种蒙特卡洛推断且分离式证明保证正确性。
概率程序推断通常需要评估大量可能执行，以找到高后验密度的执行；在大数据集上，昂贵的中间结果应被跨次评估共享，而非从头重算。本文提出基于增量计算的新方法：首先将具表达力的概率程序编译为计算其密度函数的确定性程序；然后基于增量 λ-演算，发展出对具表达力函数式程序进行组合式增量化的通用技术，并将其应用于这些密度函数。所得增量密度可加速广泛的蒙特卡洛推断算法，包括现有系统支持不佳的非参数模型。将增量密度计算分解为密度计算与增量计算两步，还支持模块化的正确性推理，缓解现有系统中临时增量特性导致的可靠性 bug；作者用指称逻辑关系分别证明两步的正确性。Julia 原型在多种模型与推断算法上展现出运行时随数据集规模增长的渐近改进。
Inference in probabilistic programs generally requires evaluating many possible program executions to find those of high posterior density. To scale inference to large datasets, it is crucial that expensive intermediate results are shared across these many evaluations, rather than recomputed from scratch. This paper presents a new approach to realizing this sharing, based on incremental computation , a technique for efficiently recomputing (deterministic) program outputs when program inputs change. First, we show how expressive probabilistic programs can be compiled to deterministic ones that compute their density functions. Then, building on the incremental λ-calculus, we develop a general technique for compositionally incrementalizing expressive functional programs, and apply it to these densities. The resulting incremental densities can be used to accelerate a broad range of Monte Carlo inference algorithms, including for nonparametric models not well supported by existing systems. Furthermore, our decomposition of incremental density computation into separate density and incrementalization steps allows for modular reasoning about correctness—a key pain point in existing systems, where ad-hoc incrementalization features are a known source of soundness bugs. We develop denotational logical relations arguments for the correctness of each step independently, and implement the approach in a Julia prototype, finding that it leads to asymptotic runtime improvements in the size of the dataset on a range of models and inference algorithms.
@article{paperbot3758,
title = {Incremental Computation for Efficient Programmable Inference in Probabilistic Programs},
author = {Fabian Zaiser and Jack Czenszak and Martin C. Rinard and Vikash K. Mansinghka and Alexander K. Lew},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808316}
}