„Es geht mir darum, logische Rätsel zu lösen“
Die Informatikerin Martina Seidl forscht an der Universität Linz zu künstlicher Intelligenz und beschäftigt sich auch mit der Frage, was diese mit menschlichem Denken gemein hat.
STANDARD: Sie haben kürzlich in einem Vortrag eine Verbindung zwischen dem antiken Griechenland und künstlicher Intelligenz hergestellt. Was hat Aristoteles mit Ihrer Forschung zu tun? Seidl: Menschen versuchen schon seit jeher, zu verstehen, wie das menschliche Denken funktioniert und wie man von vorhandenem auf neues Wissen schließen kann. Die alten Griechen haben erkannt, dass man die Welt mittels Symbolen repräsentieren kann. In Kombination mit Regeln kann man aus vorhandenen Fakten neues Wissen ableiten. Das klassische Beispiel von damals ist: Alle Menschen sind sterblich. Sokrates ist ein Mensch. Daher ist Sokrates auch sterblich. Das ist letztendlich die Grundlage für logisches Denken, logisches Schließen und hat Einzug in die Mathematik, die Informatik und die künstliche Intelligenz gefunden. So ist es schließlich auch Teil der Formalismen geworden, die hinter symbolischer künstlicher Intelligenz stehen.
STANDARD: Was genau ist symbolische künstliche Intelligenz?
Seidl: Dafür muss ich etwas ausholen: Künstliche Intelligenz basiert auf verschiedenen Verfahren. Wenn wir zum Beispiel von maschinellem Lernen sprechen – auch ein Teil der KI –, geht es darum, mit großen Datenmengen neues Wissen abzuleiten und Muster zu erkennen. Bilder werden durchsucht, um etwa sagen zu können: Das ist eine Katze. Dafür braucht man Trainingsbeispiele, und mit der Zeit kann man sehr gut mit Unschärfe umgehen. Eine Vorgehensweise, die wir auch im menschlichen Denken finden. Wir müssen auch sehr oft sehr schnell Entscheidungen basierend auf unvollständigen Informationen und basierend auf Erfahrungen treffen. Und dann gibt es noch eine Art des Denkens, bei der wir fixe Regeln haben und diese anwenden, um etwas Neues abzuleiten. Symbolische künstliche Intelligenz basiert genau darauf: die Konzepte, auf die wir Regeln anwenden wollen, mit Symbolen darstellbar zu machen.
STANDARD: Lässt sich so jede Art von Wissen darstellen?
Seidl: Ich beschäftigte mich mit Formeln, die entweder wahr oder falsch sind. In diesen Formeln werden Aussagen miteinander verknüpft, und so kann man komplexere Aussagen formen. Man kann das für Planungsprobleme verwenden: Wenn man zum Beispiel einen Stundenplan erstellen will, gibt es Einschränkungen wie die Verfügbarkeit von Räumen oder Vortragenden. Die Lösung dieser Formel wäre ein Stundenplan, der für alle funktioniert, oder die Information, dass es keine Lösung gibt.
STANDARD: Wo wird das angewendet?
Seidl: Eine wichtige Anwendung ist die Verifikation von Software und Hardware. Man will sicherstellen, dass Programme das machen, was sie machen sollen. Das muss man erst mal formulieren, und hierbei helfen logikbasierte Sprachen. Wenn man sich in natürlicher Sprache unterhält, dann passiert es sehr leicht, dass es zu Missverständnissen kommt. Logik ist eine künstliche Sprache, die so designt ist, dass es keine Mehrdeutigkeiten gibt. Wir haben eine Semantik definiert, also genau festgelegt, was ein logischer Ausdruck bedeutet. Das ist ähnlich wie in der Mathematik, in der wir auch genau wissen, was 1 + 2 bedeutet. Ich arbeite mit Aussagen, die wahr oder falsch sind. Wenn wir nun ein Programm analysieren, kann man zum Beispiel fordern: Ein Ausdruck, der im Programm vorkommt, darf niemals kleiner als Null werden. Dann kann man das Programm in eine logische Formel übersetzen und fragen, ob diese Bedingung bei jeder Ausführung erfüllt ist. Dadurch kann man beweisen, dass ein gewisser Fehler niemals auftritt. Firmen, die sich nicht leisten können, Fehler in Software oder Hardware zu haben, brauchen solche Techniken.
Was sind die großen offenen Fragen, die Sie in Ihrer Forschung behandeln?
STANDARD:
Seidl: Es gibt immer einen Trade-off zwischen Ausdrucksstärke der Logik und Komplexität. Also wie teuer ist es berechnungstechnisch, die Formel auszuwerten und eine Lösung zu bekommen? Man kann sich das so vorstellen: Wenn wir zwei elementare Aussagen haben, die wahr oder falsch sein können, kann die erste wahr und die zweite wahr sein; die erste wahr, die zweite falsch; die erste falsch und die zweite wahr; oder beide falsch. Und all diese Möglichkeiten müssen für die Auswertung der Formel überprüft werden. Wenn man sich das überlegt, gibt es eine exponentielle Anzahl dieser elementaren Aussagen. In praktischen Anwendungen hat man Millionen davon, und das macht das Lösen solcher Formeln schwierig. Je mehr man automatisieren will und je mehr Sicherheit man haben will, umso schwieriger werden die Probleme.
STANDARD: Könnten diese komplexen Beweise überhaupt noch von Menschen erbracht werden? Seidl: Nein, das läuft alles maschinell, das ginge nicht. Ein Kollege von mir, der zuvor in Linz war und jetzt in Pittsburgh forscht, hat es mit dem „largest math proof ever“– also dem größten Mathebeweis – in die Medien geschafft. Das sind Gigabyte oder Terabyte von Beweisschritten, die man da produziert. Dafür haben wir Techniken entwickelt, um solche Beweise schnell zu verifizieren. Prinzipiell geht es in unserer Forschung darum, hierfür schnellere Verfahren zu finden – damit Computer diese Probleme schneller lösen können.
STANDARD: Der CEO von Google, Sundar Pichai, ließ kürzlich mit der Aussage aufhorchen, dass künstliche Intelligenz mehr Einfluss haben wird als die Erfindung des Feuers. Stehen wir erst am Anfang?
Seidl: Ich bin skeptisch, ob künstliche Intelligenz tatsächlich einmal mehr Einfluss als die Erfindung des Feuers haben wird. Aber all die Techniken, die im Rahmen der KI-Forschung entwickelt werden, haben jetzt schon einen enormen Einfluss – und der wird immer größer werden. Die Entwicklungen gehen hier auch in sehr viele Richtungen. Wenn es mal gelingt, eine gemeinsame Strategie zu finden, hätte das Potenzial, das wir uns im Moment gar nicht vorstellen können.
Zuletzt erwähnten Sie in Ihrer Antrittsvorlesung, dass Sie einen spielerischen Ansatz bei der Erforschung von künstlicher Intelligenz wählen wollen. Was bedeutet das?
STANDARD:
„Ich bin skeptisch, ob künstliche Intelligenz einmal mehr Einfluss als die Erfindung des Feuers haben wird.“
Seidl: Wenn ich Menschen erzähle, dass meine Arbeit sehr nah an der Mathematik und sehr formal ist, dann ist das Gespräch meistens schnell beendet. Aber wenn man mit Leuten über das Spiel Sudoku redet, dann ist fast immer eine Begeisterung zu spüren. Das macht fast jeder gerne. In den Formeln, mit denen ich mich beschäftige, geht es genau darum, solche logischen Rätsel zu lösen. Ich habe einige Repräsentationen meiner logischen Formeln entwickelt, die Leute jedes Alters lösen können. Sie entwickeln interessanterweise auch selbst Techniken, wie man durch strukturelle Analyse diese Probleme besser lösen kann. Wenn ich ihnen das formal aufschreiben würde, würden sie sofort sagen: Das ist nicht meins.
MARTINA SEIDL, geboren 1980 in Klosterneuburg, ist Professorin für Künstliche Intelligenz an der Universität Linz und hielt kürzlich ihre Antrittsvorlesung. Seit Oktober 2020 leitet sie das Institut für Symbolic Artificial Intelligence.