Bookmark
Studien-/ Abschlussarbeit, Praktikum

Strategien für Paritätsspiele via Graph Neural Networks lernen

Beginn

1. Dezember 2022

Dauer

3 - 6 Monate, abhängig von Vorgaben der Hochschule

Vergütung

bis Entgeltgruppe 5 TVöD

Beschäftigungsgrad

Vollzeit

Paritätsspiele sind graphbasierte Spiele, die in vielen Bereichen der Programmverifikation und Programmsynthese genutzt werden. Um ein Paritätsspiel zu lösen, muss für jeden Knoten des Graphen ein geeigneter Nachfolgeknoten gefunden werden. Es ist bisher kein Algorithmus mit effizienter Worst-Case-Laufzeit bekannt, um Paritätsspiele zu lösen.

Graph Neural Networks (GNNs) können Metriken für Graphen lernen und diese Metriken auf neue Eingabespiele anwenden. Das Neural Network generiert eine Knotenbeschriftung, wobei jeder Knoten mit einem Wert zwischen 0 und 1 beschriftet wird. Man kann diese Beschriftung als Vorhersage nutzen, welcher Spieler von einem gegebenen Knoten gewinnt. Die Knotenbeschriftung liefert allerdings keine Informationen über die Züge, die eine Spielerin von einem Knoten aus spielen muss, um zu gewinnen.

Es existieren am Institut bereits Vorarbeiten, in denen Gewinnregionen für zufällig generierte Paritätsspiele mithilfe von Graph Neural Networks vorhergesagt wurden. Diese Ergebnisse dieser Vorarbeiten deuten darauf hin, dass dieser Ansatz zu einer effizienten und in der Praxis effektiven Lösung von Paritätsspielen genutzt werden kann.

Im Rahmen Ihrer Abschlussarbeit oder Ihres Praktikums beantworten Sie eine oder mehrere der folgenden Forschungsfragen:

  • bisher wurden nur Gewinnregionen anhand von Knotenbeschriftungen vorhergesagt. GNNs können allerdings auch Kantenbeschriftungen generieren. Können diese Kantenbeschriftungen genutzt werden, um eine Gewinnstrategie vorherzugsagen?
  • im Rahmen der Vorarbeiten wurden Strategien für Paritätsspiele erzeugt. In der Praxis bieten allerdings Büchispiele bereits eine hinreichend große Ausdrucksstärke, um eine große Zahl von nützlichen Spezifikationen auszudrücken. Kann die Effektivität oder Effizienz des GNN-basierten Lösers gesteigert werden, wenn nur Büchispiele gelöst werden?
  • die Klasse an untersuchten Spielen kann weiter eingeschränkt werden, indem nur Büchispiele betrachtet werden, die aus einer LTL-Spezifikation generiert wurden. Kann die Effektivität oder Effizienz des GNN-basierten Lösers gesteigert werden, wenn nur auf diese Art erzeugte Büchispiele gelöst werden?
  • in den Vorarbeiten wurden die gegebenen Paritätsspiele nur qualitativ gelöst, eine Lösung ist also entweder korrekt oder inkorrekt. Es gibt Metriken zur quantitativen Bewertung von Lösungen, zum Beispiel anhand ihrer Effizienz (https://lmcs.episciences.org/3938) oder anhand ihrer Robustheit gegenüber unerwarteten Eingaben (https://link.springer.com/article/10.1007/s00236-019-00345-7). Welche Güte erreicht ein GNN-basierter Löser für Paritätsspiele anhand dieser Metriken?

Ihre Qualifikation:

  • Kenntnisse in Python
  • Kenntnisse in Neural Networks
  • Grundkenntnisse in Graphentheorie
  • Bereitschaft zur Einarbeitung in Paritätsspiele
  • Kenntnisse in der Nutzung von PyTorch und PyTorch Geometric sind von Vorteil

Ihr Start:

Freuen Sie sich auf einen Arbeitgeber, der Ihr Engagement zu schätzen weiß und Ihre Entwicklung durch vielfältige Qualifizierungs- und Weiterbildungsmöglichkeiten fördert. Unser einzigartiges Arbeitsumfeld bietet Ihnen Gestaltungsfreiräume und eine unvergleichbare Infrastruktur, in der Sie Ihre Mission verwirklichen können. Vereinbarkeit von Privatleben, Familie und Beruf sowie Chancengleichheit von Personen aller Geschlechter (w/m/d) sind wichtiger Bestandteil unserer Personalpolitik. Bewerbungen schwerbehinderter Menschen bevorzugen wir bei fachlicher Eignung.

  • Jetzt online bewerben
  • Sie können sich diese Stellenanzeige per E-Mail zusenden und Ihre Bewerbung am stationären Computer oder Laptop erstellen.

    Wir benötigen Ihre digitalen Bewerbungsunterlagen (PDF). Die Übermittlung wird von einigen Mobilgeräten nicht standardmäßig unterstützt. Bitte erstellen Sie Ihre Bewerbung an einem PC/Laptop.

    Bewerbung am PC erstellen

Fachliche/r Ansprechpartner/in

Dr. Alexander Weinert
Institut für Softwaretechnologie

Tel.: +49 2203 601-5053

Nachricht senden

Kennziffer 71698

Personalbetreuung Köln

Nachricht senden

DLR-Standort Köln, Hauptverwaltung

zum Standort

DLR-Institut für Softwaretechnologie

zum Institut