Elon Musks neue Firma xAI gehört zu den geheimnisumwittertesten Start-ups im Silicon Valley. Im Juli kündigte die Website lediglich an: “Das Ziel von xAI ist es, die wahre Natur des Universums zu verstehen”, darunter die zwölf Köpfe der Gründungsmitarbeiter. Im November dann postete Musk ein paar Screenshots des neuen Chatbots Grok, die zu allerlei Spekulationen führten. Geht man heute auf die Seite, dann erfährt man, dass Grok “eine KI nach dem Vorbild von Per Anhalter durch die Galaxis” sei. Der Bot sei entwickelt worden, “um Fragen mit ein wenig Witz zu beantworten”, und habe “eine rebellische Ader”.

Viele sehen daher die Firma als eine weitere Musk-Peinlichkeit: Ein Bot, der mit gezwungen verkrampftem Humor den User politisch unkorrekt anpöbelt – das macht Musk ja schon persönlich auf seiner sinkenden Plattform X, ehemals Twitter. Aber man verkennt Elon Musk, wenn man nur seine schrille und provokante Persönlichkeit zur Kenntnis nimmt. Er hat ein ernsthaftes Interesse an Mathematik und Naturwissenschaften, und seine Absicht, die künstliche Intelligenz mithilfe von xAI in humane und verantwortungsvolle Bahnen zu lenken, ist wohl ernst gemeint. Das neue Start-up vereinigt einige kluge Köpfe, die dort offenbar mehr entwickeln wollen als einen pöbelnden Chatbot.

Zu ihnen zählen zwei der Mitgründer von xAI: Tony Wu und Christian Szegedy. In einem Edelcafé in Palo Alto erzählen sie ZEIT ONLINE von ihrem Projekt, das auf den ersten Blick vielleicht esoterisch erscheint: Sie wollen die Mathematik “lösen” – das heißt, eine künstliche Intelligenz programmieren, die intellektuell den schlauesten Mathematikern der Welt ebenbürtig oder überlegen ist, so wie Maschinen heute schon in Spielen wie Schach und Go Menschen schlagen. Eine solche formal korrekt denkende KI wäre auch ein wichtiger Schritt, um die Konversation mit den schwatzhaften und halluzinierenden Chatbots von heute, die auch mal Falsches behaupten, auf eine sicherere Grundlage zu stellen.

Noch “beweisen” Sprachmodelle falsche Behauptungen

Laien stellen sich die Arbeit von Mathematikerinnen und Mathematikern womöglich als einen sehr formale und streng den Gesetzen der Logik folgende Tätigkeit vor: Sie stellen neue Behauptungen über die Objekte auf, mit denen sie jonglieren, und beweisen oder widerlegen diese Vermutungen dann unanfechtbar Schritt für Schritt. Das kann manchmal 350 Jahre dauern wie im Fall des Großen Fermatschen Satzes – aber sobald etwas bewiesen ist, kann man sich fest darauf verlassen.

Aber mathematische Bücher und Zeitschriftenartikel sind nicht in puren Formeln verfasst – ein großer Teil ist in ganz gewöhnlicher Sprache geschrieben, nicht jeder kleinste logische Schritt wird ausformuliert. Da kann es durchaus vorkommen, dass ein allgemein akzeptiertes Ergebnis nach Jahren angezweifelt wird. Und manchmal versteht kein Kollege und keine Kollegin, was ein Gelehrter da aufgeschrieben hat.

Deshalb gibt es in den vergangenen Jahren verstärkt Bemühungen, solche Beweise in eine strenge Formelsprache zu übersetzen, die dann von einem Algorithmus auf ihre Korrektheit überprüft werden kann. Ein Netzwerk namens LEAN von Tausenden Mathematikern hat inzwischen große Mengen auch höherer mathematischer Sätze auf diese Weise verifiziert. Sogar der Bonner Mathematiker Peter Scholze, Träger der renommierten Fields-Medaille und unterwegs in recht einsamen Höhen der modernen Mathematik, hat mit den Beweisprüfern zusammengearbeitet (inzwischen sagt er aber in einer E-Mail, er sei “das ganze KI-Zeug leid”).

Aber solche “Proof-Checker” können nur bereits vorhandene Beweise überprüfen, sie kommen nicht selbst auf Ideen, wie man eine Vermutung beweisen könnte. Und da kommen die großen Sprachmodelle ins Spiel: Sie bleiben ja keine Antwort schuldig, und sie lösen auch einfache mathematische Probleme. Beim großen Mathematiktest der ZEIT im Oktober schnitt ChatGPT besser ab als 92 Prozent der Deutschen. Auch einfache Beweise kann der Bot führen. Allerdings “beweist” er auch manchmal falsche Behauptungen, sagt der LEAN-Begründer Leonardo de Moura. Etwa, dass es zwischen zwei ganzen Zahlen immer unendlich viele weitere ganze Zahlen gebe – was wirklich mathematischer Unsinn ist.

Tony Wu und Christian Szegedy haben seit 2015 bei Google an Systemen gearbeitet, die versuchen, Sprachmodellen formale Strenge beizubringen, dass sie sich also an die Fakten halten. Aber sie stießen dort an ihre Grenzen. “Wir haben unsere Vorgesetzten um mehr Ressourcen gebeten”, erzählt Szegedy. “Wir haben keine großen Forderungen gestellt – mehr Rechenkapazität und ein paar zusätzliche Leute.” Auch wenn der Umfang der mathematischen Literatur weitaus geringer ist als die Datenmengen, die große Sprachmodelle aufsaugen, sind doch sehr leistungsstarke Computer nötig, um die Modelle zu bauen. Als ihre Anfragen ignoriert wurden, nahmen sie das Angebot von Elon Musk gerne an.

“Einer meiner Brüder nennt es eine intellektuelle Atombombe”

Ihr System ist heute schon auf schulischem Oberstufen-Niveau, eine Erweiterung bis auf das Level von Mathematikstudierenden halten die beiden für wenig problematisch. Aber von da sind es noch einige Etagen bis zu den abstrakten Strukturen, mit denen sich Mathematikerinnen an der vordersten Forschungsfront beschäftigen. Trotzdem scheut sich Christian Szegedy nicht, eine kühne Prognose abzugeben: Schon im Jahr 2026 würden die Beweismaschinen den besten menschlichen Mathematikern ebenbürtig sein. “Vor ein paar Jahren lag meine Schätzung noch beim Jahr 2029, aber ich werde immer optimistischer”, sagt der aus Ungarn stammende Mathematiker, der seinen Abschluss an der Universität Bonn gemacht hat.

Das wäre natürlich eine größere Kränkung für den menschlichen Geist als die Niederlage in einem Spiel wie Schach oder Go. “Einer meiner Brüder, ein Mathematiker, nennt es eine intellektuelle Atombombe”, sagt Szegedy. Auch Tony Wu sagt: “Selbst die schwersten Probleme der Mathematik, etwa das P=NP-Problem – mit genügend Rechenkapazität sollte das System eine Antwort darauf finden.” Auf einen Zeithorizont für die Lösung dieser Jahrtausendprobleme der Mathematik will er sich nicht festlegen, aber auf jeden Fall würden die neuen Beweis-KI-Systeme “sehr gute Forschungsassistenten” sein.

Diese mathematischen Probleme sind vielleicht nicht die Fragen, die die meisten mit der modernen KI verbinden – aber ein Algorithmus, der umgangssprachlich gestellte mathematische Fragen formal präzise beantworten kann, hätte auch Anwendungen in der Praxis. Da ist zum Beispiel die Verifizierung von Software: Große Programme ähneln heute oft barocken Kathedralen, zusammengeschustert aus recyceltem Code der Vergangenheit. Eine formal denkende KI könnte diese Code-Gebäude auf ihre Verlässlichkeit überprüfen und Schwachstellen, aber auch eingeschmuggelten Schadcode identifizieren. Sicherheitsrelevante Systeme ließen sich besser vor Eindringlingen schützen. Und ganz allgemein: Eine KI, die nicht nur aufgrund statistischer Regeln daherschwätzt, sondern überprüfbare und verlässliche Informationen produziert, wäre für uns alle ein Gewinn.

Noch ist xAI mit weniger als 20 Mitarbeitern eine winzige Firma im Vergleich zu OpenAI oder Riesen wie Google und Microsoft, und ob sie wirklich einen Beitrag zur Entwicklung verantwortungsvoller KI leisten kann, muss sich noch zeigen. Vor allem, weil der Beitrag nicht nur positiv für uns ausfallen kann. “KI ist formbarer, als wir denken”, sagt Christian Szegedy, “und wenn wir die richtige KI entwickeln, kann das ein großer Segen für die Menschheit sein. Aber wir können es natürlich auch vermasseln – und das wäre eine große Katastrophe.”