一句话：提出 Approxis：面向高阶概率程序近似等价的关系分离逻辑，支持误差信用与逻辑关系，并在 Coq/Iris 中机器化验证多个案例。
随机程序的可证明安全性与正确性常表示为程序间的近似等价，但已有近似关系逻辑多局限于无一般状态的一阶程序。本文提出 Approxis：一种面向类 ML 语言的高阶近似关系分离逻辑，支持离散概率采样、高阶函数和高阶状态。其关键是把 error credits 重铸到关系设定，以支持模块化组合、新的近似关系规则，并内化用近似证明精确概率等价的极限论证。作者还用 Approxis 构建量化 error credits 的逻辑关系模型，用以证明精确上下文等价。案例涵盖 PRP/PRF switching lemma、加密方案的 IND$-CPA 安全性和多种拒绝采样器。全部结果已在 Coq 与 Iris 中机器化。
Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational program logics have been developed to reason about such approximate equivalences of probabilistic programs. However, existing approximate relational logics are mostly restricted to first-order programs without general state. In this paper we develop Approxis, a higher-order approximate relational separation logic for reasoning about approximate equivalence of programs written in an expressive ML-like language with discrete probabilistic sampling, higher-order functions, and higher-order state. The Approxis logic recasts the concept of error credits in the relational setting to reason about relational approximation, which allows for expressive notions of modularity and composition, a range of new approximate relational rules, and an internalization of a standard limiting argument for showing exact probabilistic equivalences by approximation. We also use Approxis to develop a logical relation model that quantifies over error credits, which can be used to prove exact contextual equivalence . We demonstrate the flexibility of our approach on a range of examples, including the PRP/PRF switching lemma, IND$-CPA security of an encryption scheme, and a collection of rejection samplers. All of the results have been mechanized in the Coq proof assistant and the Iris separation logic framework.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2407-14107,
title = {Approximate Relational Reasoning for Higher-Order Probabilistic Programs},
author = {Philipp G. Haselwarter and Kwing Hei Li and Alejandro Aguirre and Simon Oddershede Gregersen and Joseph Tassarotti and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704877}
}