一句话：受概率耦合启发扩展精化类型，在 Liquid Haskell 中验证概率计算的关系性质与机器学习实现。
论文研究如何为概率计算的关系性质提供类型化推理。作者受概率耦合启发，扩展精化类型，使其能表达并验证诸如期望敏感度等性质：两个概率计算输出之间的距离可由输入距离控制。作者在 Liquid Haskell 的类型系统中实现这些机制，并用其形式验证两个经典机器学习算法的 Haskell 实现：时序差分（TD）强化学习和随机梯度下降（SGD）。此外，作者为离散分布形式化系统的一个片段，并相对于集合论语义证明其可靠性。该工作将耦合推理与精化类型结合，支持对概率程序进行模块化、可机检的验证。
We enhance refinement types with mechanisms to reason about relational properties of probabilistic computations. Our mechanisms, which are inspired from probabilistic couplings, are applicable to a rich set of probabilistic properties, including expected sensitivity, which ensures that the distance between outputs of two probabilistic computations can be controlled from the distance between their inputs. We implement our mechanisms in the type system of Liquid Haskell and we use them to formally verify Haskell implementations of two classic machine learning algorithms: Temporal Difference (TD) reinforcement learning and stochastic gradient descent (SGD). We formalize a fragment of our system for discrete distributions and we prove soundness with respect to a set-theoretical semantics.
@article{paperbot1485,
title = {Safe couplings: coupled refinement types},
author = {Elizaveta Vasilenko and Niki Vazou and Gilles Barthe},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547643}
}