Formale Methoden und Maschinelles Lernen

Themenbereich

In diesem Proseminar möchten wir Synergieeffekte zwischen Formalen Methoden und Maschinellem Lernen ergründen.

Das weitläufige Forschungsgebiet der Formalen Methoden ist bestrebt, ihre entwickelten Techniken auf ein formal-mathematisches Fundament zu stellen. Zum Beispiel: Als Teildisziplin beschäftigt sich die Formale Verifikation mit dem Nachweis der Zuverlässigkeit von Systemen. Viele Formale Methoden arbeiten deduktiv, d. h. sie leiten dabei Wissen anhand von Regeln aus einer Faktenbasis her.

Im Gegensatz dazu ist Maschinelles Lernen induktiv: Anhand von vielen Beispielen wird ein komplexes System oder Verhalten approximiert. Dabei finden die gelernten Systeme immer mehr Verbreitung in kritischen Anwendungen und Infrastruktur, aktuell prominentestes Beispiel ist das Autonome Fahren.

• Können wir beweisen, ob ein maschinell gelerntes System zuverlässig ist?
• Können Formale Methoden bei der Erklärbarkeit von maschinell gelernten Systemen helfen?
• Verbessert Maschinelles Lernen die Skalier- und Anwendbarkeit von Formalen Methoden?

Aufgabenstellung

Für das Seminar werden von jedem/jeder Teilnehmer/in für eine erfolgreiche Teilnahme folgende Leistungen erwartet:

• Selbständiges Erarbeiten der Inhalte des vorzustellenden Ansatzes (meist auf Basis eines Papiers im Umfang von etwa 20 Seiten). In regelmäßigen Treffen mit einem/r betreuenden Mitarbeiter/in erhalten Sie hierbei die nötige Unterstützung.
• Auswahl und Gliederung der Inhalte die in Ihrem Seminarbeitrag präsentiert werden sollen.
• Kurze Vorstellung Ihrer Gliederung im Plenum.
• Entscheidung, wie Sie die Inhalte präsentieren wollen.
• Erstellung der Folien für die Präsentation und gegebenfalls weiterer Materialien.
• 20-minütiger Hauptvortrag im Plenum (gefolgt von einer etwa 10-minütigen Diskussion).
• Nach dem Vortrag: Verfassen einer etwa zehnseitigen Ausarbeitung, die die wesentlichen Inhalte des Ansatzes und Ihres Vortrags zusammenfassend darstellt.

Folien

Folien der Auftaktveranstaltung

Vortragsthemen

1. Grundlagen von (tiefen) Neuronalen Netzen — Jonas Klamroth
   Schmidhuber: Deep learning in neural networks: An overview
2. Angriffe auf Machine Learning — Jonas Schiffl
   SoK: Towards the Science of Security and Privacy in Machine Learning
3. SMT-Solver für Machine Learning — Carsten Sinz
   Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In CAV, pages 97–117, 2017.
4. Sicherheitseigenschaften von Neuronalen Netzen — Marko Kleine Büning
   Survey: Automated Verification of Neural Networks: Advances, Challenges and Perspectives
5. Einfluss von Implementierungsfehlern im Maschinellen Lernen — Marko Kleine Büning
   
6. Instanzspezifische Algorithmenkonfiguration im SAT Solving — Markus Iser
   Structure Features for SAT Instance Classification" (Ansótegui et al., 2017)
7. Automatisches Empfehlen von Beweismethoden für Beginner in Isabelle/HOL — Michael Kirsten
   PaMpeR: proof method recommendation system for Isabelle/HOL. Yutaka Nagashima, Yilun He. ASE 2018.
8. Prädiktion von SMT Solver Performance — Alexander Weigl
   Prediction SMT Solver Performance for Software Verification; Healy, Monahan, Power (F-IDE 2016)