Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


Bagnall Accepted Dissertation SP23.pdf (1.5 MB)

ETD Abstract Container

Abstract Header

Formally Verified Samplers From Discrete Probabilistic Programs

Bagnall, Alexander
http://orcid.org/0000-0001-6593-0661
http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1680288961557783

Abstract Details

2023, Doctor of Philosophy (PhD), Ohio University, Electrical Engineering & Computer Science (Engineering and Technology).
This dissertation presents Zar: a formally verified compilation pipeline from discrete probabilistic programs in the conditional probabilistic guarded command language (cpGCL) to proved-correct executable samplers in the random bit model. Zar exploits the key idea that discrete probability distributions can be reduced to unbiased coin-flipping schemes. The compiler pipeline first translates cpGCL programs into choice-fix trees, an intermediate representation suitable for reduction of biased probabilistic choices. Choice-fix trees are then translated to coinductive interaction trees for execution within the random bit model. The correctness of the composed translations establishes the sampling equidistribution theorem: compiled samplers are correct with respect to the conditional weakest pre-expectation (cwp) semantics of their cpGCL source programs. Zar is implemented and fully verified in the Coq proof assistant. We extract verified samplers to OCaml and Python and empirically validate them on a number of illustrative examples. We additionally present AlgCo (Algebraic Coinductives), a practical framework for inductive reasoning over coinductive types such as conats, streams, and infinitary trees with finite branching factor, developed during the course of this work to enable convenient formal reasoning for coinductive samplers generated by Zar. The key idea is to exploit the notion of algebraic CPO from domain theory to define continuous operations over coinductive types via primitive recursion on "dense" collections of their elements, enabling a convenient strategy for reasoning about algebraic coinductives by straightforward proofs by induction. We implement the AlgCo library in Coq and demonstrate its utility by verifying a stream variant of the sieve of Eratosthenes, a regular expression library based on coinductive tries, and weakest pre-expectation semantics for potentially nonterminating sampling processes over discrete probability distributions in the random bit model.
David Juedes (Advisor)
James Stewart (Committee Member)
Vladimir Uspenskiy (Committee Member)
Jundong Liu (Committee Member)
Anindya Banerjee (Committee Member)
David Chelberg (Committee Member)
187 p.
Computer Science
Zar; cpGCL; compiler; probabilistic programming; theorem proving; verification; induction; coinduction; algebraic CPO; domain theory

Recommended Citations

Citations

  • Bagnall, A. (2023). Formally Verified Samplers From Discrete Probabilistic Programs [Doctoral dissertation, Ohio University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1680288961557783

    APA Style (7th edition)

  • Bagnall, Alexander. Formally Verified Samplers From Discrete Probabilistic Programs. 2023. Ohio University, Doctoral dissertation. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1680288961557783.

    MLA Style (8th edition)

  • Bagnall, Alexander. "Formally Verified Samplers From Discrete Probabilistic Programs." Doctoral dissertation, Ohio University, 2023. http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1680288961557783

    Chicago Manual of Style (17th edition)

ohiou1680288961557783
444
© 2023, all rights reserved.
This open access ETD is published by Ohio University and OhioLINK.