Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back

Kevin Batz, Joost-Pieter Katoen, Francesca Randone, Tobias Winkler

TL;DR

This work develops a principled, semi-automatic approach to verify bounds on expected outcomes of probabilistic programs that feature continuous distributions, conditioning, and unbounded loops. It replaces exact Lebesgue-integral computations in weakest pre-expectation semantics with sound lower and upper Riemann sum approximations, yielding transform families $\underline{\mathsf{wp}}^{N}$ and $\overline{\mathsf{wp}}^{N}$ that support SMT-based invariant verification. The authors prove soundness and convergence results (including coRE-completeness of central verification problems) and show how these approximations enable reusing existing discrete probabilistic verifiers, by encoding Riemann sums in Caesar’s intermediate language. The approach is demonstrated through case studies such as Monte Carlo style estimators, the Irwin-Hall distribution, and divergence/race scenarios, illustrating practical verification times and scalability. Overall, the paper provides a tractable pathway to soundly bound continuous probabilistic programs with loops and conditioning, bridging Lebesgue and Riemann perspectives and enabling integration with established verification tooling.

Abstract

We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops, (ii) continuous distributions, and (iii) conditioning. To handle loops we rely on user-provided quantitative invariants, as is well established. However, in the realm of continuous distributions, invariant verification becomes extremely challenging due to the presence of integrals in expectation-based program semantics. Our key idea is to soundly under- or over-approximate these integrals via Riemann sums. We show that this approach enables the SMT-based invariant verification for programs with a fairly general control flow structure. On the theoretical side, we prove convergence of our Riemann approximations, and establish coRE-completeness of the central verification problems. On the practical side, we show that our approach enables to use existing automated verifiers targeting discrete probabilistic programs for the verification of programs involving continuous sampling. Towards this end, we implement our approach in the recent quantitative verification infrastructure Caesar by encoding Riemann sums in its intermediate verification language. We present several promising case studies.

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back

TL;DR

This work develops a principled, semi-automatic approach to verify bounds on expected outcomes of probabilistic programs that feature continuous distributions, conditioning, and unbounded loops. It replaces exact Lebesgue-integral computations in weakest pre-expectation semantics with sound lower and upper Riemann sum approximations, yielding transform families and that support SMT-based invariant verification. The authors prove soundness and convergence results (including coRE-completeness of central verification problems) and show how these approximations enable reusing existing discrete probabilistic verifiers, by encoding Riemann sums in Caesar’s intermediate language. The approach is demonstrated through case studies such as Monte Carlo style estimators, the Irwin-Hall distribution, and divergence/race scenarios, illustrating practical verification times and scalability. Overall, the paper provides a tractable pathway to soundly bound continuous probabilistic programs with loops and conditioning, bridging Lebesgue and Riemann perspectives and enabling integration with established verification tooling.

Abstract

We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops, (ii) continuous distributions, and (iii) conditioning. To handle loops we rely on user-provided quantitative invariants, as is well established. However, in the realm of continuous distributions, invariant verification becomes extremely challenging due to the presence of integrals in expectation-based program semantics. Our key idea is to soundly under- or over-approximate these integrals via Riemann sums. We show that this approach enables the SMT-based invariant verification for programs with a fairly general control flow structure. On the theoretical side, we prove convergence of our Riemann approximations, and establish coRE-completeness of the central verification problems. On the practical side, we show that our approach enables to use existing automated verifiers targeting discrete probabilistic programs for the verification of programs involving continuous sampling. Towards this end, we implement our approach in the recent quantitative verification infrastructure Caesar by encoding Riemann sums in its intermediate verification language. We present several promising case studies.

Paper Structure

This paper contains 47 sections, 24 theorems, 46 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Guaranteed Bounds on Expected Outcomes via Weakest Pre-Expectations
  3. Problem Statement
  4. Approach
  5. Illustrative Example: A Monte Carlo Approximator.
  6. Loops and Invariants
  7. Contributions
  8. Paper Structure
  9. A Bird's Eye View
  10. Highlights and Comparison to Other Approaches
  11. An Alternative to Moment-Based Analyses
  12. General Conditional Branching
  13. Moving Backwards: Verification and Parametric Models
  14. A Zoo of Quantities
  15. Conditioning, Everywhere
  16. ...and 32 more sections

Key Result

theorem 1

Let $(L,\,\preceq)$ be an $\omega$-cpo with bottom and let $f \colon L \to L$ be $\omega$-continuous. Then $f$ has a least fixed point $\operatorname{lfp}f \in L$ and $\operatorname{lfp}f = \sup_{i \in \mathbb{N}} f^i(\bot)$ where $f^i(\bot)$ denotes the $i$-fold application of $f$ to $\bot$.

Figures (3)

  • Figure 1: Left: Monte-Carlo approximator $C$ for $\pi$ using ability \ref{['ability:sample']}. Right: 100 random samples.
  • Figure 2: Generating the standard Irwin-Hall distribution (left) and a variant with conditioning (right).
  • Figure 3: A probably diverging loop (left) and a race between tortoise and hare (right) DBLP:conf/sas/ChakarovS14.

Theorems & Definitions (36)

  • theorem 1: Kleene's Fixed Point Theorem DBLP:books/daglib/0070910
  • theorem 2: Knaster-Tarski Theorem DBLP:books/daglib/0070910
  • definition 1: Probabilistic Programs
  • Remark 1: More General Distributions
  • Remark 2: Soft Conditioning
  • definition 2: Expectations
  • lemma 1
  • definition 3: Weakest (Liberal) Pre-expectation Transformers DBLP:conf/setss/SzymczakK19
  • Remark 3: On Non-Negativity
  • theorem 3: Well-definedness of $\wpSymb$ and $\wlpSymb$
  • ...and 26 more