Interview

Formale Beweise in natürliche Sprache übersetzen

Prof. Birte Glimm ist stellvertretende Institutsdirektorin am Institut für Künstliche Intelligenz der Universität Ulm. Sie entwickelt und optimiert mit ihrer Forschergruppe Algorithmen zum automatischen Schlussfolgern und analysiert deren Komplexität. Die Informatikerin ist Research Fellow bei fortiss und wird in das Leitprojekt Robuste KI eingebunden und mit den fortiss-Kompetenzfeldern Robotics and Machine Learning, Business Model and Service Engineering und Model-based Systems Engineering zusammenarbeiten.


Menschen tauschen Wissen aus, in dem sie mit anderen kommunizieren, sei es mündlich oder schriftlich. Welchen Weg gibt es für technische Systeme?

In der Wissensrepräsentation modellieren wir das Wissen, das die Systeme über die Anwendungsdomäne haben müssen. Ein Beispiel hierfür ist der intelligente Do-it-yourself-Assistent, den wir mit einem Industriepartner entwickeln. Dafür werden Eigenschaften von Materialien und Werkzeugen modelliert oder Aktionen, die mit den Materialien und Werkzeugen durchgeführt werden können. Übertragen auf die Domäne Heimwerker würde das System schließen: „Fichtenholz ist ein Weichholz; für Schrauben mit einem Durchmesser unter drei Millimetern muss bei Weichholz nicht vorgebohrt werden.“ Dies ist auch ein Prozess, bei dem das maschinennutzbare Wissen schrittweise erweitert wird. Teilweise kann auch bereits vorhandenes, formalisiertes Wissen genutzt werden, sodass auch Maschinen im Prinzip Wissen austauschen können.


Das heißt, die Entwicklung geht dahin, dass technische Systeme künftig wie Menschen aus wenigen Beobachtungen Regeln aufstellen und Schlüsse für alle anderen mögliche Fälle ziehen werden?

Das bekannteste Beispiel für logische Schlüsse ist wohl der Syllogismus. Aus dem Wissen „Alle Menschen sind sterblich“. und „Sokrates ist ein Mensch“, lässt sich „Sokrates ist sterblich“ ableiten. Die beiden gegebenen Tatsachen sind in diesem Fall unsere Prämissen. Der Schluss wird auch als Konklusion bezeichnet. Dieser Syllogismus ließe sich zum Beispiel formalisieren zu: „Alle X sind Y“ und „Z ist ein X“. Daraus folgt: „Z ist Y“. Hierbei sind X, Y und Z nun die Platzhalter. In der logikbasierten Wissensrepräsentation geht es darum, Regeln aufzustellen, anhand derer sich gültige Schlüsse ziehen lassen und dies möglichst effizient.


Sie haben mit anderen Forschern ein Schlussfolgerungswerkzeug entwickelt. Warum ist es wichtig, den Prozess zu automatisieren?

Computer können Schlüsse einfach schneller ziehen. Große medizinische Wissensbasen bestehen beispielsweise aus mehreren Hunderttausend Axiomen, also gegebenem Wissen über Krankheiten, Medikamente oder die menschliche Anatomie. Da dieses Wissen von mehreren Experten über längere Zeit erstellt wurde, schleichen sich ab und zu Fehler ein, die mittels automatisierter Verfahren gefunden werden können. Die Fülle an Wissen lässt sich für Menschen ohne maschinelle Hilfe eigentlich nicht mehr in der Gesamtheit überblicken.


Menschen erkennen Inkonsistenzen bzw. Regelabweichungen. Ein Beispiel hierfür: Alle Vögel können fliegen. Der Pinguin kann nicht fliegen. Die Maschine würde schließen: Der Pinguin ist kein Vogel – obwohl er zur Klasse der Vögel gehört. Welche Konzepte haben die Wissenschaftler, um solche Probleme zu lösen?

Ganz so schlimm ist es in der logikbasierten Wissensrepräsentation zum Glück nicht. Die Maschine würde hier finden, dass keine Aussage dazu gemacht werden kann, ob Pinguine Vögel sind. Adressiert werden kann das beispielsweise in sogenannten Default-Logiken, in denen festgelegt werden kann, dass Vögel normalerweise fliegen. Wenn einer Maschine dann gesagt wird, dass Tweety ein Vogel ist und dass Vögel normalerweise fliegen, dann wird solange davon ausgegangen, dass Tweety fliegen kann, bis eine gegenteilige Information bekannt wird, in dem Fall: Tweety ist ein Pinguin und Pinguine fliegen nicht.


Derzeit ist es so, dass Entscheidungen von KI-Technologien nicht transparent sind. Wenn Algorithmen falsche Schlüsse ziehen, wie lässt sich das nachweisen?

Dieser Makel existiert vor allen Dingen für Ansätze des maschinellen Lernens, die meist Black-Box-Verfahren sind. Da ist die Transparenz ganz klar ein aktueller Forschungsgegenstand. Bei logikbasierten Verfahren, wie wir sie entwickeln, kann die Maschine dagegen einen Beweis, also eine formale Erklärung darüber erbringen, wie sie zu einem Schluss gekommen ist. Hier ist dann eher die Herausforderung, wie ich diese formalen Beweise Nutzern geeignet darbieten kann.


Welche Möglichkeiten gäbe es hierfür?

Wir entwickeln hier Verfahren, um formale Beweise in natürliche Sprache zu übersetzen. Eine Herausforderung hierbei ist, dass Systeme die automatische Beweise generieren auf Performanz optimiert sind und nicht auf die Generierung möglichst kurzer Beweise. Wir haben daher Ansätze entwickelt, um möglichst kurze Beweise zu erzeugen. Zusammen mit weiteren Optimierungen zum Beispiel zur Zusammenfassung von Beweisschritten lassen sich dann prägnantere Erklärungen erzeugen. Allerdings sind die systemgenerierten Erklärungen noch relativ lang und in Teilen repetitiv. Deshalb arbeiten wir an weiteren Strategien zur kompakten, aber dennoch informativen Darstellung. Dabei soll auch Vorwissen der NutzerInnen berücksichtigt werden, denn bereits bekannte Aspekte müssen nicht erneut oder in der gleichen Ausführlichkeit erklärt werden. 


Welches Projekt möchten Sie mit fortiss anstoßen?

Ich würde mich freuen, wenn wir gemeinsam an der Herausforderung der „hybriden“ Künstlichen Intelligenz arbeiten könnten, also der Frage wie regelbasierte Ansätze erfolgreich mit lernbasierten Ansätzen zusammengebracht werden können.


Welche Anwendungen ließen sich damit realisieren?

Wir haben hier gerade erste Ansätze zur Verbesserung von Sprachassistenten entwickelt. So ist beispielsweise das Erkennen menschlicher Absichten aus Sprache meist lernbasiert. Nachdem ein System genügend menschliche Aussagen gehört hat, von denen bekannt ist, welche Absicht dahintersteht, generalisiert ein lernbasiertes System. So kann es auch bisher nicht gehörte Aussagen einer Absicht zuordnen. Oft hat ein System aber weiteres Wissen darüber, in welchem Kontext sich eine NutzerIn gerade befindet. Dieses Wissen kann ich nutzen, um Aussagen bei denen das System unsicher ist, transparent zu machen.


Können Sie eine Aussage darüber machen, wann solche Systeme einsatzfähig sein werden?

Auch wenn wir an der Universität geeignete Technologien entwickeln, begleiten wir nur selten die Einführung bis in wirkliche Anwendungen. Ich würde mich um so mehr freuen, wenn ich den Weg bis in die Anwendungen über fortiss weiter mitverfolgen könnte.