Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a 20-minute conference talk from PLDI 2023 that introduces Zar, a formally verified compiler pipeline for discrete probabilistic programs. Learn how Zar translates programs with unbounded loops in the conditional probabilistic guarded command language (cpGCL) into proved-correct executable samplers using the random bit model. Discover the key concept of reducing all discrete probability distributions to unbiased coin-flipping schemes. Examine the compilation process, including the translation to choice-fix trees and coinductive interaction trees. Understand the sampling equidistribution theorem that establishes the correctness of compiled samplers. Gain insights into the implementation and verification in Coq, as well as the extraction of verified samplers to OCaml and Python. See empirical validations on illustrative examples and explore the available artifacts evaluated as reusable.
Syllabus
[PLDI'23] Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning
Taught by
ACM SIGPLAN
Related Courses
Verifying the LLVMStrange Loop Conference via YouTube Beweisbar sichere Software
media.ccc.de via YouTube RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story
Rust via YouTube Building Measure Theory Using Hierarchy Builder
Hausdorff Center for Mathematics via YouTube Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
GOTO Conferences via YouTube