Dagstuhl Seminar 23241
Scalable Analysis of Probabilistic Models and Programs
( Jun 11 – Jun 16, 2023 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/23241
Organizers
- Sebastian Junges (Radboud University Nijmegen, NL)
- Joost-Pieter Katoen (RWTH Aachen, DE)
- Scott Sanner (University of Toronto, CA)
- Guy Van den Broeck (UCLA, US)
Contact
- Andreas Dolzmann (for scientific matters)
- Christina Schwarz (for administrative matters)
Schedule
In this Dagstuhl Seminar, we brought together researchers from three different communities that all bring their own perspective on the role of probabilities in programs and models. To facilitate future collaborations, we saw a need to define common terminology. Therefore, we split this seminar into two parts: On the first two days, we surveyed the research areas (see Chapter 3 of the full report) and on the second half, we had in-depth sessions. In the first half, we particularly discussed the following exemplary questions:
- What are probabilistic circuits and why do they allow tractable inference?
- What is probabilistic model checking and what are temporal specifications?
- What are probabilistic programs and how are their semantics defined?
- How does one reason over probabilistic programs on the source-code level?
We also spent time to identify common interests in problems, which led to some hot topics mentioned below. The second half of the seminar featured 30-minute technical talks (see Section 4 of the full report) that provided in-depth discussions on recent research and informal discussions based on the technical talks and the hot topics.
Hot discussion topics. Our discussions led to a list of seven hot topics, summarized below, that were the basis for informal discussions later in the week.
- Unbounded executions in probabilistic programs, their use-cases, analysis techniques, and the downsides.
- Algebraic decision diagrams versus probabilistic circuits and their benefits for reasoning about reachability in graphs.
- The expressiveness and tractability borders between different model types.
- Adequate planning horizons in different scenarios and their influence on the effectiveness of various approaches.
- Inferring symbolic plans and policies via reinforcement learning and with logical constraints, in particular in the context of providing verifiable and explainable controllers.
- The limits of Boolean synthesis in the context of model counting.
- Learning models from data across communities, including perspectives on inference and active automata learning.
- Probabilistic models as distribution transformers and the verification of distributional properties.
In-depth technical sessions. We wanted to highlight the many in-depth discussions that happened mostly 24/7. These discussions were both on the hot topics listed above, as well as very technical, in-depth discussions. We believe that part of the success of this seminar were the various connections that were established on very technical levels. It became clear that the prevalent approaches for very similar problems are vastly different and that there was a common interest to learn about these methodologies.
Challenges. While we are proud of what we achieved, the different backgrounds required a significant effort in order to understand the problems that the different subcommunities find most pressing. As organizers, we would have loved to see time and room to also discuss application areas, but it was hard to find cross-community overlapping interests in those.
Creative Commons BY 4.0
Sebastian Junges, Joost-Pieter Katoen, Scott Sanner, and Guy Van den Broeck
This Dagstuhl Seminar focuses on the cross-fertilization between different research fields by bringing together (a) those working on model-based reasoning (MBR) for stochastic systems, (b) those working on probabilistic programming languages (PPLs), and (c) those working on low-level inference techniques for both MBR and PPLs that could benefit from cross-fertilization given their common technical underpinnings.
On one hand, researchers in MBR subfields have developed tailored languages such as RDDL (planning), Prism (verification), and subsets of probabilistic graphical models (PGMs) for specialized probabilistic inference tasks (belief state tracking, anomaly detection, prediction and forecasting, system fault diagnosis, etc.). While these languages have found successful applications, they are purpose-built for their use cases and their associated inference engines are similarly specialized. On the other hand, PPLs such as WebPPL, Dice, or Anglican offer a flexible and expressive paradigm for specifying and reasoning about highly general stochastic systems that subsume the aforementioned MBR subfields. By borrowing constructs from general programming languages, these PPLs are easy to use and highly general. However, inference in these very general PPLs is highly challenging and hence substantial knowledge is required to achieve the necessary efficiency for practical applications. The holy grail of PPLs would be efficient, highly scalable, and easy to use engines that support expressive languages.
The aim of this Dagstuhl Seminar is to bring experts from PPLs, PGMs, probabilistic model checking and program analysis, and AI planning together in order to discuss recent advances and identify opportunities for cross-fertilization. We aim to:
- Taxonomize existing representations and methods. What is a taxonomy of language representations (e.g., propositional vs. lifted, discrete and/or continuous, recursion, etc.)? What is a taxonomy of inference problems (finite, infinite, nested, indefinite horizon, average or worst-case?) What is a taxonomy of algorithmic methodologies (e.g., optimization, decision diagrams, SAT/SMT, weighted model counting, Monte Carlo tree search, etc.)?
- Identify opportunities for cross-fertilization. These include methodological questions, such as: Which representations and inferential problems exist across fields? Is there a common low-level "assembly" representation of PPLs that could become a shared compilation target by high-level languages? What compile-time or run-time optimizations could be applied in this case? How do we support automatic abstraction? Other opportunities may arise in improving usability, sharing ideas to ease the learning curve for users.
- Distill challenge problems. What are the challenge problems, their requisite representations and inferential constraints that define high impact problems for probabilistic programming languages (e.g., safety and robustness in AI, transportation systems and urban mobility, the renewable energy grids, predictive maintenance)? How can we initiate collaborative research efforts between different communities to tackle these problems?
Sebastian Junges, Joost-Pieter Katoen, Scott Sanner, and Guy Van den Broeck
- S. Akshay (Indian Institute of Technology Bombay - Mumbai, IN) [dblp]
- Suguman Bansal (Georgia Institute of Technology - Atlanta, US) [dblp]
- Kevin Batz (RWTH Aachen, DE)
- Milan Ceska (Brno University of Technology, CZ) [dblp]
- Supratik Chakraborty (Indian Institute of Technology Bombay - Mumbai, IN) [dblp]
- YooJung Choi (Arizona State University - Tempe, US) [dblp]
- Cassio de Campos (TU Eindhoven, NL)
- Luc De Raedt (KU Leuven, BE) [dblp]
- Rayna Dimitrova (CISPA - Saarbrücken, DE) [dblp]
- Poorva Garg (UCLA, US)
- Vibhav Gogate (University of Texas at Dallas - Richardson, US)
- Ichiro Hasuo (National Institute of Informatics - Tokyo, JP) [dblp]
- Holger Hermanns (Universität des Saarlandes - Saarbrücken, DE) [dblp]
- Steven Holtzen (Northeastern University - Boston, US)
- Manfred Jaeger (Aalborg University, DK) [dblp]
- Nils Jansen (Radboud University Nijmegen, NL) [dblp]
- Sebastian Junges (Radboud University Nijmegen, NL) [dblp]
- Amir Kafshdar Goharshady (HKUST - Kowloon, HK)
- Benjamin Kaminski (Universität des Saarlandes - Saarbrücken, DE) [dblp]
- Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
- Samuel Kolb (KU Leuven, BE)
- John Li (Northeastern University - Boston, US)
- Anji Liu (UCLA, US)
- Christoph Matheja (Technical University of Denmark - Lyngby, DK)
- Chih-Hao Luke Ong (Nanyang TU - Singapore, SG) [dblp]
- David Parker (University of Oxford, GB) [dblp]
- Jean-Francois Raskin (UL - Brussels, BE) [dblp]
- Jurriaan Rot (Radboud University Nijmegen, NL) [dblp]
- Bahare Salmani Barzorki (RWTH Aachen, DE)
- Scott Sanner (University of Toronto, CA) [dblp]
- Alexandra Silva (Cornell University - Ithaca, US) [dblp]
- Matthijs Spaan (TU Delft, NL) [dblp]
- Guy Van den Broeck (UCLA, US) [dblp]
- Antonio Vergari (University of Edinburgh, GB)
Classification
- Artificial Intelligence
- Logic in Computer Science
- Programming Languages
Keywords
- Probabilistic Inference
- Probabilistic Programs
- Probabilistic Planning
- Probabilistic Model Checking
- Model Counting
