NZZ, 11.6.26

Beweise aus der Maschine

Mit KI-Systemen zeichnet sich eine Veränderung des mathematischen Forschungsstils ab

Die Mathematik gilt als Domäne des strengen Beweises. Aber eigentlich lässt sie sich ebenso treffend als Reich des Unbewiesenen charakterisieren. Sie lebt von der Kunst des Vermutens. Und im Glücksfall überführt sie die Vermutung in einen Beweis. 

Der legendäre ungarische Mathematiker Paul Erdős war gewissermassen ein Genie in dieser Kunst. Er formulierte über 1000 «Rätsel», von denen es mehr offene als gelöste gibt. Eines lautet tückisch einfach: Wenn man n Punkte auf einer Fläche platziert, maximal wie viele Punktepaare können den gleichen Einheitsabstand haben? 

Es kommt natürlich auf die Anordnung an. Man kann 4 Punkte auf einer Linie anordnen. Dann gibt es 3 Einheitsdistanzen. Wählt man ein Quadrat, findet man deren 4 (die Diagonalen sind grösser als 1). Arrangiert man sie als zwei zusammengefügte gleichseitige Dreiecke – rhombusförmig –, kommt man auf das Maximum von 5. Die Frage lässt sich bis zu 21 Punkten exakt beantworten (57 Einheitsabstände). Dann gibt es nur Abschätzungen. Und das erweist sich als tückisch. Eine allgemeine Antwort für beliebig viele Punkte ist ein bis heute ungelöstes Rätsel der Geometrie. Erdős stellte die Vermutung auf, dass es für sehr grosse Punktezahlen eine besondere Anordnung gibt, die nicht übertroffen werden kann. Während 80 Jahren blieb diese Vermutung unbewiesen. 

Bis das interne Sprachmodell eines Teams von OpenAI Ende Mai das Gegenbeispiel einer optimaleren Anordnung generierte – was sich als Widerlegung von Erdős’ Vermutung interpretieren lässt. Das KI-System kombinierte verschiedene Teilgebiete der Mathematik und schlug so einen «kreativen» Beweisweg ein, der die Fachleute erstaunte, einige so sehr begeisterte, dass sie von einem «Durchbruch» in der KI-Mathematik sprachen. Für den Zahlentheoretiker Arul Shankar zeigt die Arbeit, «dass aktuelle KI-Modelle fähig sind, eigene geniale Ideen zu haben und sie dann erfolgreich umzusetzen».  

***

Ein KI-Modell mit «genialen Ideen»?  - Nun ist gerade bei Hype-Meldungen aus der KI-Industrie Zurückhaltung ratsam. Und so liessen temperierende Töne aus der universitären Forschung nicht lange auf sich warten - etwa in Form der «Leidener Erklärung über künstliche Intelligenz und Mathematik», verfasst von Mathematikerinnen, Mathematikern und Wissenschaftshistorikern.  

Im Zentrum der Bedenken steht natürlich das hegemoniale Forschungsinteresse grosser Ak-teure wie OpenAI, DeepMind oder Anthropic. Haben sie das Wohl des Fachs im Blick? Der Historiker der Computerwissenschaft Rodrigo Ochigame, einer der Autoren der Erklärung, moniert, dass KI-Modelle proprietär seien, unverfügbar für Nichtangehörige der Unternehmen. Und unter dem herrschenden Konkurrenzkampf würden sie zentrale Elemente wie Trainingsdaten, Methoden, Prompts oder Rechenleistung monopolisieren – wodurch sich grundlegende Voraussetzungen wissenschaftlicher Öffentlichkeit verletzt sehen: Nachvollziehbarkeit, Überprüfbarkeit und Transparenz.

Die britische Mathematikerin Ursula Martin, Mitverfasserin der Leidener Erklärung, sekundiert aus methodischer Perspektive. Sie äussert einen naheliegenden Verdacht: «OpenAI hat (..) Glück gehabt (..) Aber man sagt uns nichts über die Misserfolge des Modells».  Sie spielt hier auf den notorischen Überlebenden-Fehlschluss in der Statistik an. Man präsentiert nur den erfolgreichen Lösungsversuch, die gescheiterten erwähnt man nicht. Ohne diese Korrektur droht eine verzerrte Wahrnehmung dessen, was Modelle wirklich leisten. Auf jeden Fall folgt aus «Das Modell findet einen Treffer» nicht «Das Modell versteht Mathematik».

***

Gerade die Fehleranfälligkeit weist auf ein anderes, ein notorisches Problem hin. Das Ergebnis von OpenAI stellt ein Best-Case-Szenario dar. Man sollte freilich auch den Worst Case berücksichtigen, das heisst, die Möglichkeit, dass KI-Systeme «halluzinieren». Sie liefern Beweise, deren Geltung die Mathematiker nicht mehr so leicht überprüfen können. Häufig verstehen ja die Mathematiker selbst die Beweise ihrer Kollegen nicht. Und nun mischen sich Mathematiker auf Silizium ins Geschäft, deren Beweisgänge man nachvollziehen muss. 

Ein falscher Beweis, der schwer zu erkennen ist, verschlingt womöglich Forschungszeit oder dringt sogar in die Literatur ein, wenn Gutachter ihn nicht gründlich prüfen. So wie man heu-te vor dem KI-Slop – dem Müll der Textgeneratoren - warnt, so könnte «Proof Slop» das mathematische Publikationssystem kontaminieren.  

***

Mit Wissenschaft und Mathematik assoziiert man fast instinktiv das Progressive, Innovative – aber auch sie kennen die Trägheit der Tradition. Bewährte Überzeugungen, Methoden, Standards gibt man nicht so ohne weiteres auf. Wenn zum Beispiel der deutsche Zahlentheoretiker Gerd Faltings  sagt, er arbeite mit dem Kugelschreiber und dem Kopf, dann lässt sich dies durchaus als Stimme der Tradition deuten. Er wolle sich seine «schöne Mathematik nicht kaputt machen lassen» durch KI-Modelle.  Die «Schönheit» der Mathematik – das ist die Intuition, Ingeniosität, Imagination des mathematischen Gedankengangs – die «platonische» Einsicht. 

Aber bedroht denn der KI-Beweis wirklich das mathematische Kerngeschäft? Aus histori-scher Perspektive böte sich eine Entwarnung an. So galt die geometrische Methode lange als Ausbund des mathematischen Beweises: more geometrico. Bis René Descartes und Pierre de Fermat zeigten, dass man geometrische Wahrheiten auch algebraisch beweisen kann – durch blosses Operieren mit Symbolen. Das war eine Revolution des Denkstils. Sogar das logische Denken lässt sich algebraisch beschreiben. Das zeigte George Boole im 19. Jahrhundert. Und in dieser Algebraisierung war konzeptuell bereits die Computerisierung der Mathematik an-gelegt. Denn was können die Rechenmaschinen am besten? Logisches Operieren mit Symbo-len. Sie führen uns vor, dass sie uns darin weit überlegen sind. Sie exzellieren more algorith-mico. Exzellieren sie dadurch auch im mathematischen Denken?

***

Ein neuer Forschungsstil zeichnet sich ab. In der Kooperation mit den Sprachmodellen könnte sich der Mathematiker als Problem-Prompter profilieren, als trickreicher Fragetechniker – in der Tradition von Erdős. Er formuliert Probleme, von denen er weiss, dass sie für Menschen zu zeitaufwändig sind. Er skizziert mögliche Beweisrouten, gibt unausgegorene Ideen oder Vermutungen ein. Das KI-System liefert Alternativen, sodass er einen anderen Weg einschlagen kann. Mensch und Maschine bilden eine kreative Schleife. Vielleicht wird es schon bald eine besondere Forschungsrichtung geben: die Interpretation von KI-Beweisen. 

Der Fields-Medaillen-Träger Terence Tao sieht geradezu eine Hochskalierung der mathematischen Arbeit auf «industrielles» Niveau.  Man zerlegt ein Problem in Einzelteile, die von vielen Menschen bearbeitet und dann vom Computer gegengecheckt werden. So liesse sich im Kollektiv ein grosses Problem angehen, das Mathematiker früher nur allein bearbeiten konnten. Wie Gerd Faltings einmal bemerkte: «Schon manches grosse Problem war am Ende dann doch kleiner als gedacht». 

***

Die Entwicklung der grossen Sprachmodelle ist in eine entfesselte Phase getreten. Wohin sie führt, weiss niemand. Zumindest kann man das Ergebnis von OpenAI als eine «gute» Krise interpretieren – in dem Sinn, dass es die Community reizt, über die Fundamente des Fachs nachzudenken. Das war schon vor über einem Jahrhundert so, als die Paradoxien der Mengenlehre die mathematische Architektur in den «klassischen» Grundfesten erzittern liess. Daraus erholte sich die Mathematik prächtig. Sie führte im 20. Jahrhundert zu einem üppigen Gedeihen neuer Disziplinen. 

Warum sollte man nicht Ähnliches vom Einbezug der KI-Modelle für das 21. Jahrhundert erwarten? Der maschinelle Beweis verlangt nach menschlicher Intelligenz  – mehr denn je.