一句话：提出 Eris 高阶分离逻辑与错误信用，证明高阶概率程序的精确错误概率上界。
概率程序常以少量错误概率换取效率，但已有错误界验证方法要么过粗，要么仅适用于一阶程序。本文提出 Eris，一种面向高阶概率语言的分离逻辑，用于证明错误概率上界。核心是错误信用（error credits）：一种跟踪程序出错概率上界的分离逻辑资源。将错误界表示为资源带来组合性、模块性和错误与程序项的依赖，并支持保持期望的错误组合、摊销错误推理与错误归纳。作者在哈希函数碰撞概率等例子上证明摊销错误界，并证明拒绝采样算法的正确性与几乎必然终止。结果均在 Coq 中基于 Iris 与 Coquelicot 机器化验证。
Probabilistic programs often trade accuracy for efficiency, and thus may, with a small probability, return an incorrect result. It is important to obtain precise bounds for the probability of these errors, but existing verification approaches have limitations that lead to error probability bounds that are excessively coarse, or only apply to first-order programs. In this paper we present Eris, a higher-order separation logic for proving error probability bounds for probabilistic programs written in an expressive higher-order language. Our key novelty is the introduction of error credits , a separation logic resource that tracks an upper bound on the probability that a program returns an erroneous result. By representing error bounds as a resource, we recover the benefits of separation logic, including compositionality, modularity, and dependency between errors and program terms, allowing for more precise specifications. Moreover, we enable novel reasoning principles such as expectation-preserving error composition, amortized error reasoning, and error induction. We illustrate the advantages of our approach by proving amortized error bounds on a range of examples, including collision probabilities in hash functions, which allow us to write more modular specifications for data structures that use them as clients. We also use our logic to prove correctness and almost-sure termination of rejection sampling algorithms. All of our results have been mechanized in the Coq proof assistant using the Iris separation logic framework and the Coquelicot real analysis library.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{0001HMLGTB24,
title = {Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs},
author = {Alejandro Aguirre and Philipp G. Haselwarter and Markus de Medeiros and Kwing Hei Li and Simon Oddershede Gregersen and Joseph Tassarotti and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674635}
}