paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Probabilistic Programming with Stochastic Probabilities

基于随机概率的概率编程
PLDI 7(PLDI)2023匹配度 3/10 · 论文属于概率编程语言与形式语义/推断实现,与用户核心方向(PL→AI 静态分析、AI→PL 用 LLM 改进静态分析/形式化验证、浮点程序分析、LLM 交叉)无直接关系;仅与“贝叶斯程序分析”中的概率编程/贝叶斯推断背景有较弱邻近性。引用 8 inbox
Alexander K. Lew, Matin Ghavamizadeh, Martin C. Rinard, Vikash K. Mansinghka
crossref: 2026-09-10

AI 速览

一句话:提出以随机估计密度比为核心的 PPL,首次同时支持边缘化、嵌套推断、随机控制流与可编程推断。

论文针对现有概率编程语言(PPL)必须精确计算推断所需密度比、从而限制表达力的问题,提出以随机估计密度比为核心的新 PPL 设计与实现路径。作者放宽精确密度约束,将支持边缘化与嵌套推断、无限制随机控制流、连续/离散采样及可编程推断的程序编译为随机算法,无偏估计密度及其倒数,并在修正 Monte Carlo 推断中保证依赖不精确密度比仍 sound。论文用新核心演算 λSP 和逻辑关系证明编译器正确,在 Gen 的开源扩展 GenSP 上评估六个推断问题:可自动为昂贵精确密度生成快速估计器,噪声基本不影响收敛,构造性可靠估计器与手写方案相当且仅小常数开销。

问题
当前概率编程语言通常要求精确计算推断所需的概率密度比,这限制了语言表达力,难以同时支持边缘化、嵌套推断、随机控制流、连续/离散采样与可编程推断。
方法
放宽精确密度比约束,将概率程序编译为随机算法,以无偏方式估计密度及其倒数,并嵌入修正的 Monte Carlo 推断算法;在 λSP 核心演算上用逻辑关系证明编译器正确性。
评估
在 Gen 的开源扩展 GenSP 中实现,并在六个挑战性推断问题上评估;结果显示可自动生成快速密度估计器、估计噪声基本不影响收敛,且构造性可靠估计器与手写估计器相当,仅有小常数开销。
原文摘要(Abstract)

We present a new approach to the design and implementation of probabilistic programming languages (PPLs), based on the idea of stochastically estimating the probability density ratios necessary for probabilistic inference. By relaxing the usual PPL design constraint that these densities be computed exactly, we are able to eliminate many common restrictions in current PPLs, to deliver a language that, for the first time, simultaneously supports first-class constructs for marginalization and nested inference, unrestricted stochastic control flow, continuous and discrete sampling, and programmable inference with custom proposals. At the heart of our approach is a new technique for compiling these expressive probabilistic programs into randomized algorithms for unbiasedly estimating their densities and density reciprocals. We employ these stochastic probability estimators within modified Monte Carlo inference algorithms that are guaranteed to be sound despite their reliance on inexact estimates of density ratios. We establish the correctness of our compiler using logical relations over the semantics of λSP, a new core calculus for modeling and inference with stochastic probabilities. We also implement our approach in an open-source extension to Gen, called GenSP, and evaluate it on six challenging inference problems adapted from the modeling and inference literature. We find that: (1) ‍can automate fast density estimators for programs with very expensive exact densities; (2) convergence of inference is mostly unaffected by the noise from these estimators; and (3) our sound-by-construction estimators are competitive with hand-coded density estimators, incurring only a small constant-factor overhead.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1943,
  title = {Probabilistic Programming with Stochastic Probabilities},
  author = {Alexander K. Lew and Matin Ghavamizadeh and Martin C. Rinard and Vikash K. Mansinghka},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {PLDI},
  year = {2023},
  doi = {10.1145/3591290}
}