AI 中文总结
该研究针对含连续分布的递归高阶概率程序，提出名为Slice的类型导向离散化变换，可将连续程序转化为离散形式以适配离散推理引擎，能处理现有系统无法应对的复杂连续程序且性能具竞争力。
AI 中文摘要
我们研究精确离散化，将其作为具有连续分布的递归高阶概率程序的语义保持变换。我们针对的是连续值与有限个常数进行比较的程序，这类程序的精确推理可简化为离散问题。我们的核心技术贡献是一种非局部的类型导向分析，该分析可推断出连续值能被划分为有限个观测相关区域的位置，随后重写这些区域上的采样与比较行为。我们将此变换命名为Slice。由于该构造是全局且类型导向的，其正确性需要超越局部语法的推理：我们将该变换形式化，并利用操作语义上的耦合式逻辑关系论证，证明其对布尔查询的可靠性。作为应用，经变换后的程序可由Dice、Roulette和Storm等离散引擎执行。我们的实证评估显示，Slice与离散后端结合后具有两个互补优势：它能对超出以往精确系统处理范围的复杂连续程序实现精确推理；在可直接对比的基准测试中，它与当前最先进的连续程序精确推理系统相比具有竞争力。
英文摘要
We study exact discretization as a semantics-preserving transformation for recursive, higher-order probabilistic programs with continuous distributions. We target programs where continuous values are compared against finitely many constants, so exact inference reduces to a discrete problem. Our central technical contribution is a non-local, type-directed analysis that infers where continuous values can be partitioned into finitely many observationally relevant regions, then rewrites sampling and comparison behavior over those regions. We call this transformation Slice. Because this construction is global and type-directed, correctness requires reasoning beyond the local syntax: we formalize the transformation and prove soundness for boolean queries using a coupling-style logical relations argument over operational semantics. As an application, transformed programs can be executed by discrete engines such as Dice, Roulette, and Storm. Our empirical evaluation shows two complementary strengths of Slice when paired with discrete backends: it enables exact inference for challenging continuous programs that lie beyond the reach of previous exact systems, and, on benchmarks where direct comparison is possible, it is competitive with state-of-the-art exact inference systems for continuous programs.
CommentsExtended version of OOPSLA'26 paper (with appendices)
DOI：10.1145/3839534
