Program Analysis of Probabilistic Programs
University of Edinburgh（爱丁堡大学）
概率编程是一个不断发展的领域，它通过将概率建模与概率推理分离，努力使统计分析更容易获得。在实践中，这种脱钩是困难的。没有一种推理算法可以用作同时可靠、高效、黑盒和通用的概率编程后端。可能的程序设计语言通常选择一个算法来应用于给定的问题，从而继承其局限性。虽然已经做了大量的工作，以形式化的概率编程和提高推理效率，很少有工作，利用现有的程序结构，通过正式分析，以更好地利用底层推理算法。本文提出了三种新的技术（静态和动态），旨在提高概率规划使用程序分析。这些技术分析一个概率程序，并对其进行调整，以使推理更有效，有时是以一种单调乏味或不可能手工完成的方式进行的。
2022-04-14 cs.LG cs.PL stat.ML
ptype: Probabilistic Type Inference
School of Informatics（信息学院）；University of Edinburgh（爱丁堡大学）；Alan Turing Institute（艾伦·图灵研究所）
类型推断是指推断给定数据列的数据类型的任务。当数据包含缺失数据和异常时，当前的方法通常会失败，这在现实世界的数据集中很常见。在本文中，我们提出了ptype，概率鲁棒类型推断方法，使我们能够检测到这样的条目，并推断数据类型。我们进一步表明，所提出的方法优于现有的方法。
2020-03-23 cs.LG cs.PL stat.ML
Automatic Alignment of Sequential Monte Carlo Inference in Higher-Order Probabilistic Programs
概率编程是一种用于表达灵活的概率模型的编程范式。概率程序设计语言的实现采用各种推理算法，其中通常使用顺序蒙特卡罗方法。使用顺序蒙特卡罗推断的当前最先进的实现的问题是程序同步点的对齐。提出了一种基于0-CFA算法的高阶概率程序自动对齐的静态分析方法。我们评估了系统发育模型上的自动比对，显示出运行时间的显着减少和准确性的增加。
2018-12-18 cs.PL
Stochastic Probabilistic Programs
Ben-Gurion University of the Negev（内盖夫本-古里安大学）
我们介绍了一个随机概率程序的概念，并提出了一个参考实现的概率编程设施，支持规范的随机概率程序和推理。随机概率程序允许直接规范和有效的推理模型与滋扰参数，噪声和不确定性。我们给出了几个随机概率程序的例子，并在模型说明和推理方面将这些程序与相应的确定性概率程序进行了比较。最后，我们讨论了开放的研究课题和相关工作。
2020-01-22 cs.LG cs.PL stat.ML
Verifying Handcoded Probabilistic Inference Procedures
研究人员最近提出了几个简化贝叶斯概率推理过程的系统。这些包括自动推理算法合成系统以及更强的手动算法开发抽象。然而，现有的系统，其性能依赖于开发人员手动构建的推理算法的一部分，有限的支持推理的正确性的结果算法。在本文中，我们提出了Shuffle，一个程序设计语言手动开发的推理过程，1）强制执行概率论的基本规则，2）强制执行算法的相应概率模型的统计依赖关系，3）生成一个优化的实现。我们已经使用Shuffle为几个标准的概率模型开发了推理算法。我们的研究结果表明，洗牌使开发人员能够提供正确的和高性能的实现这些算法。
2018-05-04 cs.PL
Rethinking Variational Inference for Probabilistic Programs with Stochastic Support
University of Oxford（牛津大学）；Nanyang Technological University（南洋理工大学）
本文提出支撑分解变分推断（SDVI），通过将具有随机支撑的概率程序分解为静态支撑子程序并分别构建子引导，以改进变分族构建并提升推断性能。
2023-11-01 cs.AI cs.LG cs.PL
Compositional Inference Metaprogramming with Convergence Guarantees
推理元编程通过支持将概率程序的执行分解为子问题和将不同的概率推理算法应用于不同子问题的混合概率推理算法的部署来实现有效的概率编程。我们引入了独立子问题推理的概念（相对于纠缠子问题推理，其中的子问题推理算法在整个程序跟踪操作），并提出了一个数学框架，用于研究收敛性能的混合推理算法，适用于不同的马尔可夫链蒙特卡罗算法的推理问题的不同部分。然后，我们使用这种形式主义证明渐近收敛结果的概率程序推理元编程。据我们所知，这是第一个渐近收敛的混合概率推理算法定义（基于子问题）推理元编程的结果。
2019-07-15 cs.PL
Semi-Symbolic Inference for Efficient Streaming Probabilistic Programming
在流媒体环境中，使用Rao-Blackwellized粒子滤波器（RBPF）通常可以进行有效的推理，RBPF在可能的情况下可以精确地解决推理问题，并在必要时返回采样近似。虽然RBPF可以手动实现以提供有效的推理，但流式概率编程的目标是在给定输入概率程序的情况下自动生成这种有效的推理实现。在这项工作中，我们提出了半符号推理，一种使用运行时推理系统，自动实现Rao-Blackwellized粒子滤波执行概率程序的技术。为了一起执行精确和近似推理，半符号推理系统操纵符号分布以在可能时执行精确推理，并且在必要时回到近似采样。这种方法使系统能够实现开发人员手工编写的相同RBPF。为了确保这一点，我们确定封闭的家庭分布-如线性高斯和有限离散模型-推理系统保证准确的推理。我们已经实现了运行时推理系统的ProbZelus流概率程序设计语言。尽管平均$1.6\times$放缓相比，现有的基准测试的最先进的状态，我们的评估表明，$3\times$ - $87\times$的加速是可获得的一组新的具有挑战性的基准测试，我们已经设计利用封闭的家庭。
2022-11-05 cs.PL
Learning Proposals for Probabilistic Programs with Inference Combinators
Northeastern University（东北大学）
我们开发的运营商建设的建议，在概率程序，我们称为推理组合。推理组合子定义了一个语法上的重要性采样组成的基本操作，如应用程序的过渡内核和重要性restaurant。这些采样器中的建议可以使用神经网络进行参数化，而神经网络又可以通过优化变分目标进行训练。其结果是用户可编程的变分方法，是正确的建设，并可以定制特定的模型的框架。我们证明了这个框架的灵活性，通过实施先进的变分方法的基础上摊销吉布斯抽样和退火。
2021-06-17 cs.LG cs.PL stat.ML
Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support
University of Oxford（牛津大学）；KAIST（韩国科学技术院）
通用概率编程系统（PPS）提供了一个强大的框架，指定丰富的概率模型。他们进一步尝试自动化从这些模型中得出推论的过程，但成功地做到这一点受到他们可以表达的广泛的非标准模型的严重阻碍。因此，尽管可以在通用PPS中指定复杂的模型，但所提供的推理引擎通常远远达不到所需的程度。特别是，我们表明，他们产生令人惊讶的不满意的性能模型的支持不同的执行，往往没有比重要性抽样从以前更好。为了解决这个问题，我们引入了一个新的推理框架：划分，征服和合并，这仍然是有效的，这样的模型，并显示它如何可以实现为一个自动化和通用的PPS推理引擎。我们经验证明，现有的方法在三个例子的性能大幅改善。
2020-07-16 cs.LG cs.PL stat.ML
Verifying Performance Properties of Probabilistic Inference
本文探讨通过形式化验证为概率编程的混合精确/近似推断系统提供性能保证，介绍SSI、面向复杂程序的程序分析扩展及延迟采样的有界内存验证工作。
2023-07-14 cs.PL
Sound Probabilistic Inference via Guide Types
概率程序设计语言旨在描述和自动化贝叶斯建模和推理。现代语言支持可编程推理，这允许用户通过结合指导程序来定制推理算法，以提高推理性能。为了使贝叶斯推理合理，引导程序必须与模型程序兼容。模型-指南兼容性的一个普遍但具有挑战性的条件是绝对连续性，这要求模型和指南程序定义具有相同支持的概率分布。本文提出了一种新的概率程序设计语言，保证绝对连续性，并具有一般的编程结构，如分支和递归。模型和向导程序被实现为协同程序，它们相互通信以同步它们在执行期间采样的随机变量集。新的指南类型描述和执行协程之间的通信协议。如果模型和指南使用相同的协议进行了良好的类型化，那么就可以保证它们具有绝对的连续性。一个有效的算法从代码中推断出指南类型，这样用户就不必指定类型。新的程序设计语言的评估与实现，其中包括类型推理算法和原型编译器的目标Pyro。实验表明，我们的语言是能够表达各种概率模型与非平凡的控制流和递归，并且基于协程的计算不会引入显着的开销在实际的贝叶斯推理。
2021-04-08 cs.PL
Exact Probabilistic Inference Using Generating Functions
概率程序通常是描述后验概率分布的正态程序。它们本质上编码了随机算法，长期以来一直是现代机器学习和近似计算的核心。我们探索了生成函数的理论[19]，并研究了它在概率程序的精确定量推理中的用途。重要的主题包括程序语义的精确表示[13]，证明精确的程序等价性[5]，以及--作为我们在这个扩展摘要中的主要焦点--精确的概率推理。在概率编程中，推理的目的是导出程序的后验分布。与近似推断相反，推断精确分布有几个好处[8]，例如，不损失精度，对符号参数的自然支持，以及对具有某些结构的模型的效率。然而，精确的概率推理是一项众所周知的艰巨任务[6，12，17，18]。挑战主要来自三个程序结构：（1）无界while循环和/或递归，（2）无限支持分布，（3）条件反射（通过后验观测）。我们提出了我们正在进行的研究，在解决这些挑战（重点是空调）利用生成函数，并显示其潜力，促进精确的概率推理离散概率程序。
2023-02-12 cs.DM cs.LO cs.PL
Probabilistic Inference for Datalog with Correlated Inputs
本文提出 Datalog 扩展 Praline，将相关输入下的概率推断形式化为约束优化问题，并设计 δ-精确推断算法，在侧信道分析等基准上实现可扩展且紧致的概率界限。
2025-08-21 cs.PL
Bit Blasting Probabilistic Programs
针对现有概率编程语言对混合概率程序支持不足的问题，提出基于bit blasting的离散化近似推理算法，构建HyBit系统，在精度无损的前提下实现高效推理，性能优于现有采样与符号推理方法。
2024-04-30 cs.PL
Swift: Compiled Inference for Probabilistic Programming Languages
UC Berkeley（加州大学伯克利分校）；University of Washington（华盛顿大学）
概率程序定义了其语义结构上的概率度量。概率程序设计语言（PPL）的一个共同目标是使用通用推理引擎，在给定观察到的证据的情况下，计算任意模型和查询的后验概率。大多数PPL推理引擎-即使是编译的-会产生显著的运行时解释开销，特别是对于偶然和开放宇宙模型。本文介绍了一个用于BLOG PPL的编译器Swift。Swift生成的代码结合了优化，消除了解释开销，有效地维护了动态依赖关系，并处理了不同大小的可能世界的存储管理。Swift与其他PPL引擎在各种推理问题上的比较实验表明，加速比从12倍到326倍不等。
2016-06-30 cs.AI cs.PL
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
本文提出基于概率生成函数语义的精确贝叶斯推断方法，并实现 Prodigy 工具，以支持含无界循环的条件化概率程序的推断与定量验证。
2024-03-05 cs.LO cs.PL
Reactive Graphs for Efficient Markov Chain Monte Carlo Inference in Probabilistic Programming Languages
KTH Royal Institute of Technology（瑞典皇家理工学院）；Swedish Museum of Natural History（瑞典自然历史博物馆）
提出一种自动将概率程序转换为动态反应图的方法，显式表示数据依赖，使得MCMC提议仅重新计算依赖已重绘随机变量的部分，从而提升推断效率。
2026-06-29 cs.PL
Modular Probabilistic Models via Algebraic Effects
针对概率编程语言中模型可重用性和可组合性受限的问题，本文以Haskell为宿主语言，提出一种基于代数效应的嵌入式领域特定语言，使概率模型成为模块化、一等公民且可重用于模拟与推断，并利用代数效应处理器将模拟和推断表达为可组合的程序转换。
2024-12-23 cs.PL
Edward: A library for probabilistic modeling, inference, and criticism
Columbia University（哥伦比亚大学）
概率建模是分析经验信息的一种强有力的方法。我们描述爱德华，概率建模库。Edward的设计反映了George Box开创的迭代过程：建立一个现象的模型，对给定数据的模型进行推断，并批评模型与数据的拟合。爱德华支持广泛的概率模型，有效的推理算法，以及许多模型批评技术。该库构建在TensorFlow之上，以支持分布式训练和GPU等硬件。Edward能够大规模开发复杂的概率模型及其算法。
2017-02-01 cs.AI cs.PL stat.AP
Reactive Probabilistic Programming
同步建模是程序设计语言（如Lustre、Esterel或Scade）的核心，通常用于实现安全关键控制软件，例如，飞机的电传操纵和发动机控制。然而，到目前为止，这些语言对建模不确定性（软件环境或行为的概率方面）的现代支持有限，尽管建模不确定性是设计控制系统时的主要活动。在本文中，我们提出了第一个同步概率程序设计语言ProbZelus。ProbZelus保守地提供了编写控制软件的同步语言的设施，具有概率结构来建模不确定性并执行循环中的推理。我们提出的语言的设计和实现。我们提出了概率流函数的测度论语义和一个简单的类型纪律来分离确定性和概率表达式。我们展示了一个语义保持编译成一个一阶函数语言，适合于一个简单的演示推理算法的流模型。我们还重新设计了延迟采样推理算法，以提供高效的流式推理。结合对几个反应式应用程序的评估，我们的结果表明，ProbZelus可以设计反应式概率应用程序和高效的有界内存推理。
2020-04-09 cs.PL
SPPL: Probabilistic Programming with Fast Exact Symbolic Inference
Massachusetts Institute of Technology（麻省理工学院）
我们提出的总和产品概率语言（SPPL），一种新的概率程序设计语言，自动提供精确的解决方案，广泛的概率推理查询。SPPL将概率程序转换为和积表达式，这是一种新的符号表示和相关的语义域，扩展了标准和积网络以支持混合型分布，数值变换，逻辑公式以及逐点和集值约束。我们正式SPPL通过一种新的翻译策略，从概率程序和产品的表达式，并给出健全的精确算法的条件和计算事件的概率。SPPL对概率程序施加了一系列限制，以确保它们可以被翻译成和积表达式，这允许系统利用新技术，通过自动利用概率结构来提高翻译和推理的可扩展性。我们实现了一个原型的SPPL与模块化架构和评估基准系统的目标，显示它获得了高达3500倍的加速比最先进的符号系统的任务，如验证的公平性的决策树分类，平滑隐马尔可夫模型，条件变换的随机变量，并计算罕见的事件概率。
2021-06-11 cs.LG cs.PL cs.SC
Probabilistic Programming Meets Automata Theory: Exact Inference using Weighted Automata
本文提出利用加权自动机实现有限概率程序的精确推断，通过将变量分布编码为自动机来计算后验分布。
2025-12-15 cs.FL cs.PL
Augur: a Modeling Language for Data-Parallel Probabilistic Inference
Oracle Labs（甲骨文实验室）；Harvard University（哈佛大学）；Carnegie Mellon University（卡内基梅隆大学）
为每个新的概率模型实现推理过程是耗时且容易出错的。概率编程通过允许用户指定模型并让编译器自动为其生成推理过程来解决这个问题。为了使这种方法实用，重要的是生成具有合理性能的推理代码。在本文中，我们提出了一个概率编程语言和编译器的贝叶斯网络，旨在有效地利用数据并行架构，如GPU。我们的语言完全集成在Scala编程语言中，并受益于IDE支持，类型检查和代码完成等工具。我们表明，编译器可以生成可扩展到数千个GPU核心的数据并行推理代码，利用贝叶斯网络中的条件独立关系。
2014-06-10 cs.AI cs.DC cs.PL
Venture: a higher-order probabilistic programming platform with programmable inference
MIT（麻省理工学院）
我们描述风险，概率编程的交互式虚拟机，其目的是充分表达，可扩展，高效的通用用途。像Church一样，Venture中的概率模型和推理问题也是通过一种图灵完备的高阶概率语言来描述的。与Church不同，Venture还提供了一种组合语言，用于基于可扩展的精确和近似技术构建的自定义推理策略。我们还描述了四个关键方面的风险投资的实施，建立在概率图形模型的想法。首先，我们描述了随机过程接口（SPI），指定和封装原始随机变量。SPI支持自定义控制流、高阶概率程序、部分可交换序列和“无可能性”随机模拟器。它还支持外部模型，这些模型对隐藏在Venture中的潜在变量进行推断。其次，我们描述了概率执行轨迹（PETS），这代表了执行历史的风险投资计划。PET捕获条件依赖、存在依赖和可交换耦合。第三，我们描述了分区的执行历史称为脚手架的因素，全球推理问题成连贯的子问题。最后，我们描述了一个家庭的随机再生算法，有效地修改PET片段内的支架。随机再生线性运行时缩放的情况下，许多以前的方法缩放二次。我们将展示如何使用随机再生和SPI来实现通用的推理策略，如大都会黑斯廷斯，吉布斯采样，并阻止粒子马尔可夫链蒙特卡罗和平均场变分推理技术的基础上的建议。
2014-04-01 cs.AI cs.PL stat.CO
A New Approach to Probabilistic Programming Inference
University of Oxford（牛津大学）；Columbia University（哥伦比亚大学）；Massachusetts Institute of Technology（麻省理工学院）
我们介绍并证明了一种新的方法，推理表达概率编程语言的基础上粒子马尔可夫链蒙特卡罗。我们的方法是简单的实现和易于并行化。它适用于图灵完备概率编程语言，并支持使用复杂控制流（包括随机递归）的模型中的精确推理。它还包括贝叶斯非参数统计的基元。我们的实验表明，这种方法可以更有效地比以前介绍的单站点Metropolis-Hastings方法。
2015-07-09 cs.AI cs.PL stat.ML
Knowledge Compilation with Continuous Random Variables and its Application in Hybrid Probabilistic Logic Programming
KU Leuven（鲁汶大学）
在概率推理中，传统的离散域已被提升到包含额外连续随机变量的混合域。然而，在混合域中的推理通常需要对离散或连续随机变量的推理进行权衡。我们介绍了一种新的方法，加权模型集成和代数模型计数的基础上，规避这些权衡。然后，我们展示了它如何支持知识编译和精确的概率推理。此外，我们引入了混合概率逻辑程序设计语言HAL-ProbLog，ProbLog的扩展，我们适用于我们的推理方法。
2018-07-12 cs.AI cs.LO cs.PL
Weighted Automata for Exact Inference in Discrete Probabilistic Programs
本文提出利用加权自动机进行离散概率程序中精确推断，通过将分布编码为自动机并映射编程语句到自动机构造，实现先验到后验分布的转换。
2025-11-25 cs.FL cs.PL
Modular probabilistic programming with algebraic effects (MSc Thesis 2019)
University of Edinburgh（爱丁堡大学）
本文提出Koka Bayes库，结合代数效应处理与模块化设计，解决概率编程中推理算法的模块化实现问题。
2024-12-18 cs.PL stat.CO
Slice Sampling for Probabilistic Programming
University of Cambridge（剑桥大学）
我们介绍了第一个，通用的，切片采样推理机的概率程序。该引擎作为StocPy的一部分发布，StocPy是一种新的图灵完备概率程序设计语言，可作为Python库使用。我们提出了一个transdimensional概括切片采样，这是必要的推理机工作的痕迹与不同数量的随机变量。我们表明，StocPy相比其他PPL的灵活性和可用性方面，切片采样可以优于以前介绍的推理方法。我们的实验包括逻辑回归，HMM和贝叶斯神经网络。
2015-01-20 cs.AI cs.PL
Deep Probabilistic Programming
Columbia University（哥伦比亚大学）；Adobe Research（Adobe研究院）；Google Research（谷歌研究院）；Google Brain（谷歌大脑）
我们建议爱德华，图灵完备的概率编程语言。Edward定义了两种组合表示-随机变量和推理。通过将推理视为一等公民，与建模相提并论，我们证明了概率编程可以像传统的深度学习一样灵活和计算效率高。为了灵活性，Edward使用各种可组合的推理方法，从点估计到变分推断，再到MCMC，很容易拟合同一模型。此外，Edward可以重用建模表示作为推理的一部分，促进丰富的变分模型和生成对抗网络的设计。为了提高效率，Edward被集成到TensorFlow中，比现有的概率系统提供了显著的加速。例如，我们在一个基准测试逻辑斯谛回归任务上显示，Edward至少比Stan快35倍，比PyMC 3快6倍。此外，Edward没有运行时开销：它和手写的TensorFlow一样快。
2017-03-07 cs.AI cs.LG cs.PL
Advanced Probabilistic Couplings for Differential Privacy
差分隐私是一种很有前途的数据隐私的形式化方法，它提供了一个量化的界限上的隐私成本的算法，操作敏感信息。已经开发了几种工具用于差分私有算法的形式化验证，包括程序逻辑和类型系统。然而，这些工具并没有捕捉到近年来出现的基本技术，也不能用于推理尖端的差异隐私算法。现有技术无法处理三大类算法：1）隐私依赖于准确性保证的算法，2）用高级合成定理分析的算法，其显示隐私成本增长较慢，3）交互式接受自适应输入的算法。我们解决这些限制与一个新的形式主义扩展apRHL，关系程序逻辑，已被用于证明差分隐私的非交互式算法，并将aHL，（非关系）程序逻辑的准确性。我们说明我们的方法，通过一个单一的运行的例子，这说明了三类算法，并探讨了新的变种稀疏向量技术，一个很好的研究算法的隐私文献。我们在EasyCrypt中实现我们的逻辑，并正式验证隐私。我们还介绍了一种新的耦合技术称为\emph{optimal subset coupling}，可能是独立的利益。
2016-08-17 cs.DS cs.LO cs.PL
Monolingual Probabilistic Programming Using Generalized Coroutines
FNMOC（美国海军舰队气象与海洋学中心）；Rutgers University（罗格斯大学）
概率程序设计语言和建模工具包是构建和重用随机模型和推理过程的两种模块化方法。结合两者的优势，我们在同一通用语言中将模型和推理表示为广义协程。我们使用语言的现有设施，如丰富的库，优化编译器和类型，开发简洁，声明性和现实的模型，具有竞争力的性能，精确和近似推理。特别地，可以使用备忘录化来表达广泛的模型。因为模型的确定性部分是全速运行的，所以自定义推理过程是微不足道的，并且推理过程可以在没有解释开销的情况下进行推理。在这个框架内，我们介绍了一个新的，一般的重要性采样算法与前瞻。
2012-05-09 cs.AI cs.PL
