一句话：提出基于 k-归纳的分段定量分析方法，为概率程序合成更紧的分段多项式界。
现有概率程序定量分析多在整个状态空间上寻求单一数值界，往往过于保守或缺乏表达力。本文提出分段界合成方法：首先从格化 k-归纳算子中提取有用分段信息，并结合可选停时定理，给出推导概率程序分段界的一般框架；随后给出分段多项式界合成算法，在线性情形归约到双线性规划，在多项式情形可靠松弛为半定规划。实验表明，与当前最优方法相比，该方法在大量基准上能生成更紧的分段界。
In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most previous works consider numerical bounds over the whole program state space monolithically and do not consider piecewise bounds. Not surprisingly, monolithic bounds are either conservative, or not expressive and succinct enough in general. To derive better bounds, we propose a novel approach for synthesizing piecewise bounds over probabilistic programs. First, we show how to extract useful piecewise information from latticed 𝑘-induction operators, and combine the piecewise information with Optional Stopping Theorem to obtain a general approach to derive piecewise bounds over probabilistic programs. Second, we develop algorithms to synthesize piecewise polynomial bounds, and show that the synthesis can be reduced to bilinear programming in the linear case, and soundly relaxed to semidefinite programming in the polynomial case. Experimental results show that our approach generates tight piecewise bounds for a wide range of benchmarks when compared with the state of the art.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{YangFFZKW26,
title = {Piecewise Analysis of Probabilistic Programs via 𝑘-Induction},
author = {Tengshun Yang and Shenghua Feng and Hongfei Fu and Naijun Zhan and Jingyu Ke and Shiyang Wu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776709}
}