# Lower Bounds for Possibly Divergent Probabilistic Programs

arXiv: https://arxiv.org/abs/2302.06082 · HTML: https://mlsanity.com/paper/2302.06082/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Feb 2023.

## Built on by (most cited first, 2 of 2)

- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [Quantitative Verification of Omega-regular Properties in Probabilistic Programming](https://mlsanity.com/paper/2512.21596/) (2025)

## Abstract (arXiv)

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.