We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the case for existing rules -- and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice.

翻译：我们提出了一种新的证明规则，用于验证概率程序量的下界。该证明规则并不局限于几乎必然终止的程序——这与现有规则的情况不同——并且可用于为可能发散的概率循环（例如，众所周知的格点上的三维随机游走）建立非平凡的下界，例如终止概率和期望值。