一句话：提出 PPV 逻辑族，用于验证带连续分布和高阶函数概率程序的近似、收敛、贝叶斯推断与优化性质。
概率编程语言常结合连续分布、条件化与高阶函数，表达力强但给程序语义与验证带来根本挑战，已有工作多聚焦基础语义。本文提出逻辑族 PPV，用于证明这类高阶概率程序的属性，支持对近似、收敛、贝叶斯推断和优化的推理。PPV 通过精心选取概率论结果的公理，模拟非形式证明的推理风格；其可靠性基于 quasi-Borel spaces（QBS）解释程序与断言。作者还给出已有逻辑的可靠嵌入，并以参数化方式将一元与关系型 ⊤⊤-lifting 的语义思想内化到逻辑中。最后，通过对统计学、概率推断和机器学习中的多个复杂例子进行形式验证，展示其实用性与表达力。
Probabilistic programming provides a convenient lingua franca for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic programming languages, including Anglican, Church or Hakaru, derive their expressiveness from a powerful combination of continuous distributions, conditioning, and higher-order functions. Although very important for practical applications, these features raise fundamental challenges for program semantics and verification. Several recent works offer promising answers to these challenges, but their primary focus is on foundational semantics issues. In this paper, we take a step further by developing a suite of logics, collectively named PPV for proving properties of programs written in an expressive probabilistic higher-order language with continuous sampling operations and primitives for conditioning distributions. Our logics mimic the comfortable reasoning style of informal proofs using carefully selected axiomatizations of key results from probability theory. The versatility of our logics is illustrated through the formal verification of several intricate examples from statistics, probabilistic inference, and machine learning. We further show expressiveness by giving sound embeddings of existing logics. In particular, we do this in a parametric way by showing how the semantics idea of (unary and relational) ⊤⊤-lifting can be internalized in our logics. The soundness of PPV follows by interpreting programs and assertions in quasi-Borel spaces (QBS), a recently proposed variant of Borel spaces with a good structure for interpreting higher order probabilistic programs.
@article{paperbot681,
title = {Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization},
author = {Tetsuya Sato and Alejandro Aguirre and Gilles Barthe and Marco Gaboardi and Deepak Garg and Justin Hsu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290351}
}