保证引导程序组合正确性的可编程 MCMC

以下摘要由 AI 根据胶片自动生成。

本报告（OOPSLA’24）将 Multiple-Block Metropolis-Hastings（BMH）算法形式化为引导程序的顺序组合，解决了可编程贝叶斯推断中模型与引导程序一致性难以保证的问题。基于协程与消息传递通道，利用 Session Types 设计了引导类型系统，并证明结构类型等价判定的多项式时间复杂度。此外给出了覆盖性检查算法，静态保证每个随机变量在推断过程中至少被新鲜采样一次。