Die neuen Gesichter der TNF

Gleich elf neue Professor*innen forschen und lehren an der TN-Fakultät der JKU. Hier stellen wir sie vor - heute Martina Seidl.

Professorin Martina Seidl
Professorin Martina Seidl

Prof.in Martina Seidl hat am 1. Oktober 2020 ihre Professur für Artificial Intelligence angetreten. Warum es wichtig ist, Artificial Intelligence zu verstehen, wenn man sie gar nicht mehr verstehen kann und wieso sie gerne Spiele in ihrem Unterricht einsetzt, erzählt sie im Interview.

Frau Seidl, in welchem Bereich forschen Sie?
Martina Seidl: Meine Forschung ist im Bereich der symbolischen künstlichen Intelligenz angesiedelt, einem der ältesten Teilgebieten der künstlichen Intelligenz (KI). Hierbei werden Symbole und Regeln verwendet, um einer KI logisches Denken und Schlussfolgerungen beizubringen. Meine Forschung beschäftigt sich mit der schnellen Auswertung von logischen Formeln. Diese stellen Aussagen dar, die wahr oder falsch sind. Zum Beispiel können durch solche Formeln Regeln ausgedrückt werden, die eine KI befolgen muss, um ein bestimmtes Ziel zu erreichen. Daraus ergeben sich dann Fragestellungen wie “Kann das Ziel unter den vorgegebenen Regeln überhaupt erreicht werden?” oder “Wie teuer ist es, das Ziel zu erreichen?”. Für solche Aufgaben erforsche ich Techniken und entwickle Werkzeuge. 

Was begeistert Sie an diesem Bereich?
Martina Seidl: Mich begeistert die Verschmelzung von Theorie und Praxis. Auf den ersten Blick wirkt meine Arbeit sehr theoretisch und mathematisch, und viele Formalisierungen und Beweise entstehen tatsächlich zunächst am Papier. Interessant ist es dann zu sehen, ob die neuen Ideen auch wirklich zu Verbesserungen des State of the Art beitragen. Dies geschieht dann durch die Entwicklung von Computerprogrammen. Diese Programme werden dann sorgfältig evaluiert (auch im Rahmen von Wettbewerben) und führen dann oft wiederum zu neuen Arbeiten. Besonders schön ist es natürlich, wenn andere Forschungsgruppen Techniken und Programme für ihre Arbeiten aufgreifen und weiterentwickeln. 

Wofür ist diese Forschung überhaupt notwendig bzw. wie verbessert sie unser Leben?
Martina Seidl: Mit den Formeln, die ich untersuche, kann man eine Vielzahl von unterschiedlichen Fragestellungen ausdrücken und beantworten. Eine sehr erfolgreiche Anwendung ist die Verifikation der Korrektheit von Computersystemen und -programmen. Diese sind derart komplex, dass es nicht mehr möglich ist, von Hand sicherzustellen, dass diese auch so funktionieren wie sie sollen. Dies betrifft Hardware und Software in Handys, in Computern, aber auch in Flugzeugen. Nicht nur bei der Entwicklung von sicherheitskritischen Anwendungen spielen formale Methoden eine bedeutende Rolle - sie werden auch in sozialen Netzwerken eingesetzt. Andere Anwendungen sind Planungsprobleme wie zum Beispiel die Erstellung des Stundenplans einer Schule, Belegungsplänen von Hörsälen oder auch die Planung von großen Sportligen. 

Warum sollten sich Studierende Sie als Lehrenden wünschen?
Martina Seidl: Ich bemühe sehr, auch bei theoretischen Inhalten eine Praxisbezug herzustellen. Sehr oft hilft auch eine spielerische Komponente, das Interesse der Studierenden zu wecken. Zum Beispiel kann man sehr einfach Spiele wie Sudoku mittels logischen Formeln automatisch lösen.  Besonders ist es mir wichtig, Studierenden die Möglichkeit zu bieten, die Stärken und Schwächen von unterschiedlichen Formalismen selbst mit Programmen auszuprobieren. Außerdem denke ich, dass ich auch in großen Lehrveranstaltungen sehr bemüht bin, auf individuelle Fragen und Probleme einzugehen.  

An welchem Projekt arbeiten Sie momentan konkret?
Martina Seidl: Eine Frage, die mich sehr beschäftigt, ist die Korrektheit von Solvern, also den Programmen, die logische Formeln auswerten. Wenn ein Solver dazu verwendet wird, um zu verifizieren, ob ein anderes Programm korrekt ist, muss man sich darauf verlassen können, dass der Solver selbst korrekt ist. Allerdings ist ein Solver meist so komplex, dass dieser selbst nicht verifiziert werden kann und daher muss man sich andere Verfahren überlegen, um sicher zu sein, dass das gefundene Resultat stimmt. Konkret setze ich hierzu Techniken aus der Beweistheorie ein. 

Welche Hobbys haben Sie?
Martina Seidl: Ich habe eine 9 Monate alte Tochter. Im Moment gehört meine ganze Freizeit meiner Familie.

Was wollen Sie in Ihrem Leben unbedingt noch machen oder erreichen?
Martina Seidl: Es gibt sehr viele Forschungsfragen, die es noch gilt zu beantworten und ich freue mich auf eine spannende Zeit an der JKU.