Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Proseminar im Sommersemester 2019

Formale Methoden und Maschinelles Lernen

Veranstaltungstyp: Proseminar
Zielgruppe: Bachelor Informatik
Umfang: 2 SWS / 3 ECTS
Termine: 25.04.2019, 13:00 — 14:00 Uhr in 50.34R236, Auftaktveranstaltung
06.06.2019, 15:45 — 17:15 Uhr in Raum 236 (50.34), Zwischenvorträge
15.07.2019, 09:00 — 13:00 Uhr in Raum 010 (50.34), Hauptvorträge
30.09.2019, Abgabe der Ausarbeitung
Veranstaltungsnr.: 2400070
Lehrstühle: Anwendungsorientierte Formale Verifikation
Zuverlässige Softwaresysteme in der Automobilindustrie
Dozenten:

Alexander Weigl [Organisation]
Prof. B. Beckert
Prof. C. Sinz
Marko Kleine Büning
Mihai Herda
Markus Iser
Michael Kirsten
Jonas Klamroth
Jonas Schiffl
Dr. Mattias Ulbrich

Anmeldung: Anmeldungen im WiWi-Portal
Platzvergabe nach Anmeldereihenfolge
Platzvergabe: Reihenfolge nach Eingang der Anmeldung
Alle Plätze vergeben (15.10.2018)
Neue Anmeldungen kommen auf die Warteliste.

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)