OpenAI hat diese Woche Hunderte angebliche Lösungen für schwierige mathematische Probleme veröffentlicht, um die Fähigkeit seiner Modelle im Umgang mit anspruchsvollen Aufgaben zu demonstrieren. Die Veröffentlichung entsprach jedoch nicht vollständig den Leitlinien einer beratenden Gruppe mathematischer Forscher und hat damit die grundlegende Frage erneut aufgeworfen: Reicht es aus, wenn Modelle eine Lösung erzeugen, die sich formal in Code ausdrücken lässt, oder muss sie für Mathematiker verständlich und überprüfbar sein?
Die Gruppe Advisory Group on Mathematics and Artificial Intelligence (AGMAI) umfasst neun führende Forscher und wird vom Institute for Advanced Study an der Princeton University beherbergt. Ende September hatte die Gruppe Leitlinien für Labore veröffentlicht, die fortgeschrittene Modelle zur Lösung mathematischer Probleme entwickeln.
Teilweise Einhaltung der Leitlinien der Forscher
AGMAI wies darauf hin, dass die Beurteilung, inwieweit ihre Empfehlungen eingehalten werden, letztlich der mathematischen Gemeinschaft obliegt. Zu ihren wichtigsten Empfehlungen gehört, fortgeschrittene mathematische Probleme nicht mehr an kommerziell proprietären Modellen zu testen. OpenAI erklärte hingegen ausdrücklich, dass es offene Forschungsprobleme zur Bewertung seiner eigenen Modelle verwendet.
OpenAI befolgte einige der Grundsätze, etwa die schnelle Veröffentlichung der Ergebnisse und die Bereitstellung von Informationen darüber, wie die Modelle zu ihren Schlussfolgerungen gelangten. Allerdings enthielten nur 10 von 719 Manuskripten die Denkketten des Modells. Zudem wurden 42 % der veröffentlichten Beweise nicht formalisiert.
Die Gruppe ist der Ansicht, dass Beweise, die für Menschen schwer verständlich sind, in eine formale Darstellung überführt werden sollten. Zugleich betonte sie die Verantwortung des Labors dafür, sicherzustellen, dass auf die Veröffentlichung der Ergebnisse ein menschliches Verständnis folgt, und schlug vor, Mathematiker zu finanzieren, die dabei helfen, diese Ergebnisse wissenschaftlich tatsächlich sinnvoll zu machen.
Lücke zwischen natürlicher Sprache und Lean-Code
Modelle beginnen gewöhnlich damit, eine Erklärung in natürlicher Sprache zu erstellen, und versuchen anschließend, sie in Lean zu übertragen. Dabei handelt es sich um eine Programmiersprache, deren Compiler die Konsistenz eines Beweises in einer ausführbaren Form bestätigen kann. Die automatische Übertragung kann jedoch den Inhalt des Beweises verändern oder eine Diskrepanz zwischen dem Gesagten der Erklärung und dem von dem Code Bewiesenen schaffen.
Eine von Mathematikern der University of Cambridge und des King’s College London veröffentlichte Studie dokumentierte mindestens zwei Unterschiede zwischen einem Beweis in natürlicher Sprache und dem mit einer von OpenAI vorgelegten Lösung verbundenen Lean-Code für ein Problem, das aus den Navier-Stokes-Gleichungen zum Verhalten komplexer Fluide abgeleitet war. Diese Unterschiede beweisen nicht zwangsläufig, dass eine der beiden Lösungen falsch ist, wecken jedoch Zweifel daran, Modelle ohne menschliches Eingreifen die formale Ausarbeitung ihrer Lösungen übernehmen zu lassen.
AGMAI forderte außerdem maschinenlesbare Metadaten, die den Textbeweis mit der formalen Version verknüpfen. OpenAI stellte solche Metadaten in diesen Veröffentlichungen nicht bereit. Die Autoren der unter dem Namen „lost in translation“ bekannten Studie kamen zu dem Schluss, dass Textbeweise und automatisch in Lean übertragene Beweise grundsätzlich nicht ohne Peer-Review und eine Prüfung akzeptiert werden sollten, die der Prüfung anderer Beweise gleichwertig ist.
Warum ist diese Nachricht wichtig?
Das Problem besteht nicht nur darin nachzuweisen, dass der Code erfolgreich kompiliert wird, sondern auch darin nachzuweisen, dass der Code tatsächlich die mathematische Idee repräsentiert, die der Text erklärt. In der traditionellen Forschung tragen Wissenschaftler die Verantwortung für ihre Ergebnisse und diskutieren sie in Veröffentlichungen, Vorträgen und Seminaren. Dieser Prozess hilft dabei, Fehler zu entdecken und wiederverwendbare Methoden zu verstehen.
Wenn Modelle hingegen eine Lösung für ein schwieriges Problem erzeugen, ist dieses menschliche Verständnis zum Zeitpunkt der Veröffentlichung möglicherweise nicht vorhanden. Daher wirken die aktuellen Ergebnisse von OpenAI eher wie der Beginn eines wissenschaftlichen Überprüfungsprozesses als wie das Ende des Problems. Die menschliche Prüfung sowie die Verknüpfung der textlichen und formalen Ausgaben bleiben Voraussetzungen, bevor diese Beweise innerhalb der mathematischen Gemeinschaft anerkannt werden können.