TU Dresden
A joint project with Uni Leipzig DE EN

Explaining Composite AI: From Formal Analysis to Overall Understanding

Mentored by Christel Baier & Markus Krötzsch
at Faculty of Computer Science, TU Dresden

Composite AI systems are easier built than understood. Already today, one can use many existing components that are based on different (and not directly incompatible) AI approaches, and combine them through hand-coded interfaces. This might allow us to solve challenging problems, yet it is also hard to trust such a mash-up of distinct components. The goal of this research topic is to analyze such systems based on formal methods (originally developed for tasks like software verification) and to use knowledge-based methods to recover understandable explanations from the results of this analysis.

To accomplish this, the project will leverage methods from formal methods to analyze and reason about composite systems that include both classical components and AI-based systems. In particular, we will consider methods for finding explications and certificates that have been developed in the formal methods community, and study how they can be applied in a compositional setting. Questions that we will aim to answer include:

  • How can the transformation from high-level system description to low-level formal methods abstraction be reversed to recover understandable explanations?
  • How can we find "decomposable" explanations, i.e., explanations that tell us something about the individual components?
  • How large is the influence of individual components on the outcome?
Moreover, if machine learning is involved, we will study how explanations of the composite system can be used to guide the learning, and how certificates for the compositional system could be defined.

Work Environment

You will work in the creative environment of the research groups of Christel Baier and Markus Krötzsch, which are located in close vicinity, giving you direct access to a number of experienced reserchers in both formal methods and knowledge-based systems. You are also part of the International Center of Computational Logic of TU Dresden. All your research-related needs in terms of hardware, travel, or connection to relevant communities can be provided for by your group(s).


To conduct this research, you should hold a very good university degree (MSc or equivalent) in computer science, mathematics or related disciplines. The position requires a solid foundational training, preferrably in a university program that focuses on methods and principles more than on specific applications or technologies.

Research involves the lively exchange with others and the work in teams, but also phases of concentrated self-directed work on own ideas and new solutions. Enjoying both kinds of activity is helpful.