FRAPPANT’s objective is to enable predictable probabilistic programming by developing unique, advanced formal verification techniques.
ERC Advanced Grant 2017 (787914). Project duration: 1.11.2018 to 31.10.2024. See also the CORDIS fact sheet on FRAPPANT and the RWTH press release.
Researchers. Joost-Pieter Katoen, Kevin Batz, Lutz Klinkenberg, Bahare Salmani, Philipp Schroer. Former members: Jushua Moermann, Mingshuai Chen, Benjamin Kaminski, Marcin Szymczak.
Abstract
Probabilistic programs describe recipes on how to infer statistical conclusions about data from a complex mixture of uncertain data and real-world observations. They can represent probabilistic graphical models far beyond the capabilities of Bayesian networks and are expected to have a major impact on machine intelligence.
Probabilistic programs are ubiquitous. They steer autonomous robots and self-driving cars, are key to describe security mechanisms, naturally code up randomised algorithms for solving NP-hard problems, and are rapidly encroaching AI. Probabilistic programming aims to make probabilistic modeling and machine learning accessible to the programmer.
Probabilistic programs, though typically relatively small in size, are hard to grasp, let alone automatically checkable. Are they doing the right thing? What’s their precision? These questions are notoriously hard — even the most elementary question “does a program halt with probability one?” is “more undecidable” than the halting problem — and can (if at all) be answered with statistical evidence only. Bugs thus easily occur. Hard guarantees are called for. The objective of this project is to enable predictable probabilistic programming. We do so by developing formal verification techniques.
Whereas program correctness is pivotal in computer science, the formal verification of probabilistic programs is in its infancy. The project aims to fill this barren landscape by developing program analysis techniques, leveraging model checking, deductive verification, and static analysis. Challenging problems such as checking program equivalence, loop-invariant and parameter synthesis, program repair, program robustness and exact inference using weakest precondition reasoning will be tackled. The techniques will be evaluated in the context of probabilistic graphical models, randomised algorithms, and autonomous robots.
FRAPPANT will spearhead formally verifiable probabilistic programming.
Recent Research Highlights
To give an overview of our work, each of our current researchers presents highlights one of their recent publications.
Kevin Batz: Probabilistic program verification via inductive synthesis of inductive invariants
Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We have developed a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generating inductive invariants on source-code level. Our implementation finds invariants for (in)finite-state programs, can beat state-of-the-art probabilistic model checkers, and is competitive with modern tools dedicated to invariant synthesis and expected runtime reasoning.
Bahare Salmani: Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks
As a FRAPPANT member, I work on Bayesian Networks (BNs) and how they relate to probabilistic model checking. I’ve focused my research on probabilistic (and symbolic) inference, sensitivity analysis, and parameter tuning on BNs. Our latest paper entitled “Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks” has been recently accepted for presentation at IJCAI 2023 (the 32nd Int. Joint Conf. on Artificial Intelligence) in Macao. Out of 4566 full-paper submissions, about 15% have been accepted. The paper gives an algorithm for estimating the sensitivity of a given fully-specified Bayesian network to small perturbations in the values of local conditional probabilities.
Philipp Schroer: Building an Infrastructure for Probabilistic Program Verification
We are developing Caesar, a deductive verifier for probabilistic programs. It is based on our verification infrastructure for probabilistic programs, similar to a probabilistic version of Boogie. Our work includes an intermediate verification language called HeyVL and a real-valued logic called HeyLo. This allows us to generate verification conditions that prove a program’s correctness. Our focus is on measuring properties like expected outcomes and termination probabilities, so we use a real-valued approach instead of the usual Boolean logic. Our IVL adapts standard verification elements to handle quantitative aspects and uses weakest preexpectation-style semantics to generate verification conditions. Our SMT-based implementation Caesar enables us to automatically verify a wide range of benchmarks.
Caesar has a website where you can download the tool and find its documentation, including a tutorial-style guide. It is developed as an open-source project on Github. A paper on HeyVL and Caesar was published at OOPSLA 2023 and there’s an extended version available on arxiv.
Thesis Projects, Lectures, and Seminars
If you are interested in working on this project as a thesis or Hiwi student, contact one of our researchers on the project. We always have interesting topics available related to this project.
We also provide a recurring lecture series on probabilistic programs. For example, check out the WS 2022/23 lecture page. Furthermore, our seminars regularly deal with topics related to FRAPPANT. Head over to our teaching page for more information.
List of Publications Related to FRAPPANT
| 2024 | |
|---|---|
[bibtex]
[issue]
|
Lutz Klinkenberg, , , , Joost-Pieter Katoen. Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions, Proceedings of the ACM on programming languages 8 (OOPSLA1), ACM, 2024. |
[bibtex]
[issue]
|
Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs, Proceedings of the ACM on programming languages 8, pages 93, ACM, 2024. |
| 2023 | |
|
[bibtex]
[issue]
|
Philipp Schroer, Kevin Batz, , Joost-Pieter Katoen, . A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version), [1]-48, 2023. https://arxiv.org/abs/2309.07781 |
|
[bibtex]
[issue]
|
Philipp Schroer, Kevin Batz, , Joost-Pieter Katoen, . A Deductive Verification Infrastructure for Probabilistic Programs, Proceedings of the ACM on programming languages 7 (OOPSLA2), pages 294, ACM, 2023. |
|
[bibtex]
[issue]
|
Tobias Winkler, Joost-Pieter Katoen. On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata, 38. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023), IEEE, 2023. |
|
[bibtex]
[issue]
|
Tobias Winkler, Joost-Pieter Katoen. Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 391-409, Springer, 2023. |
|
[bibtex]
[issue]
|
Roman Andriushchenko, Alexander Nikolai Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Filip Macák. Search and Explore: Symbiotic Policy Synthesis in POMDPs, 35. International Conference on Computer-Aided Verification (CAV 2023), Volume 13966 of LNCS, 113-135, Springer, 2023. |
|
[bibtex]
[issue]
|
Kevin Batz, Mingshuai Chen, Sebastian Junges, , Joost-Pieter Katoen, . Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 410-429, Springer, 2023. |
|
[bibtex]
[issue]
|
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 2023. |
| Show all | |