Die Österreichische Akademie der Wissenschaften (ÖAW) hat wieder eine Reihe von Stipendien für Dissertationsprojekte vergeben. Drei davon gehen an Doktoranden der TU Wien. Überraschenderweise verbindet zwei der Projekte eine kulinarische Note: Während Christoph Spiess an mathematischen Sandwiches forscht, entwickelt Maximilian Kovar ein Kochbuch für künstliche Intelligenz. Johannes Weiser komplettiert das Trio mit einer Dissertation über die theoretischen Grenzen von Methoden zur automatischen Überprüfung von Computerprogrammen – was sehr theoretisch klingt, hat jedoch enorme praktische Auswirkungen.

Maximilian Kovar: „Data for Chemical Reaction Machine Learning"

Dissertationsbetreuerin: Esther Heid
Institut für Materialchemie, Fakultät für Technische Chemie

Maximilian Kovar ist Doktorand am Institut für Materialchemie der TU Wien. In seiner Dissertation beschäftigt er sich mit maschinellem Lernen im Bereich chemischer Reaktionen. Die KI soll künftig schon vor Experimenten abschätzen, ob Reaktionen funktionieren, unter welchen Bedingungen sie optimal ablaufen und ob der Aufwand gerechtfertigt ist. So lassen sich Ressourcen sparen und gefährliche Experimente minimieren.

Damit solche Modelle verlässliche Vorhersagen treffen können, brauchen sie jedoch hochwertige Trainingsdaten. Genau hier setzt das Forschungsprojekt an: Es untersucht, welche chemischen Reaktionen sich besonders gut eignen, um künstliche Intelligenz effizient zu trainieren und warum. Dabei geht es auch um grundlegende Fragen der Vorhersagbarkeit und chemischen Ähnlichkeit. Ziel ist es effiziente Datensätze zu erstellen, die als Lehrbuch für zukünftige KI-Assistenten in der Synthesechemie dienen können.

Man kann sich das wie ein Kochbuch für eine künstliche Intelligenz vorstellen: Es soll nicht möglichst viele Rezepte enthalten, sondern genau die richtigen Beispiele. Das Modell soll die Grundprinzipien verstehen lernen, um aus den passenden Ausgangsstoffen unter den richtigen Bedingungen die gewünschte Reaktion erfolgreich zu „kochen", wie man auch in der Chemie sagt.

Christoph Spiess: „Omega-categorical sandwiches for Promise Constraint Satisfaction Problems"

Dissertationsbetreuer: Michael Pinsker
Institut für Diskrete Mathematik und Geometrie, Fakultät für Mathematik und Geoinformation

Christoph Spiess beschäftigt sich in seiner Dissertation damit, wie Einschränkungen zur Erfüllung von Bedingungen überwunden werden. Ein Algorithmus muss dabei entscheiden, ob sich bestimmte Vorgaben gleichzeitig erfüllen lassen. Ein klassisches Beispiel: Lässt sich eine Landkarte mit nur drei Farben so einfärben, dass benachbarte Länder nie dieselbe Farbe haben?

Solche CSPs werden durch mathematische Strukturen beschrieben. Kombiniert man zwei davon, entsteht ein Promise-CSP (PCSP). Die Frage lautet dann nicht mehr nur „Geht es mit drei Farben?", sondern „Geht es mit drei Farben – oder scheitert es sogar mit fünf?". Und hier wird die Mathematik kulinarisch: Findet man eine weitere Struktur, die zwischen diesen beiden liegt, nennt man sie „Käsestruktur“. Zusammen mit den beiden endlichen „Brotstrukturen“ bildet sie ein mathematisches Sandwich. Der Clou: Hat man einen Algorithmus für das CSP der Käsestruktur, besitzt man damit automatisch auch einen Algorithmus für das PCSP des gesamten Sandwiches – das essfertige Gericht, sozusagen: Christoph Spiess forscht daran, unendliche Käsestrukturen zu identifizieren, deren bekannte Algorithmen sich effizient auf endliche Promise-CSPs übertragen lassen. Damit könnten Forschende zukünftig auf bewährte CSP-Algorithmen zurückgreifen, anstatt sie für jedes neue Problem neu zu entwickeln. Das spart Rechenzeit, eröffnet neue Anwendungsfelder und stärkt die Brücke zwischen theoretischer Mathematik und praktischer Algorithmik.

Johannes Weiser: „Limits of Methods for Solving Constrained Horn Clauses"

Dissertationsbetreuer: Stefan Hetzl
Institut für Diskrete Mathematik und Geometrie, Fakultät für Mathematik und Geoinformation

Johannes Weiser erforscht in seiner Dissertation die theoretischen Grenzen von Methoden zur automatischen Überprüfung von Computerprogrammen – sein scheinbar abstraktes Thema ist tief im Alltag aller Nutzer_innen verankert.

Im Mittelpunkt stehen Constrained Horn Clauses, ein mathematischer Formalismus, mit dem sich Software modellieren und analysieren lässt. Damit kann überprüft werden, ob ein Programm unter allen denkbaren Eingaben sicher ausgeführt wird – oder ob es etwa zu einem Absturz kommt, weil eine Division durch Null auftritt. Man kann sich das wie eine Art „mathematischen Sicherheitscheck" vorstellen, der garantiert, dass die Software keine unerwarteten Fehler macht.

Der Haken daran: Eine vollständige automatische Überprüfung von Software ist grundsätzlich nicht möglich. In der Praxis kommen daher verschiedene Methoden zum Einsatz, die jeweils nur bestimmte Fälle lösen können. Scheitert eine solche Methode, bleibt oft unklar, ob es an begrenzten Ressourcen liegt oder an einer fundamentalen Grenze des Algorithmus.

Johannes Weiser setzt hier an und sucht nach den theoretischen Grenzen dieser Methoden. Damit hilft er herauszufinden, welcher Algorithmus am besten geeignet dafür ist, ein bestimmtes Problem zu lösen. Das verbessert nicht nur das Verständnis bestehender Verfahren, sondern unterstützt auch die Entwicklung neuer, effizienterer Methoden, etwa in kritischen Bereichen wie Medizintechnik über die Flugsteuerung bis hin zu Banking-Systemen. Wo Fehler lebensgefährlich oder kostspielig werden können, trägt diese Forschung dazu bei, dass Programme ihre „Hausaufgaben" machen, bevor sie überhaupt zum Einsatz kommen.

Wir gratulieren den Stipendiaten!