Dagstuhl Seminar 24361
Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy
( Sep 01 – Sep 06, 2024 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/24361
Organizers
- Nils Jansen (Ruhr-Universität Bochum, DE)
- Mykel Kochenderfer (Stanford University, US)
- Jan Kretinsky (Masaryk University - Brno, CZ)
- Jana Tumova (KTH Royal Institute of Technology - Stockholm, SE)
Contact
- Andreas Dolzmann (for scientific matters)
- Simone Schilke (for administrative matters)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
Introduction
Artificial intelligence (AI) is a disruptive force. With growing applications in fields like healthcare, transportation, game playing, finance, and robotics, 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 of 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. Therefore, it provides ample grounds to address the safety concerns of and provide guarantees in AI systems.
Via a diverse program with ample space for open yet guided discussion, this Dagstuhl Seminar brought together experts from the fields of artificial intelligence, formal methods, and robotics. The predecessor was the Dagstuhl Seminar 18121 Machine Learning and Model Checking Join Forces, on the interaction of AI (specifically machine learning) and FM (specifically model checking), mainly from the theoretical perspective. In contrast, this seminar broadened the scope methodologically, including AI and FM generally, but focused more narrowly on the application of reliable robotics in real-world robotics, which then drives the concrete questions towards increased applicability of combined research in AI and FM.
Formal Methods, AI and Robotics
Formal methods (FM) and AI differ not only in the type of problems they tackle but also in their focus on the desirable properties of the methods. While AI focuses primarily on effectiveness and efficiency, formal methods focus on reliability and safety. Obviously, in both cases, the other properties are not negligible for actual real applications. Consequently, over the last decade, achieving the best of both worlds has become even more important. On the one hand, ML experienced a huge boom accompanied by challenges orthogonal to the tradition, such as provable reliability or explainability; on the other hand, FM was transformed by this process, with AI becoming both an object of FM and a useful technique to be used within FM.
In particular, the problem of controlling complex systems is so fundamental that many approaches have evolved independently in several communities, depending on the particular setting and type of the system, e.g., in artificial intelligence, formal methods, control theory, or robotics. Recently, many of the specifics such as uncertainty, safety-criticality, cyber-physical nature, or complex dynamics (combining continuous and discrete aspects) are present all at once, such as in robots. This rich combination of challenges calls for combining the techniques of the respective disciplines in fundamentally new ways so that real complex systems can be efficiently and reliably controlled and deployed in society.
In addition to the challenges related to integrating AI and formal methods in general, several application-specific challenges arise, reflecting that robots are physical systems: Robot models are highly complex, and often, it is not even possible to derive or use an analytic model (e.g., in contact-rich manipulation). Consequently, the dimensionality and the degree of uncertainty in these systems are very high. These challenges were the inspiration for the topics discussed in this seminar.
Seminar Structure
Tutorials
The first half of the week aimed at creating a mutual theoretical understanding and an interdisciplinary view on the topics of the seminar. To this end, the seminar had five plenary tutorials, each focusing on a different aspect of the subject areas relevant to the seminar. In particular, the following topics were presented:
- Model-Based Reinforcement Learning, by Wendelin Böhmer,
- An Overview of Probabilistic Verification Techniques, by Sebastian Junges,
- Formal Methods & Verification in Robotics & Autonomous Systems Engineering @ Bosch, by Michaela Klauck,
- Robot Learning, by Georgia Chalvatzaki, and,
- Conformal Prediction, by Lars Lindemann.
Working Groups
In the latter half of the week, there was ample time for focused discussions among participants in breakout sessions. These sessions had various aims, such as further increasing interdisciplinary understanding of the relevant concepts, discussing new research ideas, and identifying open problems. The working groups (breakout rooms) consisted of the following topics, from which a subset is elaborated in more detail in Section 4 of the full report:
- Human Models: Modelling Humans Towards AI Decision-Making,
- Models and Programmatic Reinforcement Learning,
- Partially Observable Markov Decision Processes (POMDPs),
- Robust Markov Decision Processes (Robust MDPs),
- Hierarchies of Specifications,
- Runtime Monitoring (with a particular focus on latent verification),
- Reliability,
- Explainability.
Talks
In addition to the tutorials and working groups, many participants presented their lines of work, blue-sky ideas, open problems, and big challenges in dedicated presentation slots. The abstracts can be found in the overview section of the talks.
The seminar provided a platform for early-career researchers among the participants to present their research in so-called spotlight talks throughout the week. In these talks, the participants presented recent work and their general research direction to the seminar audience. Thanks to the spotlights, participants got an impression of the research directions of the other participants.
In addition to the spotlight talks, the seminar participants disseminated open problems, blue-sky ideas, and big challenges. Many of these talks resulted in topics for further discussion.
Creative Commons BY 4.0
Nils Jansen, Mykel Kochenderfer, Jan Kretinsky, Jana Tumova, and Maris Galesloot
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.
Nils Jansen, Mykel Kochenderfer, Jan Kretínský, and Jana Tumova
Please log in to DOOR to see more details.
- Eric Atkinson (Binghamton University, US)
- Joydeep Biswas (University of Texas - Austin, US) [dblp]
- Wendelin Böhmer (TU Delft, NL)
- Jonathan DeCastro (Toyota Research Institute - Cambridge, US) [dblp]
- Clemens Dubslaff (TU Eindhoven, NL)
- Khen Elimelech (Rice University - Houston, US) [dblp]
- Georgios Fainekos (Toyota Motor North America, R&D - Ann Arbor, US) [dblp]
- Maris Galesloot (Radboud University Nijmegen, NL)
- Anna Gautier (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Kush Grover (TU München, DE)
- Sofie Haesaert (TU Eindhoven, NL) [dblp]
- Nick Hawes (University of Oxford, GB) [dblp]
- Nils Jansen (Ruhr-Universität Bochum, DE) [dblp]
- Sebastian Junges (Radboud University Nijmegen, NL) [dblp]
- Ruya Karagulle (University of Michigan - Ann Arbor, US) [dblp]
- Sydney Katz (Stanford University, US)
- Michaela Klauck (Robert Bosch GmbH - Stuttgart, DE) [dblp]
- Mykel Kochenderfer (Stanford University, US) [dblp]
- Johannes Köhler (ETH Zürich, CH)
- Jan Kretinsky (Masaryk University - Brno, CZ) [dblp]
- Hanna Kurniawati (Australian National University - Canberra, AU) [dblp]
- Bruno Lacerda (University of Oxford, GB) [dblp]
- Lars Lindemann (USC - Los Angeles, US) [dblp]
- Sara Magliacane (University of Amsterdam, NL) [dblp]
- Dimitra Panagou (University of Michigan - Ann Arbor, US) [dblp]
- David Parker (University of Oxford, GB) [dblp]
- Karinne Ramirez Amaro (Chalmers University of Technology - Göteborg, SE) [dblp]
- Christian Schilling (Aalborg University, DK) [dblp]
- Philipp Schillinger (Bosch Center for AI - Renningen, DE) [dblp]
- Thiago D. Simão (TU Eindhoven, NL) [dblp]
- Stephen Smith (University of Waterloo, CA) [dblp]
- Matthijs Spaan (TU Delft, NL) [dblp]
- Hazem Torfah (Chalmers University of Technology - Göteborg, SE) [dblp]
- Jana Tumova (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
- Cristian Ioan Vasile (Lehigh University - Bethlehem, US) [dblp]
- Abhinav Verma (Pennsylvania State University - University Park, US) [dblp]
- Esen Yel (Rensselaer Polytechnic Institute, US) [dblp]
Related Seminars
- Dagstuhl Seminar 18121: Machine Learning and Model Checking Join Forces (2018-03-18 - 2018-03-23) (Details)
Classification
- Artificial Intelligence
- Formal Languages and Automata Theory
- Robotics
Keywords
- Formal Verification
- Artificial Intelligence
- Machine Learning
- Autonomous Systems
- Robotics
