一句话：提出依赖细化类型系统，将高阶概率程序的多种定量性质验证归约到扩展 CHC 求解，并可复用现有求解器。
本文研究高阶概率程序的自动验证，目标覆盖最弱前置期望、期望代价、代价矩以及条件最弱前置期望等定量性质，并支持连续分布与条件化。为避免为概率扩展重造验证工具，作者提出一种面向广义高阶不动点逻辑（HFL）的依赖细化类型系统，并通过 CPS 编码将性质嵌入 HFL。其可靠性在范畴语义框架下统一证明。实现上，类型检查被归约为扩展约束 Horn 子句（CHC），引入 admissible 与 integrable 谓词变量以可靠处理最小不动点和概率采样，从而只需少量工作即可复用现有非概率 CHC 求解器。实验在多个具体例子上展示了类型检查器的验证能力。
Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to handle the quantitative aspects of probabilistic programs often entails extensive modifications to existing tools, reducing compatibility with advanced techniques developed for qualitative verification. In contrast, our approach necessitates only small amounts of modification, facilitating the reuse of existing techniques and implementations. On the theoretical side, we propose a dependent refinement type system for a generalised higher-order fixed point logic (HFL). Combined with continuation-passing style encodings of properties into HFL, our dependent refinement type system enables reasoning about several quantitative properties, including weakest pre-expectations, expected costs, moments of cost, and conditional weakest pre-expectations for higher-order probabilistic programs with continuous distributions and conditioning. The soundness of our approach is proved in a general setting using a framework of categorical semantics so that we don’t have to repeat similar proofs for each individual problem. On the empirical side, we implement a type checker for our dependent refinement type system that reduces the problem of type checking to constraint solving. We introduce admissible predicate variables and integrable predicate variables to constrained Horn clauses (CHC) so that we can soundly reason about the least fixed points and samplings from probability distributions. Our implementation demonstrates that existing CHC solvers developed for non-probabilistic programs can be extended to a solver for the extended CHC with only small efforts. We also demonstrate the ability of our type checker to verify various concrete examples.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2407-02975,
title = {Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System},
author = {Satoshi Kura and Hiroshi Unno},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674662}
}