Modul Spezielle Kapitel Maschinelles Lernen, Informatik (Master) (SPO 7)

Diese Vorlesung vermittelt das Grundwissen über Codes und Codierungen und die gängigen Algorithmen aus dem Gebiet der Quellen-, Kanal- und Leitungscodierung. Im Einzelnen werden Themen aus den folgenden Bereichen behandelt: Informations- und Codierungstheorie, Datenkompression, Fehler­erkennende und -korrigierende Codes, Grenzen der Daten­übertragung.

• PowerPoint-Folien
• Tafelmitschrift
• Übungsblätter

Vorlesungsteilnahme

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, um Vertrauen, Transparenz, Fairness und regulatorische Konformität zu gewährleisten. Diese Vorlesung vermittelt das Grundwissen über Explainable AI (XAI). Wichtig dabei ist, dass XAI hilft, die Black-Box-Natur von komplexen KI-Modellen aufzubrechen, indem es erklärt, wie Entscheidungen zustande kommen. Die Ziele von XAI sind dabei vielfältig: neben dem Fördern von Vertrauen und Akzeptanz bei den Endnutzern können XAI Methoden auch dazu beitragen ein besseres Verständnis der Entscheidungsprozesse von KI-Modellen zu erlangen, was zur Fehlererkennung und Modellverbesserung genutzt werden kann. 

Thematisch werden in dieser Vorlesung zahlreiche XAI Methoden abgedeckt und verschiedenste Aspekte von XAI Methoden betrachtet, unter anderm (i) Scope (local vs. global), (ii) Results (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). Zusätzlich werden auch die potentiellen Gefahren von XAI Methoden diskutiert etwa bezüglich "Fairwashing" und "Manipulation".

• Vorlesungsfolien
• Molnar, C. (2022). 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.:

• 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 soll Studierenden die theoretischen und schwerpunktmäßig praktischen Aspekte des SAT-Solving vermitteln. Behandelt werden:

1. Grundlagen, historische Entwicklung
2. Codierungen, z.B. cardinality constraints
3. Phasenübergänge bei Zufallsproblemen
4. Lokale Suche (GSAT, WalkSAT, ..., ProbSAT)
5. Resolution, Davis-Putnam-Algorithmus, DPLL-Algorithmus, Look-Ahead-Algorithmus
6. Effiziente Implementierungen, Datenstrukturen
7. Heuristiken im DPLL-Algorithmus
8. CDCL-Algorithmus, Klausellernen, Implikationsgraphen
9. Restarts und Heuristiken im CDCL-Algorithmus
10. Preprocessing, Inprocessing
11. Generierung von Beweisen und deren Prüfung
12. Paralleles SAT Solving (Guiding Paths, Portfolios, Cube-and-Conquer)
13. Fortgeschrittene Anwendungen: Bounded Model Checking, Planen, satisfiability-modulo-theories

Auch die Einbindung von industriellen Anwendern (z.B. von Mercedes-Benz) 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.