Vorlesungsbegleitendes Forschungspraktikum
im Sommersemester 2023

Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich, Dr. Michael Kirsten

Typ:	Praktikum
Zielgruppe:	Master Informatik
Umfang:	5 Leistungspunkte (3 Praktikum + 2 Schlüsselqualifikation)
Ort:	n.V.
Veranstaltungs-Nr.:	2400281

Zur Seite der Vorlesung

Inhalt

In diesem Semester bieten wir neben der Vorlesung ein optionales begleitendes Forschungspraktikum im Umfang von insgesamt fünf Leistpungspunkten (LP) (davon zwei Schlüsselqualifikation (SQ)) an. Hierbei handelt es sich um ein Projektpraktikum, in dem über das ganze Semester an einem Thema gearbeitet wird (und nicht an verschiedenen Aufgabenblättern). Die Bearbeitung aktueller Forschungsthemen erfordert hierbei ein größeres Maß an Eigeninitiative als dies bei im Vorhinein festgelegten Praktika der Fall ist. Die Fortschritte werden dabei regelmäßig mit einem bzw. einer betreuenden Mitarbeitenden der Forschungsgruppe diskutiert.

Zu Beginn der Vorlesung werden Themen vorgestellt, für die sich die Teilnehmer:innen innerhalb der ersten Woche bewerben können (die Plätze sind begrenzt!). Das Forschungspraktikum basiert thematisch auf in der gekoppelten Vorlesung vermittelten Inhalten. Die praktische Forschungsaktivität ist Teil einer (größeren) Forschungsaktivität der Forschungsgruppe und trägt zu deren Erfolg bei.

Beispiele für solche Forschungsaktivitäten sind etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation (u.ä.). Am Ende des Semesters werden die Ergebnisse des Forschungspraktikums auf drei bis fünf Seiten dokumentiert, sowie zum letzten Vorlesungstermin im Rahmen eines Kolloquiums in jeweils etwa 10 bis 15 Minuten präsentiert und in einer anschließenden Fragerunde diskutiert.

Qualifikationsziele

• Einen Forschungsansatz und die eigene Forschungs(teil-)aufgabe verstehen, begründen, bewerten und einordnen können
• Aus der Aufgabenbeschreibung konkrete Arbeitsschritte entwickeln können
• In dem Forschungsbereich des Projekts wissenschaftlich arbeiten können
• Die für das Projekt relevanten inhaltlichen Grundlagen kennen, einsetzen und die Relevanz für die Fragestellung bewerten können
• Forschungsergebnisse dokumentieren, zusammenfassen und präsentieren, sowie diskutieren können

Methodische Begleitveranstaltungen

Neben der Forschungsarbeit umfasst das Praktikum auch die folgenden mit der Projektarbeit verzahnten methodischen Veranstaltungen im Rahmen von zwei Leistungspunkten (LP), die im Rahmen des Forschungspraktikums als Schlüsselqualifikationsleistungen zu besuchen sind:

• Literaturrechereche und Zitieren (2,0 Stunden)
• Projektmanagementworkshop (7,0 Stunden)
• Präsentationsworkshop (8,0 Stunden)
• Erkenntnistheorie (1,5 Stunden)
• Wissenschaftstheorie (1,5 Stunden)
• Workshop zum Aufstellen einer Forschungsfrage (3,0 Stunden)
• Schreiben von Forschungsanträgen (1,5 Stunden)
• Experimentaldesign (1,5 Stunden)

Die Workshops zu Projektmanagement und Präsentationen finden in Kooperation mit dem House of Competence (HoC) statt. Alle Veranstaltungen sind gezielt auf Forschungsprojekte im Bereich der Informatik ausgerichtet. Die Termine der Veranstaltungen werden zu Vorlesungsbeginn bekanntgegeben.

Themen

Die Themen werden zu Beginn der Vorlesung vorgestellt. Zudem sind wir offen für Themenvorschläge, die im Zusammenhang zur Vorlesung bzw. zur Forschung unserer Forschungsgruppe stehen. Beispiele hierfür sind Forschungsaktivitäten wie etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation ausgewählter formaler Methoden (u.ä.). An dieser Stelle werden wir vor Beginn der Vorlesung eine Auswahl geplanter Themen auflisten. Bei Fragen hierzu können Sie sich bereits im Vorfeld bei den genannten Ansprechpersonen melden. Gern gesehen sind auch Initiativanfragen zu Themengebieten unserer Forschungsgruppe.

• Modellierung und Verifikation eines Smart Contracts für ein Casino-Szenario

  Smart Contracts sind Programme, die bestimmte Funktionalitäten in einem dezentralen Netzwerk zur Verfügung stellen. Da sie oft den Zugang zu Währung oder anderen Ressourcen verwalten, ist es sehr wichtig, schon vor der Veröffentlichung des Programms zu überprüfen, ob es sich immer korrekt verhält. Zu diesem Zweck kann es sinnvoll sein, eine Smart-Contract-Anwendung auf einer abstrakteren Ebene zu modellieren, um dann beispielsweise Safety- und Livenesseigenschaften spezifizieren und beweisen zu können.

  In diesem Projekt soll ein bereits existierender Smart Contract als abstrakte Maschine in Event-B modelliert werden. Dies beinhaltet eine Einarbeitung in Event-B und das Werkzeug Rodin. Weiterhin soll versucht werden, Safety- und Livenesseigenschaften des entstandenen Modells zu spezifizieren und verifizieren.

  Betreuung: Jonas Schiffl

• Automatisches Finden von Wahlmanipulationen mittels Bounded Model Checking

  Die strategische Manipulation eines Wahlverfahrens ist die Abgabe einer Stimme, die von der eigenen Präferenz abweicht, mit dem Ziel, das Wahlergebnis stärker (als die "wirklich" präferierte Stimme) hin zur eigenen Präferenz zu beeinflussen. Es gibt ein grundsätzliches Ergebnis, dass jedes nicht-diktatorische Wahlverfahren mit mindestens drei Alternativen für solche Manipulationen anfällig ist. Manche Wahlverfahren lassen sich jedoch einfacher manipulieren als andere. Traditionell wird diese Fragestellung komplexitätstheoretisch untersucht, in neueren Arbeiten aber auch konkret quantifiziert.

  Das Projekt beinhaltet die Einarbeitung in obige Fragestellung, die Formalisierung einer solchen Quantifizierung für einfache Scoring-Wahlverfahren (z. B. relative Mehrheitswahl, Borda, ...) und die Entwicklung und Evaluation einfacher Experimente für den Bounded Model Checker CBMC, um solche Manipulationen für ein Wahlverfahren automatisch zu generieren und bewerten zu können.

  Betreuung: Michael Kirsten

• Splitting Oracles für die Verifikation Neuronaler Netze

  Die Verifikation neuronaler Netze mit stückweise linearen Aktivierungsfunktionen ist NP-schwer. Zurzeit bauen die meisten Solver auf einer Mischung von Überapproximation und Branch-and-Bound-Techniken für die Eingabevariablen oder den Zustand der Aktivierungsfunktionen auf.

  In diesem Projekt soll untersucht werden, ob sich der Verifikationsprozess beschleunigen lässt, wenn man zuerst ein Netzwerk, das sich ähnlich zum ursprünglichen Netzwerk verhält – aber kleiner (und damit schneller zu verifizieren) ist – verifiziert. Dabei sollen die Splits des Solvers für dieses einfachere Netz aufgezeichnet werden. Die Hoffnung ist, dass diese Splits schon ausreichen, die gewünschte Eigenschaft auch auf dem größeren ursprünglichen Netz zu zeigen.

  Das Projekt beinhaltet die Einarbeitung in das Themengebiet der Verifikation neuronaler Netze, sowie die Benutzung und Erweiterung eines bestehenden Solvers zur Implementierung der Projektidee und die anschließende Evaluation.

  Betreuung: Philipp Kern

• Large Language Models für die Synthese von JML-Spezifikationen und Schleifeninvarianten

  Eine wichtige Herausforderung bei der Anwendung deduktiver Beweismethoden für die Programmverifikation (wie bspw. in KeY) ist die geeignete Spezifizierung von Untermethoden sowie die Konstruktion von Schleifeninvarianten. Dies passiert aktuell oftmals manuell: Ein:e Entwickler:in muss auf Basis der Top-Level Spezifikation geeignete Verträge für Untermethoden sowie Invarianten für Schleifen spezifizieren und anschließend beweisen. Erste Experimente mit ChatGPT legen nahe, dass der Trainingskorpus von GPT-3.5 ausreichend JML-annotierten Java Code enthalten hat um GPT (als Beispiel für Large Language Models im allgemeinen) für die Synthese von JML zu verwenden.

  In diesem Projekt soll eine Schnittstelle, die GPT mit KeY interagieren lässt, prototypisch implementiert und evaluiert werden. Ziel ist es die Fähigkeiten und Grenzen eines "naiven" Ansatzes zu evaluieren: Wie weit kommt man mit einer derartigen Anbindung ohne ein spezialisiertes Modell? Auf welchen Programmen funktioniert es und wo nicht? Hier gilt es insbesondere geeignete Benchmarks zu finden oder zu konstruieren, die sehr wahrscheinlich nicht im Trainingskorpus von GPT enthalten waren.

  Abgrenzung: Ziel dieses Praktikums ist es nicht, neue KI-Modelle zu trainieren oder fine-tuning zu betreiben. Wir befassen uns ausschließlich mit der Interaktion mit bestehenden Modellen und beschränken die Optimierung auf Prompt Engineering.

  Betreuung: Samuel Teuber

• Analyse von Langzeit-Fairness mittels Probabilistischem Model Checking

  Dieses Projekt befasst sich mit der Frage von Langzeit-Effekten im Kontext algorithmischer Fairness: D’Amour et al. [1] untersuchten hierzu bereits wie sich Fairness-Eigenschaften verhalten, wenn man den Feedback-Loop zwischen einer algorithmischen Entscheidung und gesellschaftlicher Dynamik über längere Zeiträume betrachtet und ergänzten hiermit die Arbeit von Liu et al. [2].

  Das Ziel des Projektes wäre es zunächst eine von D’Amour et al. präsentierte Fairness-Simulationen (bspw. zur Kreditvergabe) mithilfe eines probabilistischen Model Checkers (z. B. mit Storm [3]) nachzubauen und die Ergebnisse dort (soweit möglich) zu reproduzieren. Im Anschluss sollen die Modelle dann um weitere Effekte ergänzt werden, um zu analysieren inwieweit dies Fairness-Eigenschaften verändert.

  [1] D'Amour, Alexander, et al. "Fairness is not static: deeper understanding of long term fairness via simulation studies." Conference on Fairness, Accountability, and Transparency (FAT* 2020).
  [2] Liu, Lydia T., et al. "Delayed impact of fair machine learning." International Conference on Machine Learning (PMLR 2018).
  [3] Hensel, Christian, et al. "The probabilistic model checker Storm." International Journal on Software Tools for Technology Transfer 24.4 (2022): 589-610.

  Betreuung: Samuel Teuber

Ansprechperson

Bei Fragen rund um das Thema Forschungspraktikum (hier oder bei anderen Vorlesungen) können Sie sich bei Michael Kirsten melden.