Machine Learning and Model Checking Join Forces

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