Seminar Probabilistic Programming

Seminar in Theoretical CS, Winter Semester 2024/25

News

  • 16.10.2024: Topics assigned to students and supervisors.
  • 12.10.2024: Uploaded introduction slides and topic preferences form.
  • 06.06.2024: We are online!

Introduction and Assignment of Topics

Dates & Deadlines

Fri, Oct 11, 10:00Kick-off meeting (room 4201b, 2nd floor, building E1, CS Department)
Tue, Oct 15, 23:59Topic preferences due
Mon, Nov 11, 23:59Detailed outline and one page of initial text due
Mon, Dec 9, 23:59Full report due
Mon, Jan 13, 23:59Presentation slides due
Feb 3-5 (?)Presentations (room 4201b, 2nd floor, building E1, CS Department)

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.

Prerequisites

Basic knowledge in the following areas is expected:

  • Probability theory
  • Automata theory
  • Mathematical logic

Topics

Note that the list of topics is not yet final.

A. Semantics

  1. Jules Jacobs: Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities. Proc. ACM Program. Lang. 5(POPL): 1-26 (2021)
  2. David Chiang, Colin McDonald, Chung-chieh Shan: Exact Recursive Probabilistic Programming. Proc. ACM Program. Lang. 7(OOPSLA1): 665-695 (2023)
  3. John M. Li, Amal Ahmed, Steven Holtzen: Lilac: A Modal Separation Logic for Conditional Probability. Proc. ACM Program. Lang. 7(PLDI): 148-171 (2023)
    • Student:
    • Supervisor:
  4. Noam Zilberstein, Derek Dreyer, Alexandra Silva: Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proc. ACM Program. Lang. 7(OOPSLA1): 522-550 (2023)
  5. Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja: A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5(POPL): 1-28 (2021)

B. Verification

  1. Rupak Majumdar, V. R. Sathiyanarayana: Positive Almost-Sure Termination: Complexity and Proof Rules. Proc. ACM Program. Lang. 8(POPL): 1089-1117 (2024)
    • Student:
    • Supervisor:
  2. Julian Müllner, Marcel Moosbrugger, Laura Kovács: Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. Proc. ACM Program. Lang. 8(POPL): 882-910 (2024)
  3. Rupak Majumdar, V. R. Sathiyanarayana: Sound and Complete Proof Rules for Probabilistic Termination. CoRR abs/2404.19724 (2024)
  4. Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal: Almost-Sure Termination by Guarded Refinement. CoRR abs/2404.08494 (2024)
  5. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiri Zárevúcky, Dorde Zikelic: On Lexicographic Proof Rules for Probabilistic Termination. Formal Aspects Comput. 35(2): 11:1-11:25 (2023)
    • Student:
    • Supervisor:
  6. Michael J. Butler, Pieter H. Hartel: Reasoning about Grover’s quantum search algorithm using probabilistic wp. ACM Trans. Program. Lang. Syst. 21(3): 417-429 (1999)

C. Program Analysis

  1. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Dorde Zikelic: Equivalence and Similarity Refutation for Probabilistic Programs. Proc. ACM Program. Lang. 8(PLDI): 2098-2122 (2024)
  2. Jianlin Li, Eric Wang, Yizhou Zhang: Compiling Probabilistic Programs for Variable Elimination with Information Flow. Proc. ACM Program. Lang. 8(PLDI): 1755-1780 (2024)
  3. Poorva Garg, Steven Holtzen, Guy Van den Broeck, Todd D. Millstein: Bit Blasting Probabilistic Programs. Proc. ACM Program. Lang. 8(PLDI): 865-888 (2024)
  4. Francesca Randone, Luca Bortolussi, Emilio Incerto, Mirco Tribastone: Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures. Proc. ACM Program. Lang. 8(POPL): 1882-1912 (2024)

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

Philipp Schroer