AI is a disruptive force. With growing applications in fields like healthcare, transportation, game playing, finance, or robotics in general, AI systems and methods are entering our everyday lives. Such tight interaction with AI requires serious safety, correctness, and reliability considerations. Recently, the field of safety in AI has triggered a vast amount of research.

The area of formal methods (FM) offers structured and rigorous ways to reason about the correctness of a system. Techniques range from model learning, over testing to formal verification. As an example for the application of verification in AI, solving techniques like SAT or SMT solving help to assess the robustness of neural networks. Model checking is a prominent verification technique that proves the system's correctness with respect to formal specifications.

In 2018, the time was right to bring the two communities of machine learning and formal methods together and let people discover common interests and problems. This was the aim of the Dagstuhl Seminar "Machine Learning and Model Checking Join Forces" (18121), topically a predecessor of this seminar. Now, the time is right to take the next step.

From a vast number of funded research projects and publications, it is clear that what is actually missing is a practical stance toward reliable autonomy. Building upon various collaborations and results stemming from the former seminar, we take a broader stance on AI and FM and invite key players in robotics to this Dagstuhl Seminar, in addition to a broad selection of AI and FM researchers. In particular, most of the invitees are not restricted to one research community but usually publish across several of these areas.

Via a diverse program with ample space for open yet guided discussion, we aim to address a number of key challenges that range across all fields, for instance

• specific properties of real-world problems,
• guarantees on reliability of AI systems and AI methods,
• specifications for the behavior of AI systems, and
• the form or representation of, for instance, controllers of an AI system.

Creative Commons BY 4.0

Nils Jansen, Mykel Kochenderfer, Jan Kretínský, and Jana Tumova