AI 中文总结
本文提出面向Liquid Haskell的成本感知概率单子，结合可执行概率程序与精化类型验证、SMT自动化，在经典概率算法上验证了其支持概率程序期望成本推理的有效性。
AI 中文摘要
概率算法与数据结构被广泛用于获得良好的期望性能保证，尽管其数学分析已被充分理解，但实现期望成本分析的机械化仍具挑战性，需要对概率分布、期望及递归随机行为进行推理。现有形式化方法常需大量手动证明工作，因为期望成本常与概率计算分开编码，必须在整个证明中显式传播。本文提出一种面向\textbf{LH}（Liquid Haskell）的成本感知概率单子，支持对概率程序及其期望成本进行推理。该方法将可执行概率程序与基于精化类型的验证、SMT支持的自动化相结合，单子通过精化类型内在地跟踪概率质量、期望和期望成本，使概率计算的许多定量属性能从程序结构中组合推断。我们在多个经典概率算法与数据结构上评估该方法，包括可合并堆、随机快速排序与快速选择、随机伸展树、随机排列及招聘问题，案例研究展示了自动化与交互式验证之间的不同应用场景。
英文摘要
Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mechanising expected-cost analyses remains challenging, requiring reasoning about probability distributions, expectations, and recursive stochastic behaviour. Existing formal approaches frequently require substantial manual proof effort, since expected costs are often encoded separately from probabilistic computations and must therefore be propagated explicitly throughout proofs. In this paper, we present a cost-aware probability monad for \LH/ that supports reasoning about probabilistic programs together with their expected costs. Our approach combines executable probabilistic programs with refinement-type-based verification and SMT-supported automation. The monad intrinsically tracks probability mass, expected values, and expected costs through refinement types, enabling many quantitative properties of probabilistic computations to be inferred compositionally from program structure. We evaluate our approach on several classical probabilistic algorithms and data structures, including meldable heaps, randomised quicksort and quickselect, randomised splay trees, random permutations, and the hiring problem. The case studies demonstrate different points along the spectrum between automated and interactive verification.
CommentsAccepted at 19th ACM SIGPLAN International Symposium on Haskell 2026
