Im Oktober finden an der Johannes Kepler Universität Linz wieder die traditionellen Antrittsvorlesungen neuer Professor*innen statt. Den Auftakt macht am 4. Oktober Prof.in Martina Seidl (Institut für Symbolic Artificial Intelligence). Sie spricht um 16.00 Uhr im Festsaal der JKU über "Symbolic Artificial Intelligence: Intelligenz durch formale Logik".

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.

Worum geht es in Ihrer Antrittsvorlesung konkret?
Martina Seidl: Artificial Intelligence ist ein riesiges wissenschaftliches Gebiet, das aus vielen Teilbereichen besteht. Einer der ältesten dieser Teilbereiche ist die Symbolic Artificial Intelligence. Hier wird Wissen durch Symbole repräsentiert. Die Anwendung von gewissen Regeln erlaubt es, aus vorhandenem Wissen neues Wissen abzuleiten. Die Einsatzbereiche sind vielfältig: sei es etwa um Fehler in Software- und Hardwaresystemen zu finden, die Konsistenz von großen Datenmengen sicherzustellen oder um Planungsprobleme zu lösen. In diesem Vortrag werden wir exemplarisch einen der wichtigsten Formalismen der Symbolic Artificial Intelligence betrachten. Wir werden erklären, warum ein scheinbar einfaches Problem schwierig zu lösen ist, und aufzeigen, welche spannenden Forschungsfragen sich aus diesem und verwandten Problemen ergeben.

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.

Rückfragehinweis
Mag. Christian Savoy
PR-Manager
Universitätskommunikation
T +43 732 2468 3012
christian.savoy@jku.at