Probabilistic Programming

News

  • 12.12.2018: on slide 29 of lecture 14+15, there was a typo in the bracketing of the progress condition. A new version of the notes of lecture 14+15 has been updated.
  • 11.12.2018: the last lectures in 2018 take place on December 18 and 20. The last lecture of this course takes place January 10, 2019.
  • 27.11.2018: on the last slide of Lecture #11 the statement cwp(P, (f, 1)) = (Q,f) should read cwp(P, (f,1)) = wp(Q,f). We also updated exercise sheet 6 accordingly.
  • 24.11.2018: the exercise class on Friday 7.12 will take place during the lecture slot on Thursday 6.12. So instead of a lecture, there will be an exercise class on 6.12 and no exercise class on 7.12.
  • 24.11.2018: on slide 21 of lecture 8+9 the following premise has to be added: I is a wp–subinvariant of while(G) P with respect to f.
  • 07.11.2018: Besides the plain and annotated slides, for some of the lectures additional material is made available. This material is meant as background material. Its usage is recommended but optional. Some of the notations in this material are slightly different from the lecture, and some issues are treated in a more general, extensive manner.
  • 05.11.2018: Please notice that the lecture on Thursday, 08.11.2018, and the exercise class on Friday, 09.11.2018, have been swapped. The exercise class will take place on Thursday in room 5055 and the lecture will take place on Friday in room 5056, respectively. Furthermore, notice that this means that the third exercise sheet is due on Thursday, 08.11.2018.
  • 02.11.2018: If you hand in your exercises via L2P, we kindly ask you to hand in a single PDF file. Moreover, please do not handing in scanned pages. If you cannot hand in right before the lecture, it is possible to hand in exercises at our chair.
  • 25.10.2018: a more precise definition of periodic states (Lecture 3, slide 27) is given here:
  • 20.10.2018: an update of the slides of Lecture 3 has been uploaded.
  • 19.10.2018: Please notice that you have to search for “probabilistic programming” or “probabilistische Programmierung” among all courses in RWTH Online to register for the course.
  • 11.10.2018: To get a better idea about the kind of exercises you will encounter throughout the course, you can find some old exercises on our old website.
  • 09.10.2018: The first three lectures take place on Thu October 11, Thu October 18 and Fri October 19.
  • 11.09.2018: Please notice that (despite different information in RWTHonline) students will be awarded 6 ECTS credits for the lecture after passing the final exam.

Schedule

Type Day Time Hall Start Lecturer
Lecture Tue  14:30 – 16:00 5052 23.10 Katoen
  Thu 14:30 – 16:00 5055 11.10 Katoen
Exercise Fri 14:30 – 16:00 5056 26.10 Matheja

Motivation and background

Probabilistic programs support random choices like “execute program P with probability 1/3 and program Q with probability 2/3″. Probabilistic programs are typically normal–looking sequential programs describing posterior probability distributions. 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 probabilistic-programming.org.

Most of these languages feature, in addition to sampling from probability distributions, the ability to condition values of variables in a program. Conditioning allows for adding information about observed events into the program that may influence the posterior distribution. It is one of the key features in Bayesian networks that rely on Bayes’ rule as the basis for updating information. It is this feature that distinguishes modern probabilistic programming languages from those in the early days describing randomized algorithms. 

What is special about probabilistic programs? Although probabilistic programs are normal–looking programs, reasoning about their correctness is intricate. They do not generate a single output but a distribution over outputs. The key property of program termination exemplifies this. Whereas a classical program terminates or not, this is no longer true for probabilistic programs. They can diverge, but this may happen with probability zero. That is, even if programs terminate with probability one, they may have non-terminating runs!  In addition, in contrast to classical programs that either do not terminate at all or terminate in finitely many steps, a probabilistic program may take infinitely many steps on average to terminate, even if its termination probability is one.

Establishing correctness of probabilistic programs needs—even more so than ordinary programs—formal reasoning.

This lecture series will introduce the probabilistic programming language webppl, a functional language based on JavaScript with a simple web interface.  Subsequently, we will go into elementary questions such as:

  • What do probabilistic programs mean?  Exactly.
  • What does it mean for a program to not terminate with some likelihood?
  • How to analyze that a probabilistic program does what it is supposed to do?
  • How to prove that a probabilistic program is (more) efficient?
  • What are Bayesian networks and how are they related to probabilistic programs?

screen-shot-2016-10-18-at-13-19-24

Prerequisites

Basic knowledge of programming and probability theory.

Exercises

  • To achieve a certificate to this course or to be admitted to the final exam, at least half of the exercises has to be reasonably dealt.
  • The exercise sheets will be issued weekly. The first exercise sheet will be made available here on October 19, 2018.

Slides

Lecture Date Topic Slides Notes Exercises Syllabus
1 Oct 11  Introduction PP2018_Lec1      
2 Oct 18 WebPPL  

WebPPL-

examples

ex01  
3 Oct 19 Markov chains PP2018_Lec3 Notes3    
4 Oct 23 Probabilistic GCL PP2018_Lec4 Notes4 ex02 pGCL
5 Oct 25 Domain theory PP2018_Lec5 Notes5    
6 Oct 30 Weakest preconditions PP2018_Lec6 Notes6 ex03 dijkstra_wp
7 Nov 6 Probabilistic weakest preconditions PP2018_Lec7 Notes7+8A ex04 probabilistic-wp
8 Nov 9 Loop invariants (1) PP2018_Lec8+9     loop-invariants
9 Nov 13 Loop invariants (2)   Notes8B+9 ex05  
10 Nov 15 Conditioning PP2018_Lec10 Notes10 ex06  
11 Nov 20 Conditioning with weakest preconditions PP2018_Lec11 Notes11   conditioning
12 Nov 27 Hardness of computing weakest preconditions PP2018_Lec12 Notes12 ex07  
13 Nov 29 Hardness of almost-sure termination PP2018_Lec13 Notes13    
14 Dec 4 Proving almost-sure termination PP2018_Lec14   ex08  
15 Dec 11     Notes14+15    
16 Dec 13 Runtime Analysis        
17 Dec 18 Runtime Analysis        
18 Dec 20 Nondeterminism        
19 Jan 8 Bayesian networks        
20 Jan 10 Analysing Bayesian networks        

Exam

  • Written exam on: February 25, 2019 (10:00-12:00) and March 27, 2019 (10:00-12:00)

Further information

  • The lecture will be given in English. All course material will be in English.
  • The students will be awarded 6 ECTS credits for the lecture after passing the final exam. The current indication in RWTHOnline is (unfortunately) incorrect.
Literature

The course is based several research papers and material from several books: