OpenAI löst zehn mathematische Probleme: KI greift nach den Sternen
Als Mathematiker rund um die Welt am Samstag, dem 1. August, in die Foren und Substacks ihres Vertrauens blickten, gerieten einige von ihnen in nicht unbeträchtliche Erregung. Denn an diesem Tag verkündete das KI-Unternehmen Open AI, Urheber von ChatGPT, auf seiner Website Fortschritte oder gar Lösungen für nicht weniger als zehn bislang offenen mathematischen Problemen. Es waren nicht irgendwelche Knobeleien. Mindestens zwei der zehn Themen sind für die mathematische Forschung von erheblicher Bedeutung: Die Frage, ob es sogenannte nicht-sofische Gruppen gibt, beschäftigt die Fachwelt seit 1999, und wie schnell die Dichte, mit der sich hochdimensionale Kugeln allerhöchstens packen lassen, mit steigender Dimension abnimmt, dazu wurde seit 1978 kein substantieller Fortschritt mehr erzielt. Letztere Frage ist potentiell auch von praktischem Belang, da hochdimensionale Kugelpackungen mit Fragen der Codierung von Nachrichten auf verrauschten Kanälen in Zusammenhang gebracht werden können. F.A.Z.-Artikel häufiger in Ihren Suchergebnissen sehen F.A.Z. bei Google bevorzugen Wettbewerb der Beweismaschinen Nun hat also eine KI in diesen und acht anderen Fragen Lösungen oder substantielle Fortschritte erzielt, und ihre Lösungen wurden laut Open AI durch eine Software namens „Lean“ auf Korrektheit überprüft, wovon sich jeder Interessierte anhand der auf der Plattform Github hinterlegten Daten überzeugen könne. Dabei ist es kaum zwei Wochen her, dass ein Mitarbeiter der Firma Anthropic, gegenwärtig Open AIs schärfster Konkurrent, mittels ihres neusten öffentlich zugänglichen KI-Modells Claude Fable 5, ein Gegenbeispiel für die ebenfalls sehr prominente Jacobi-Vermutung vorlegte. Für diese waren schon mehrfach Beweise vorgelegt worden, die sich aber alle als fehlerhaft erwiesen hatten. Der Gedanke liegt nahe, dass Open AI mit seinem neusten, noch unveröffentlichten Modell namens „Astra“ (lateinisch für „Sterne“) nun publikumswirksam gleichziehen will, zumal beide Unternehmen im Moment durch preisgünstige chinesische KI-Modelle unter Druck stehen. In diesem Zusammenhang ist vielleicht der Hinweis des Unternehmens zu sehen, dass der Token-Verbrauch zur Lösung aller zehn Probleme einen zahlenden Kunden von Open AI gerade mal zweitausend Dollar gekostet hätte. Auch wenn unsere Token teurer sind als die chinesischen, könnte Open AI damit sagen wollen: Schaut, was man mit ihnen machen kann! Was Maschinen beweisen, soll nicht Menschen zugerechnet werden Doch jenseits aller PR-Manöver vertieft diese neueste Entwicklung die Sinnkrise, in welche die Künstliche Intelligenz die Mathematiker nun zu stürzen droht. Denn es stellt sich die Frage, wem solche Leistungen zugeschrieben werden sollen. Erst Anfang Juni – die ersten KI-Lösungen mathematischer Probleme auf Forschungsniveau waren in den Wochen zuvor bekannt geworden – wurde die „Leiden Declaration on Artificial Intelligence and Mathematics“ veröffentlicht. Rund 3400 Mathematiker haben sie bislang unterzeichnet. Sie fordern unter anderem, nur Menschen sollten für mathematische Leistungen Anerkennung bekommen dürfen und Verantwortung übernehmen müssen. In seiner Verlautbarung vom 1. August stellt Open AI den ersten Teil dieses Postulats nun offen infrage: „Menschliche Urheberschaft für einen vollständig von einem KI-System generierten Beweis zu beanspruchen, würde sowohl den Beitrag des Systems als auch das Wesen genuin menschlicher geistiger Arbeit falsch darstellen.“ Die Ehre geht dem Menschen verloren, die Verantwortung bleibt Dagegen ließe sich einwenden, dass die KI-Systeme ja auf menschlichen Leistungen aufbauen, die sie in der veröffentlichten Literatur und anderen Trainingsdaten finden, um dann Verbindungen zwischen ihnen herzustellen. Im Fall der Frage nach der Existenz nicht-sofischer Gruppen etwa, beruhte laut einer Wortmeldung des Gruppentheoretikers Francesco Fournier-Facio von der Universität Cambridge die Lösung des KI-Systems Astra wesentlich auf zwei Arbeiten des ungarischen Mathematikers Gábor Kun von 2016 und 2019, letztere zusammen mit seinem Dresdener Kollegen Andreas Thom. Nur: Menschliche Mathematiker tun oft dasselbe und nennen dann ihre Quellen im Literaturverzeichnis, nicht in der Autorenzeile. Andererseits werden menschliche Mathematiker von der KI nicht im selben Maße ihrer Verantwortung enthoben, wie ihrer Entdeckerehre. Auch dazu hält dieser für das Thema Mathematik und KI so ereignisreiche Sommer Anschauungsmaterial bereit: Am 25. Juli hatte ein Mathematiker namens Ramana Kumar die mit KI-Unterstützung erzielte Widerlegung eines sehr berühmten Theorems, der Collatz-Vermutung, zusammen mit einer Verifikation durch Lean auf einer öffentlich einsehbaren Datenbank hinterlegt. Drei Tage später stellte sich heraus: Die Widerlegung war falsch, was Lean aufgrund eines Programmierfehlers nicht bemerkt hatte. Dafür konnte Kumar nichts, aber wäre er angesichts der Prominenz des Problems der Versuchung erlegen, seinen angeblichen Beweis an die große Glocke zu hängen, hätte wohl vor allem seine Reputation Schaden genommen. Der Fehler in Lean wurde noch am selben Tag behoben. Doch die Möglichkeit, es könne noch andere geben und einer davon einen der zehn nun erzielten Fortschritte fälschlicherweise verifiziert haben, ist erst dann völlig ausgeräumt, wenn menschliche Mathematiker jeden Schritt der von Astra generierten Beweise nachvollzogen haben. Auch von daher kann von einer Gefährdung von Arbeitsplätzen für Mathematiker durch die KI bis auf Weiteres nicht die Rede sein, auch wenn das trickreiche Ersinnen eleganter Beweisen für wichtige oder interessante Theoreme vielleicht wirklich bald nicht mehr zu ihrem Tätigkeitsprofil gehört. Das mögen manche Mathematiker bedauern – aber insoweit ihre Vorfahren Spaß an geschicktem Reduzieren komplexer Berechnungen auf Operationen hatten, die sich mit Rechenschieber und Logarithmentafeln durchführen lassen, so wurden denen dieses Vergnügen ja auch irgendwann genommen. Und im schöpferischen Entwickeln neuer, potentiell fruchtbarer Konzepte, über die sich erst etwas vermuten lässt, was dann zu beweisen wäre, darin sind die KI-Systeme bislang überhaupt noch nicht auffällig geworden.