一句话：为高阶概率对抗计算建立一元与关系程序逻辑，并在准 Borel 空间范畴中证明可靠性。
对抗计算中，资源受限的概率对手可调用带私有状态的预言机，广泛出现于安全、隐私与机器学习。论文在高阶设定下为此类计算设计程序逻辑：以带概率与状态分级单子的简单类型 λ 演算为语言，用分级约束内存占用与预言机调用代价；对手被表示为以预言机代码为参数的高阶表达式。作者给出推理错误概率与期望值的一元逻辑，以及推理耦合性质的关系逻辑，规则保证对所有满足固定资源策略的对手有效；并在准 Borel 空间范畴中用分级谓词提升及其逻辑关系证明逻辑与对手规则的可靠性。示例展示逻辑的用法。
Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, including security, privacy and machine learning. In this paper, we develop program logics for reasoning about adversarial computations in a higher-order setting. Our logics are built on top of a simply typed λ-calculus extended with a graded monad for probabilities and state. The grading is used to model and restrict the memory footprint and the cost (in terms of oracle calls) of computations. Under this view, an adversary is a higher-order expression that expects as arguments the code of its oracles. We develop unary program logics for reasoning about error probabilities and expected values, and a relational logic for reasoning about coupling-based properties. All logics feature rules for adversarial computations, and yield guarantees that are valid for all adversaries that satisfy a fixed resource policy. We prove the soundness of the logics in the category of quasi-Borel spaces, using a general notion of graded predicate liftings, and we use logical relations over graded predicate liftings to establish the soundness of proof rules for adversaries. We illustrate the working of our logics with simple but illustrative examples.
@article{paperbot1113,
title = {Higher-order probabilistic adversarial computations: categorical semantics and program logics},
author = {Alejandro Aguirre and Gilles Barthe and Marco Gaboardi and Deepak Garg and Shin-ya Katsumata and Tetsuya Sato},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473598}
}