Formal Verification of Higher-Order Probabilistic Programs
Probabilistic programming provides a convenient lingua franca for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic programming languages, including Anglican, Church or Hakaru, derive their expressiveness from a powerful combination of continuous distributions, conditioning, and higher-order functions. Although very important for practical applications, these combined features raise fundamental challenges for program semantics and verification. Several recent works offer promising answers to these challenges, but their primary focus is on semantical issues.
In this paper, we take a step further and we develop a set of program logics, named PPV for proving properties of programs written in an expressive probabilistic higher-order language with continuous distributions and operators for conditioning distributions by real-valued functions. Pleasingly, our program logics retain the comfortable reasoning style of informal proofs thanks to carefully selected axiomatizations of key results from probability theory. The versatility of our logics is illustrated through the formal verification of several intricate examples from statistics, probabilistic inference, and machine learning. We further show the expressiveness of our logics by giving sound embeddings of existing logics. In particular, we do this in a parametric way by showing how the semantics idea of (unary and relational) $\top\top$-lifting can be internalized in our logics. The soundness of PPV follows by interpreting programs and assertions in quasi-Borel spaces (QBS), a recently proposed variant of Borel spaces with a good structure for interpreting higher order probabilistic programs.
Wed 16 JanDisplayed time zone: Belfast change
10:35 - 12:03
Reasoning about Probabilistic ProgramsResearch Papers at Sala I
Chair(s): Jan Hoffmann Carnegie Mellon University
|Formal Verification of Higher-Order Probabilistic Programs|
Tetsuya Sato University at Buffalo, SUNY, USA, Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Justin Hsu University of Wisconsin-Madison, USALink to publication DOI Media Attached File Attached
|A Separation Logic for Concurrent Randomized Programs|
Joseph Tassarotti Carnegie Mellon University, Robert HarperLink to publication DOI Media Attached File Attached
|Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs|
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen UniversityLink to publication DOI Media Attached File Attached
|Trace Abstraction Modulo Probability|
Calvin Smith University of Wisconsin - Madison, Justin Hsu University of Wisconsin-Madison, USA, Aws Albarghouthi University of Wisconsin-MadisonLink to publication DOI Media Attached