一句话：提出以超鞅见证不动点唯一性的统一框架，用于概率程序多种定量性质的下界验证。
概率程序的许多定量性质可刻画为最小不动点，但其下界验证仍具挑战。本文提出一种下界验证新方法，利用并扩展不动点唯一性与程序终止性之间的联系。核心技术工具是排序超鞅的推广，可作为不动点唯一性的见证。该方法给出简单统一的推理原则，适用于终止概率、最弱前期望、期望运行时间、运行时间高阶矩以及条件最弱前期望等多种定量性质。作者还提出基于模板的自动化验证算法，并通过实验证明方法的有效性。
Many quantitative properties of probabilistic programs can be characterized as least fixed points, but verifying their lower bounds remains a challenging problem. We present a new approach to lower-bound verification that exploits and extends the connection between the uniqueness of fixed points and program termination. The core technical tool is a generalization of ranking supermartingales, which serves as witnesses of the uniqueness of fixed points. Our method provides a simple and unified reasoning principle applicable to a wide range of quantitative properties, including termination probability, the weakest preexpectation, expected runtime, higher moments of runtime, and conditional weakest preexpectation. We provide a template-based algorithm for automated verification of lower bounds and demonstrate the effectiveness of the proposed method via experiments.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KuraUT26,
title = {Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification},
author = {Satoshi Kura and Hiroshi Unno and Takeshi Tsukada},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808348}
}