In den vergangenen Monaten hat das Sprachmodell ChatGPT weltweit für Schlagzeilen gesorgt. Der im November 2022 veröffentlichte Chatbot der Firma OpenAI kann menschliche Sprache so überzeugend verarbeiten, dass er ähnlich kreativ und intelligent wie ein Mensch wirkt: Er gibt detaillierte Antworten auf schriftliche Fragen und kann Gedichte oder Lieder verfassen. Allerdings sind solche Programme nicht vertrauenswürdig. Sie treffen manchmal unlogische Aussagen oder geben selbstsicher Unwahrheiten als Tatsachen aus. »Sie sprechen von Einhörnern, vergessen dann aber, dass die Fabelwesen bloß ein Horn besitzen«, sagt der Mathematiker und KI-Experte Jason Rute von IBM Research.

Dahinter steckt mehr als nur ein Programmierfehler. Sprachmodelle können ihre Fehler nur schwer erkennen, was ihre Leistung einschränkt. Aber nicht jede künstliche Intelligenz (KI) leidet unter dieser Schwäche. Seit mehreren Jahren gibt es Algorithmen, die durch »reinforcement learning« aus ihren Fehlern lernen – und so zu Meistern von strategischen Spielen wie Schach und Go werden. Diese Art des Lernens beherrschen Sprachmodelle wie ChatGPT bisher jedoch nicht.

»Wir wollen kein Sprachmodell schaffen, das einfach wie ein Mensch spricht«, sagt Yuhuai Wu von Google AI. »Wir wollen, dass es versteht, worüber es redet.« Wu hat 2022 zusammen mit seinen Kolleginnen und Kollegen zwei Arbeiten veröffentlicht, die das ehrgeizige Ziel ermöglichen könnten. Auf den ersten Blick geht es dabei um eine sehr spezifische Anwendung: der künstlichen Intelligenz Mathematik beibringen. Doch durch diese Fähigkeit werden Computer künftig logische Schlüsse ziehen, hoffen die Fachleute.

Mathematiker brauchen Tausende von Stunden, um einen Beweis zu formalisieren, weshalb sie nur selten auf Beweisassistenten zurückgreifen

In der ersten Arbeit haben die Forscher einem Sprachmodell beigebracht, mathematische Aussagen in einen formalen Code zu übersetzen, damit ein »Beweisassistent« sie überprüfen kann. Der Ansatz ist nicht neu: Seit Jahrzehnten gibt es Bemühungen, Beweise in Computercode zu übertragen – ein Prozess, der als Formalisierung bezeichnet wird. Der Vorteil davon liegt auf der Hand: Wenn man eine Argumentation als Code darstellt und ein Computer diesen ohne Fehler ausführt, dann ist sie zwangsläufig korrekt. Allerdings brauchen Menschen Hunderte oder gar Tausende von Stunden, um einen einzigen Beweis zu formalisieren, weshalb Mathematikerinnen und Mathematiker nur selten auf Beweisassistenten zurückgreifen.

Eine KI übersetzt Mathematik in Computercode

Um den Aufwand zu verringern, versuchen KI-Experten nun Sprachmodellen beizubringen, mathematische Aussagen automatisch in eine »formale Sprache« zu übertragen. KI-Programme wie GPT oder DeepL können bereits erfolgreich menschliche Sprachen ineinander übersetzen. Aber die Übersetzung von Mathematik in Code ist deutlich schwieriger. Es gibt viel weniger Übersetzungsbeispiele, mit denen man eine KI trainieren kann. Außerdem enthalten formale Sprachen nicht immer den gesamten Wortschatz, der in einem ausgeschriebenen Beweis vorkommt.

Deshalb haben sich die Fachleute entschieden, zunächst nur kurze mathematische Aussagen von einer KI übersetzen zu lassen – und nicht gleich ganze Beweise. Dafür haben sie mit dem Sprachmodell »Codex« gearbeitet, das sich auf GPT-3 (eine Vorgängerversion von ChatGPT) stützt, zusätzlich aber mit Daten aus Quellen wie GitHub trainiert wurde. Um Codex das Formalisieren beizubringen, übergaben die Forscherinnen und Forscher der KI lediglich zwei Beispiele: je ein mathematisches Problem in natürlicher Sprache und dessen formale Code-Übersetzung.

»Das ist das größte Problem bei Sprachmodellen: Sie raten oft«Jason Rute, Mathematiker und KI-Experte

Nach diesem spärlichen Tutorial fütterten sie Codex mit knapp 4000 Aufgaben aus Highschool-Wettbewerben. Das Ergebnis scheint auf den ersten Blick nicht sonderlich beeindruckend: Die Übersetzungen in die formale Sprache namens Isabelle/HOL waren in 70 Prozent der Fälle falsch. »Manchmal weiß das Sprachmodell zum Beispiel nicht, was der Isabelle-Name für ›Primzahl‹ oder für ›Fakultät‹ ist – und erfindet es einfach. Das ist das größte Problem bei diesen Modellen«, sagt Jason Rute, »sie raten oft.« Doch für die Fachleute war nicht wichtig, dass Codex in 70 Prozent der Fälle versagte, sondern dass die KI bei 30 Prozent erfolgreich war – und das, nachdem sie bloß zwei Beispiele gesehen hatte!

Das verdeutlicht eine spannende Eigenschaft von Sprachmodellen: Mit genügend allgemeinen Trainingsdaten lernen sie nicht nur, natürliche Sprache zu verarbeiten, sondern erlangen gleichzeitig weitere Fähigkeiten. Codex war vor dieser Forschungsarbeit nie darauf trainiert worden, Aussagen in formalen Code zu übersetzen. Aber durch das Training mit den GitHub-Daten war die KI mit Isabelle/HOL vertraut, und durch andere Internetseiten kannte sie mathematische Probleme. Deshalb reichte es, Codex zwei Beispiele für das Gewünschte zu zeigen. »Wirklich erstaunlich ist, dass die Autoren nicht viel getan haben«, betont Rute. »Das Modell besaß bereits die Fähigkeit für diese Aufgabe.« Etwas Ähnliches konnte das Team um Wu beobachten, als es einem Sprachmodell nicht nur beibrachte, Rechenaufgaben zu übersetzen, sondern sie zu lösen.

Die KI Minerva löst Aufgaben mit Zwischenschritten

Damit beschäftigt sich die zweite Arbeit der Forscher und Forscherinnen. In diesem Fall trainierten sie eine KI, Matheaufgaben auf Highschool-Niveau Schritt für Schritt zu berechnen. Zum Beispiel: »Eine Gerade parallel zu y = 4x + 6 verläuft durch den Punkt (5, 10). Wie lautet die y-Koordinate des Punkts, an dem diese Gerade die y-Achse schneidet?« Dafür griffen die Fachleute auf die Google-KI PaLM zurück, die wie GPT-3 natürliche Sprache verarbeiten kann, und trainierten sie zusätzlich mit mathematischen Inhalten von Internetseiten wie dem Preprint-Server ArXiv. Das erweiterte KI-Modell nannten sie »Minerva«.

Um den Algorithmus auf seine bevorstehende Aufgabe vorzubereiten, präsentierten ihm die Forscherinnen und Forscher vier Beispiele: schrittweise ausformulierte Lösungswege für mathematische Textaufgaben. Im Praxistest schnitt Minerva dann je nach Themenfeld unterschiedlich ab: In Algebra beantwortete es die Fragen in etwas mehr als der Hälfte der Fälle richtig, während es bei Geometrie häufiger falschlag.

»Wenn man ein Sprachmodell bittet, sich Schritt für Schritt zu erklären, erhöht sich die Genauigkeit immens«Siddhartha Gadgil, Mathematiker

Um die Ergebnisse einzuordnen, mussten die Autorinnen und Autoren sicherstellen, dass Minerva die Fragen nicht nur deshalb richtig beantwortet, weil es diese oder ähnliche Aufgaben bereits aus den Trainingsdaten kannte. »In den Modellen stecken so viele Informationen, dass sie eine Standardaufgabe sehr wahrscheinlich schon einmal gesehen haben«, erklärt Rute. Um dieser Möglichkeit vorzubeugen, sollte Minerva eine polnische Mathematikprüfung aus dem Jahr 2022 lösen, die erst nach dem Training veröffentlicht wurde. Die KI hat beeindruckende 65 Prozent der Fragen richtig beantwortet. Das deutet auch in diesem Fall darauf hin, dass sie bereits über die erforderlichen Fähigkeiten verfügte, bevor man ihr die vier ausgewählten Beispielaufgaben mit Lösungen übergab. »Das ist eine Lektion, die wir beim Deep Learning immer wieder lernen: Skalierung hilft erstaunlich gut bei vielen Aufgaben«, sagt Guy Gur-Ari, Koautor der Studie.

Die Forscher und Forscherinnen konnten Minervas Leistung sogar steigern: indem sie das Programm ein Problem mehrmals lösen ließen und das am häufigsten genannte Ergebnis auswählten. Dadurch stieg der Anteil korrekter Antworten in manchen Fällen von 33 auf 50 Prozent an. Was noch erstaunlicher ist: »Wenn man ein Sprachmodell bittet, sich Schritt für Schritt zu erklären, erhöht sich die Genauigkeit immens«, erklärt der Mathematiker Siddhartha Gadgil vom Indian Institute of Science in Bangalore. Diese Methode scheint für KIs dieselben Vorteile zu bieten wie für Menschen: Man ist gezwungen, sich mehr Zeit zu nehmen, und widmet dadurch jedem Aufgabenteil mehr Aufmerksamkeit.

Die Arbeit von Minerva ist zwar beeindruckend, hat aber einen erheblichen Nachteil: Die KI kann nicht überprüfen, ob sie eine Frage korrekt beantwortet hat. Selbst wenn sie richtiglag, kann sie nicht sicherstellen, dass die Zwischenschritte fehlerfrei waren. »Manchmal kommen die Programme zu falsch positiven Ergebnissen mit falschen Begründungen für richtige Antworten«, sagt Gadgil. Deshalb ist das Modell auf menschliches Feedback angewiesen, um besser zu werden. Das ist jedoch ein langwieriger und aufwändiger Prozess. »Ich glaube nicht, dass dieser Ansatz für komplizierte Probleme geeignet ist«, sagt Christian Szegedy, KI-Forscher bei Google und Mitverfasser der Arbeit.

Ein Brücke zwischen Übersetzung und Überprüfung

Stattdessen möchten die Forscherinnen und Forscher die mathematischen Fähigkeiten der Maschinen mit denselben Techniken verbessern, die es KIs wie AlphaGo ermöglicht haben, die weltbesten Spieler bei strategischen Aufgaben wie Brettspielen zu schlagen. Entscheidend ist dabei der Einsatz von »reinforcement learning«, das einer KI beibringt, zu erkennen, welcher Spielzug gut ist. Wenn AlphaGo eine Go-Partie verliert, analysiert das Programm die relevanten Spielzüge und lernt aus seinen Fehlern. Für solche Systeme braucht man jede Menge Trainingsdaten. »Wenn man mit natürlicher Sprache oder Minerva arbeitet, ist das kein Problem; das ganze Internet ist voll Mathematik. Aber man kann damit kein ›reinforcement learning‹ machen«, sagt Wu. Denn die KI kann nicht beurteilen, welcher Rechenschritt »gut« war. Sie müsste erst wissen, welche Schritte zulässig sind und was ein richtiges Ergebnis ist – und dafür muss sie in der Lage sein, Berechnungen zu verifizieren.

Beweisassistenten bieten eventuell eine Lösung. Allerdings gibt es zu diesen nur wenige Daten. »Wir brauchen eine Art Brücke, um von einer Seite zur anderen zu gelangen«, sagt Wu. Vielleicht ist eine KI wie Codex diese Verbindung: Eine KI könnte ein mathematisches Problem zunächst formalisieren, es dann lösen und das Ergebnis anschließend mit einem Beweisassistenten wie Isabelle/HOL überprüfen. Das würde das für das »reinforcement learning« notwendige Feedback liefern, damit die Programme aus ihren Fehlern lernen. Am Ende könnte die KI zu einer beweisbar korrekten Antwort kommen, mit allen gewünschten Zwischenschritten.

KI-Forscher haben noch ehrgeizigere Ziele vor Augen. Denn die Mathematik ist ein perfektes Versuchsfeld, um maschinelle Schlussfolgerungen zu entwickeln. Wenn ein Computer effektiv über Mathematik nachdenken kann, so die Überlegung, sollte er ganz natürlich auch andere Fähigkeiten erwerben: etwa programmieren oder medizinische Diagnosen stellen – und vielleicht lernt er sogar, die widersprüchlichen Details in einer Geschichte über Einhörner aufzudecken.