Seminar Probabilistic Programming

Seminar in Theoretical CS, Winter Semester 2022/23

News

  • 26.10.2022: The student-topic-supervisor assignments are now available.
  • 17.10.2022: The slides of the introductory presentation are now online.
  • 02.06.2022: We are online!

Introduction and Assignment of Topics

Dates & Deadlines

20.10.2022Topic preferences due
21.11.2022Detailed outline due
22.12.2022Full report due
13.01.2023Presentation slides due
06.02./07.02.2023Seminar talks

Note that the full versions of your report and your slides should be your final submission and the camera-ready versions should differ only with regard to minor remarks, comments, and corrections by your supervisor. Please feel free, however, to talk to your supervisor about submitting preliminary versions before the due dates.

Overview

This seminar covers a variety of topics in the field of probabilistic programs. Roughly speaking, probabilistic programs are like ordinary programs, with an extra feature: the ability to make some sort of probabilistic choice. Here we show how one can exploit this feature to model, for instance, a duel between two cowboys. Describing randomized algorithms has been the classical application of these programs. Applications in biology, machine learning, quantum computing, security, and so on, have led to a rapidly growing interest in probabilistic programs in the last decade. For almost all programming languages, such as C, C#, Prolog, Haskell, Scala, LISP, a probabilistic variant does exist; and even a variant of Microsoft’s Excel has been developed – see the corresponding Wikipedia entry.

The topics considered in this seminar are mostly based on the book Foundations of Probabilistic Programming (edited by Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva and freely accessible). It contains 15 surveying chapters by different (teams of) authors, divided into five parts:

  1. Semantics,
  2. Verification.,
  3. Logic,
  4. Security, and
  5. Programming languages.

Additionally, we include some recent papers dealing with several different research areas in the field of probabilistic programs.

Prerequisites

Basic knowledge in the following areas is expected:

  • Probability theory
  • Automata theory
  • Mathematical logic

Topics

(Move the cursor over the entry to see the corresponding abstract.)

Chapters of Foundations of Probabilistic Programming:

  1. [Semantics] (Ch.1) Fredrik Dahlqvist, Dexter Kozen, Alexandra Silva: Semantics of Probabilistic Programming: A Gentle Introduction (44 pages) (B)
  2. [Semantics] (Ch.2) Sam Staton: Probabilistic Programs as Measures (35 pages) (M)
  3. [Semantics] (Ch.4) Ugo Dal Lago: On Probabilistic Lambda-Calculi (27 pages) (M)
  4. [Verification] (Ch.5) Gilles Barthe, Justin Hsu: Probabilistic Couplings from Program Logics (43 pages) (M)
    • Student: Zihan Zhou
    • Supervisor: Raphaël Berthon
  5. [Verification] (Ch.6) Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja: Expected Runtime Analysis by Program Verification (39 pages) (B)
  6. [Verification] (Ch.7) Krishnendu Chatterjee, Hongfei Fu, Petr Novotný: Termination Analysis of Probabilistic Programs with Martingales (41 pages) (M)
  7. [Verification] (Ch.8) Sriram Sankaranarayanan: Quantitative Analysis of Programs with Probabilities and Concentration of Measure Inequalities (40 pages) (M)
    • Student: –
    • Supervisor: –
  8. [Programming languages] (Ch.13) Lampropoulos Leonidas, Benjamin C. Pierce, Li-yao Xia, Diane Gallois-Wong, Catalin Hritcu, John Hughes: Luck: A Probabilistic Language for Testing (44 pages) (B)
  9. [Programming languages] (Ch.14) Andrew D. Gordon, Claudio Russo, Marcin Szymczak, Johannes Borgström, Nicolas Rolland, Thore Graepel, Daniel Tarlow: Tabular: Probabilistic Inference from the Spreadsheet (47 pages) (B)
  10. [Programming languages] (Ch.15) Michael Carbin, Sasa Misailovic: Programming Unreliable Hardware (39 pages) (B)

Additional Papers

  1. Zixin Huang, Saikat Dutta, Sasa Misailovic: Automated quantized inference for probabilistic programs with AQUA. Innov. Syst. Softw. Eng. 18(3): 369-384 (2022) (M)
    • Student: Hanbin Chen
  2. Gilles Barthe, Charlie Jacomme, Steve Kremer: Universal Equivalence and Majority of Probabilistic Programs over Finite Fields. ACM Trans. Comput. Log. 23(1): 5:1-5:42 (2022) (M)
    • Student: –
    • Supervisor: –
  3. Marcelo Navarro, Federico Olmedo: Slicing of Probabilistic Programs Based on Specifications (Extended Abstract). ECOOP 2022: 34:1-34:2 (B)
    • Student: Christopher Zeise
  4. Alessandro Abate, Mirco Giacobbe, Diptarko Roy: Learning Probabilistic Termination Proofs. CAV (2) 2021: 3-26 (B)
    • Student: Nils Sommerfeld
  5. Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti: A separation logic for negative dependence. Proc. ACM Program. Lang. 6(POPL): 1-29 (2022) (M)
    • Student: –
    • Supervisor: –
  6. Di Wang, Jan Hoffmann, Thomas W. Reps: A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism. MFPS 2019: 303-324 (B/M)
    • Student: –
    • Supervisor: –
  7. Daniel J. Fremont, Edward Kim, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli & Sanjit A. Seshia: Scenic: A language for scenario specification and data generation. Machine Learning (2022)(B)
    • Student: (1) Farid Qasimov, (2) Luca Kempkes
  8. Timon Gehr, Samuel Steffen, Martin T. Vechev: λPSI: exact inference for higher-order probabilistic programs. PLDI 2020: 883-897 (B)
    • Student: Rika Kade
  9. Raven Beutner, C.-H. Luke Ong, and Fabian Zaiser: Guaranteed bounds for posterior inference in universal probabilistic programming. PLDI 2022: 536–551 (M)
    • Student: –
    • Supervisor: –

Registration

Registration to the seminar is handled via the SuPra system.

Grading Scheme

You can access the grading scheme here: https://moves.rwth-aachen.de/wp-content/uploads/seminar_grading_scheme.pdf

Additional Material

Contact

Joost-Pieter Katoen