高阶概率编程语言中的自动对齐
摘要：概率编程语言（PPLs）允许用户编码统计推断问题，并自动应用推断算法解决这些问题。流行的PPLs推断算法，如顺序蒙特卡洛（SMC）和马尔科夫链蒙特卡洛（MCMC），是围绕检查点（在执行概率程序期间对推断算法具有相关性的事件）构建的。在当前的PPLs中，决定检查点的位置并不是最佳的。为了解决这个问题，我们提出了一种静态分析技术，自动确定程序中的检查点，减轻了PPL用户的任务。该分析识别出在每个程序运行中以相同顺序执行的一组检查点- 它们是对齐的。我们形式化对齐，证明了分析的正确性，并将该分析实现为高阶函数式PPL Miking CorePPL的一部分。通过利用对齐分析，我们设计了两种新的推断算法变体：对齐的SMC和对齐的轻量级MCMC。通过真实世界实验，我们展示了它们与标准PPL版本的SMC和MCMC相比，在推断执行时间和准确性方面显著提高。
作者：Daniel Lund''en, Gizem c{C}aylak, Fredrik Ronquist, David Broman
论文ID：2301.11664
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-05-05