TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 18121

Machine Learning and Model Checking Join Forces

( Mar 18 – Mar 23, 2018 )


Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/18121

Organizers

Contact


Motivation

Machine learning. A prominent field related to artificial intelligence (AI) is the one of machine learning (ML). Very broadly, machine learning describes algorithms that independently learn from data that is observed in possibly unknown environments. Applications are - only to mention a few - given in autonomous systems, computer vision, and video games. In the real-world, these previously not well-defined environments carry the risk of taking safety-critical action along the way of obtaining optimal strategies.

Model checking. With a rapidly growing number of computer-controlled systems, the need to ensure that systems are correct is present everywhere. Formal verification is a research area that aims at providing guarantees on system behavior. In particular, model checking is a technique that proves or disproves properties of a system by rigorous exploration of the state space of a system model. Naturally, such verification techniques necessitate well-defined models of a real-world system.

This Dagstuhl Seminar aims at bringing together researchers working in the fields of machine learning and model checking. The spirit of the seminar shall be "Machine Learning and Model Checking Join Forces". We believe that in-depth understanding of each others problems and solutions will help to identify new research topics on the one hand, and to help with current problems on the other hand. Growing application areas for machine learning, such as autonomous driving, require the exclusion or likely avoidance of unsafe behaviors. An important question is then, how confidence in system behaviors obtained from machine learning can be transferred to formal verification. Vice versa, industrial usage of model checking still suffers from scalability issues for large applications. Leveraging the capabilities of machine learning to assess large data sets will help to enable the verification for more realistic systems. We emphasize the following directions for discussions:

  • Safety-related issues for machine learning
  • Explainability in AI and in model checking
  • Scalability and applicability of formal verification

We identify the following concrete research questions:

  • What does formal verification actually mean for system models that are not well-defined and subject to change? What kind of guarantees can or should be given?
  • How can models and guarantees be robustified against further samples/observations?
  • Many validity problems in machine learning point to the opportunity of employing human feed-back. How can such feedback be incorporated in a verification scheme?
  • Can we use formal verification to train machine learning by identifying corner cases in the form of counterexamples?
  • Towards explainable AI, can verification of probabilistic programs improve the understanding of verification and machine learning results for humans?
  • How can machine learning help to improve scalability of verification techniques?
  • How can machine learning be employed in verification for hard guarantees?
  • Can machine-learning classifiers learn abstractions appropriate for verification analysis?
  • Can machine learning help to interpret verification results? Can error traces or synthesized controllers be mined so that they are presentable in an understandable way?
Copyright Nils Jansen, Joost-Pieter Katoen, Pushmeet Kohli, and Jan Kretinsky

Summary

This Dagstuhl Seminar aimed at bringing together researchers working in the fields of machine learning and model checking. Growing application areas for machine learning, such as autonomous driving, require the exclusion or likely avoidance of unsafe behaviors. An important question is then, how confidence in system behaviors obtained from machine learning can be transferred to formal verification. Vice versa, industrial usage of model checking still suffers from scalability issues for large applications. Leveraging the capabilities of machine learning to assess large data sets will help to enable the verification for more realistic systems.

Based on the concrete discussions and inputs from all the participants, we identified the following topics as great challenges to the combination of the fields of machine learning and model checking.

  • Safety Verification of Deep Neural Networks
  • Formal Program Synthesis and Analysis using Machine Learning
  • Representation of Strategies and Controllers
  • Explainable Artificial Intelligence
  • Challenges for Machine Learning in Motion Planning
  • Guarantees on Reinforcement Learning in Verification
  • Social and Legal Issues in Artificial Intelligence
  • Exploiting Weaknesses in Reinforcement Learning
Copyright Nils Jansen, Joost-Pieter Katoen, Pushmeet Kohli, and Jan Kretinsky

Participants
  • Alessandro Abate (University of Oxford, GB) [dblp]
  • Erika Abraham (RWTH Aachen, DE) [dblp]
  • Ezio Bartocci (TU Wien, AT) [dblp]
  • Roderick Bloem (TU Graz, AT) [dblp]
  • Luca Bortolussi (University of Trieste, IT) [dblp]
  • Tomáš Brázdil (Masaryk University - Brno, CZ) [dblp]
  • Marc Brockschmidt (Microsoft Research UK - Cambridge, GB) [dblp]
  • Rudy Bunel (University of Oxford, GB) [dblp]
  • Michael Carbin (MIT - Cambridge, US) [dblp]
  • Rayna Dimitrova (University of Leicester, GB) [dblp]
  • Krishnamurthy Dvijotham (Google UK - London, GB) [dblp]
  • Rüdiger Ehlers (Universität Bremen, DE) [dblp]
  • Andreas Berre Eriksen (Aalborg University, DK) [dblp]
  • Radu Grosu (TU Wien, AT) [dblp]
  • Arnd Hartmanns (University of Twente, NL) [dblp]
  • Laura Humphrey (AFRL - Wright Patterson, US) [dblp]
  • Manfred Jaeger (Aalborg University, DK) [dblp]
  • Nils Jansen (Radboud University Nijmegen, NL) [dblp]
  • Sebastian Junges (RWTH Aachen, DE) [dblp]
  • Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
  • Pushmeet Kohli (Google DeepMind - London, GB) [dblp]
  • Jan Kretinsky (TU München, DE) [dblp]
  • Kim Guldstrand Larsen (Aalborg University, DK) [dblp]
  • Alexis Linard (Radboud University Nijmegen, NL) [dblp]
  • Tobias Meggendorfer (TU München, DE) [dblp]
  • Daniel Neider (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Guillermo A. Pérez (Free University of Brussels, BE) [dblp]
  • Ruzica Piskac (Yale University - New Haven, US) [dblp]
  • Hasan Poonawala (Univ. of Texas at Austin, US) [dblp]
  • Pavithra Prabhakar (Kansas State University - Manhattan, US) [dblp]
  • Jean-Francois Raskin (Free University of Brussels, BE) [dblp]
  • Guido Sanguinetti (University of Edinburgh, GB) [dblp]
  • Daniel Selsam (Stanford University, US) [dblp]
  • Sanjit A. Seshia (University of California - Berkeley, US) [dblp]
  • Armando Solar-Lezama (MIT - Cambridge, US) [dblp]
  • Ufuk Topcu (University of Texas - Austin, US) [dblp]
  • Jana Tumova (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
  • Jonathan Uesato (Google DeepMind - London, GB) [dblp]
  • Frits Vaandrager (Radboud University Nijmegen, NL) [dblp]
  • Min Wen (University of Pennsylvania - Philadelphia, US) [dblp]
  • Leonore Winterer (Universität Freiburg, DE) [dblp]

Classification
  • artificial intelligence / robotics
  • semantics / formal methods
  • verification / logic

Keywords
  • Machine learning
  • Artificial Intelligence
  • Formal Methods
  • Formal Verification
  • Logics
  • Cyber-physical Systems
  • Quantitative Verification
  • Model Checking
  • Safety-critical Systems