Modul Spezielle Kapitel KI, Informatik (Master) (SPO 8)

Diese Vorlesung befasst sich mit einem Teilgebiet der Künstlichen Intelligenz, Explainable AI (XAI). XAI-Methoden erfüllen eine kritische Funktion in der modernen KI-Landschaft, indem sie die Brücke zwischen menschlichen Nutzern und komplexen KI-Systemen schlagen.

Nach der Teilnahme an der Vorlesung sind die Studierenden in der Lage, die vielfältigen Ziele von XAI zu beschreiben und mit der korrekten XAI-Terminologie zahlreiche Methoden aus dem Bereich der erklärbaren künstlichen Intelligenz einzuordnen und zu bewerten. Weiterhin sind Studierende in der Lage für dedizierte XAI-Methoden die zugrundeliegenden Ideen, Architekturen und Implikationen zu bewerten sowie Fachliteratur wie aktuelle Publikationen zu verstehen und Teilaspekte herauszustellen. Auch sind die Studierenden in der Lage durch praktische Übungen Methoden anzuwenden und Libraries einzusetzen.

Inhaltlich werden in dieser Vorlesung folgende Themen abgedeckt. Dabei werden Methoden mit unterschiedlichem (i) Scope (local vs. global), (ii) Result (z.B. feature relevance, surrogate models), (iii) Functioning (z.B. perturbations, examples), (iv) Format (z.B. textual, visual) und (v) Stage (post-hoc vs. ante-hoc) abgedeckt:

-              Motivation und Ziele von XAI

-              XAI-Terminologie und XAI Taxonomie

-              Methoden aus dem Bereich der Feature Importance Explanations (u.a. feature attribution vs. feature selection)

-              Methoden aus dem Bereich Removal-based Explanations (z.B. LIME, RISE)

-              Shapley Values (und SHAP)

-              Methoden aus dem Bereich Concept-based Explanations (z.B. Concept Bottleneck Models)

-              Methoden zur Interpretation neuronaler Netze (z.B. Attention-basierte Methoden)

-              Potentiellen Gefahren von XAI-Methoden etwa bezüglich "Fairwashing" und "Manipulation".

Am Ende der Vorlesung wird mittels einer mündlichen Prüfung überprüft, inwieweit die Studierenden die grundlegenden XAI-Konzepte verstanden haben sowie aktuelle Forschungsergebnisse bewerten können. Das Beantworten der Fragen erfordert sowohl die gelernte Terminologie richtig zu gebrauchen, als auch unterschiedliche Methoden analysieren bzw. teilweise auch evaluieren zu können.

Neben den durch Gruppenarbeit nachvollzogenen und durch Kurzpräsentationen vorgestellten einzelnen Methoden, haben Studierende zusätzlich die Möglichkeit mit einer freiwilligen, größeren Gruppenpräsentation eines Spezialthemas zu demonstrieren, dass sie einzelne Themen detailliert bewerten und erklären können. Eine Präsentation, die durch fundierte Analyse und verständliche Darstellung überzeugt, führt zu einer Verbesserung der Prüfungsnote um einen Notenschritt.

• Vorlesungsfolien
• Molnar, C. (2024). Interpretable Machine Learning: A Guide for Making Black Box Models Explainable (2nd ed.). christophm.github.io/interpretable-ml-book/

SAT-Solving ist eines der wichtigsten allgemeinen Verfahren zur Lösung schwerer (oft NP-vollständiger) kombinatorischer Probleme. Diese treten in der Praxis in einer Vielzahl von Anwendungen auf, z.B. hier:

• Planungs- und Scheduling-Probleme in Lieferketten
• Konfiguration komplexer, variantenreicher Produkte, z.B. PKWs, LKWs, Flugzeuge
• Prüfung (Verifikation) von Hardware- und Software
• Erstellung von Spielplänen, z.B. in der Bundesliga

Dieses Modul vermittelt Studierenden die theoretischen und schwerpunktmäßig praktischen Aspekte des SAT-Solvings. Behandelt werden:

• Grundlagen, historische Entwicklung
• Codierungen, z.B. cardinality constraints
• Phasenübergänge bei Zufallsproblemen
• Lokale Suche (GSAT, WalkSAT, ..., ProbSAT)
• Resolution, Davis-Putnam-Algorithmus, DPLL-Algorithmus, Look-Ahead-Algorithmus
• Effiziente Implementierungen, Datenstrukturen
• Heuristiken im DPLL-Algorithmus
• CDCL-Algorithmus, Klausellernen, Implikationsgraphen
• Restarts und Heuristiken im CDCL-Algorithmus
• Preprocessing, Inprocessing
• Generierung von Beweisen und deren Prüfung
• Paralleles SAT-Solving (Guiding Paths, Portfolios, Cube-and-Conquer)
• Fortgeschrittene Anwendungen: Bounded Model Checking, Planen, Satisfiability-Modulo-theories

Auch die Einbindung von industriellen Anwendern ist vorgesehen.

In dieser Übung werden Verfahren der Vorlesung Practical SAT Solving anhand von Fragestellungen aus der Praxis erprobt und SAT-Solver zur Lösung von kombinatorischen Problemen eingesetzt.