Technical reports
Formal verification of probabilistic algorithms
May 2003, 154 pages
This technical report is based on a dissertation submitted December 2001 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Trinity College.
DOI: 10.48456/tr-566
Abstract
This thesis shows how probabilistic algorithms can be formally verified using a mechanical theorem prover.
We begin with an extensive foundational development of probability, creating a higher-order logic formalization of mathematical measure theory. This allows the definition of the probability space we use to model a random bit generator, which informally is a stream of coin-flips, or technically an infinite sequence of IID Bernoulli(1/2) random variables.
Probabilistic programs are modelled using the state-transformer monad familiar from functional programming, where the random bit generator is passed around in the computation. Functions remove random bits from the generator to perform their calculation, and then pass back the changed random bit generator with the result.
Our probability space modelling the random bit generator allows us to give precise probabilistic specifications of such programs, and then verify them in the theorem prover.
We also develop technical support designed to expedite verification: probabilistic quantifiers; a compositional property subsuming measurability and independence; a probabilistic while loop together with a formal concept of termination with probability 1. We also introduce a technique for reducing properties of a probabilistic while loop to properties of programs that are guaranteed to terminate: these can then be established using induction and standard methods of program correctness.
We demonstrate the formal framework with some example probabilistic programs: sampling algorithms for four probability distributions; some optimal procedures for generating dice rolls from coin flips; the symmetric simple random walk. In addition, we verify the Miller-Rabin primality test, a well-known and commercially used probabilistic algorithm. Our fundamental perspective allows us to define a version with strong properties, which we can execute in the logic to prove compositeness of numbers.
Full text
PDF (0.9 MB)
BibTeX record
@TechReport{UCAM-CL-TR-566,
author = {Hurd, Joe},
title = {{Formal verification of probabilistic algorithms}},
year = 2003,
month = may,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-566.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-566},
number = {UCAM-CL-TR-566}
}