Dec, 2015

通用概率编程的 Lambda 演算基础

PDF
TL;DR本文通过在 terms 上创建一个 measure space，定义级别逐步逼近的连续 lambda-Calculus 的典型操作语义，并定义采样基异质的语义来实现 MCMC 的 Tracing，并证明了分布语义与集成所有 Traces 的分布具有等价性，这是第一个针对高阶函数语言 Trace MCMC 的验证正确性的证明。
probabilistic programminglambda-calculusdistribution-based semanticsmarkov chain monte carloinference techniques
发现论文，激发创造
  • 概率编程的语义学：高阶函数，连续分布和软约束

    本文研究表达丰富的概率编程语言（如 Anglican，Church 和 Venture），分析它们的语义基础，运用测度论、随机标记转移系统和函子范畴，定义操作语义和标称语义，并证明其存在性、充分性、终止性，采用其来验证编译器优化和推理算法的正确性，研究了高阶函数上概率分布的性质。

    Jan, 2016

  • 高阶贝叶斯推断的指称验证

    我们提出一个模块化的语义计算方法，用于概率编程语言中的贝叶斯推断算法，并使用高阶函数和归纳类型等方式操纵概率程序的中间表示，定义了语义结构类及其转换的词义准则，并使用 Kock's 综合测度理论证明了一个准 Borel 同源定理。

    Nov, 2017

  • 运行概率程序的反向计算

    本篇研究论文提出一种牵涉到概率的编程语言，基于测度理论建立抽象语义学，实现贝叶斯推断、随机射线跟踪、以及浮点误差边界的概率验证

    Dec, 2014

  • 概率编程推断的新方法

    介绍和证明了一个基于粒子马尔可夫蒙特卡罗的新的推理方法。该方法适用于图灵完备的概率编程语言，支持使用复杂控制流（包括随机递归）的模型的准确推理，并包括来自贝叶斯非参数统计的基元。实验证明，该方法比之前介绍的单一站点 Metropolis-Hastings 方法更有效。

    Jul, 2015

  • 具有连续随机变量和递归的概率语言的上下文等价性

    我们提出了一个完整的论证原则，用于解决无类型的概率编程语言中的语境等效性问题，并证明了概率编程中的上下文等效性。

    Jul, 2018

  • 概率编程中的离散连续混合：广义语义和推断算法

    本篇研究开发了概率编程语言（PPLs）的度量叙事贝叶斯网络（MTBNs）的概念，并使用它来提供更多的语义，包括有限的支持组合离散和连续元素的随机变量。最终将 MTBNs 集成到广泛使用的概率编程语言系统 BLOG 中，并通过代表性的算例验证了新的推理算法的有效性。

    Jun, 2018

  • 动作的概率微积分

    本研究提出一种符号机制，能够处理有关概率和因果信息，从而推断出关于行动影响和观测影响的概率性语句，并利用条件概率和贝叶斯网络等技术来推导新的条件概率，以此量化行动效果和政策制定等方面的确认知识。

    Feb, 2013

  • 高阶概率理论的便捷类别

    介绍了赋予高阶函数和连续分布的概率编程语言的新概率论形式化 —— 拟 Borel 空间。展示了拟 Borel 空间可以替代标准可测空间、支持高阶函数、支持等式推理证明、同时支持连续概率分布，并将其运用于高阶函数与概率的理论证明。

    Jan, 2017

  • 概率逻辑推理

    本研究采用分布语义模型为基础，提出了描述逻辑的概率语义，设计了 TRILL P 系统，实现了对具有概率知识库的查询的概率计算和推理学习算法。

    May, 2014

  • 统计概率编程的领域理论

    本文为具有递归高阶类型、连续概率分布和软约束的语言提供了充分的指称语义，以建立计算统计和机器学习中使用的贝叶斯模型，其中包括类似于 Church 和 WebPPL 的无类型语言，因为我们的语义允许递归混合方差数据类型，并建立在 “拟 - 波雷尔代数” 之上，这些代数是链完整部分序列 (cpos) 和拟 - 波雷尔空间的混合。

    Nov, 2018