KI löst jahrzehntealte Mathe-Rätsel – OpenAI veröffentlicht 722 Arbeiten

Was passiert, wenn eine künstliche Intelligenz mathematische Probleme löst, an denen die klügsten Köpfe seit Jahrzehnten scheitern? OpenAI behauptet, dass seinem bislang geheimen KI-Modell genau das gelungen ist – und zwar gleich in Hunderten Fällen. Wie das US-Technologiemagazin The Verge berichtet, hat das Unternehmen 722 mathematische Manuskripte veröffentlicht. Besonders erstaunlich: Der Rechenaufwand pro Ergebnis entsprach laut OpenAI durchschnittlich nur drei Stunden Denkzeit von ChatGPT Pro.

Die Arbeiten verteilen sich auf 372 Gruppen mit verwandten Ergebnissen. Nach Angaben der unabhängigen Beratungsgruppe AGMAI enthalten sie Lösungen für Hunderte bislang offene mathematische Fragen. Bereits im September hatte OpenAI mehr als 100 gelöste Probleme gemeldet. Viele der neuen Beweise lassen sich mit der Programmiersprache Lean automatisch auf logische Fehler überprüfen. Allerdings steht die unabhängige wissenschaftliche Bewertung zahlreicher Ergebnisse noch aus. Ob die KI tatsächlich alle beanspruchten Probleme gelöst hat, müssen Mathematiker erst bestätigen.

OpenAI macht Rechenaufwand und Lösungswege öffentlich

Wie die KI zu ihren mathematischen Ergebnissen gelangte, lässt sich zumindest teilweise nachvollziehen. OpenAI hat dafür ein öffentlich zugängliches GitHub-Repository eingerichtet. Dort sind neben den Manuskripten auch Angaben zum Rechenaufwand und zur Zahl der bearbeiteten Aufgaben hinterlegt. Allerdings verraten die veröffentlichten Daten bislang nicht sämtliche Einzelheiten der Berechnungen.

Zusätzlich stellt das Unternehmen zehn Zusammenfassungen der Lösungswege bereit. Sie sollen Einblicke in die mathematischen Überlegungen des Modells ermöglichen. Offen bleibt, wie viele Versuche für einzelne Ergebnisse nötig waren und welche Probleme die KI trotz ihres hohen Rechenaufwands nicht bewältigen konnte.

Computer überprüfen mathematische Beweise Schritt für Schritt

In der Mathematik reicht es nicht, eine richtige Zahl oder eine plausible Antwort zu finden. Jeder Schritt eines Beweises muss logisch aus den vorherigen Aussagen folgen. Ein einziger Fehler kann eine vermeintliche Lösung zunichtemachen. Deshalb nutzt OpenAI zusätzlich die Programmiersprache Lean, mit der sich mathematische Beweise maschinell überprüfen lassen.

Die Software kontrolliert, ob die Beweisschritte den festgelegten mathematischen Regeln entsprechen. Dafür müssen die Aussagen zunächst in eine präzise Computersprache übertragen werden. Diese sogenannte Formalisierung ist aufwendig, ermöglicht aber eine besonders strenge logische Kontrolle.

Das Verfahren bietet mehrere Vorteile:

Logische Fehler erkennen: Der Computer prüft, ob sämtliche Schritte eines Beweises korrekt aufeinander aufbauen.
Ergebnisse nachvollziehen: Wissenschaftler können formalisierte Beweise unabhängig vom KI-Modell überprüfen.
Überprüfungen wiederholen: Ein einmal formalisierter Beweis lässt sich jederzeit erneut maschinell kontrollieren.
Grenzen erkennen: Die Software bestätigt die formale Korrektheit, bewertet aber nicht automatisch die wissenschaftliche Bedeutung eines Ergebnisses.

Bislang liegen solche maschinenlesbaren Beweise nicht für sämtliche veröffentlichten Arbeiten vor. OpenAI will weitere Formalisierungen ergänzen. Zudem hängt die Aussagekraft der Überprüfung davon ab, ob die ursprünglich gestellte mathematische Frage korrekt in die formale Sprache übertragen wurde.

Mathematiker fordern strengere Regeln für KI-Ergebnisse

Die rasanten Fortschritte haben innerhalb der mathematischen Fachgemeinschaft eine Debatte ausgelöst. Dabei geht es um die Zuverlässigkeit der Ergebnisse, die Offenlegung der verwendeten Methoden und den Umgang mit menschlichen Vorarbeiten. Schließlich greifen KI-Systeme auf mathematisches Wissen zurück, das über Generationen hinweg entstanden ist.

Die unabhängige Advisory Group on Mathematics and Artificial Intelligence hat deshalb Empfehlungen für den wissenschaftlichen Umgang mit KI-generierten Ergebnissen veröffentlicht. Das Gremium fordert transparente Angaben zu den eingesetzten Modellen, den verwendeten Eingaben und den benötigten Rechenressourcen. Auch die Herkunft mathematischer Vorarbeiten soll nachvollziehbar bleiben.

Besonders kritisch beurteilt die Expertengruppe die Vermischung wissenschaftlicher Veröffentlichungen mit Produktwerbung. KI-Unternehmen sollten mathematische Forschungsergebnisse nicht als Werbemittel für ihre Modelle einsetzen. Stattdessen sollen sie ihre Arbeiten möglichst zügig über etablierte wissenschaftliche Kanäle zugänglich machen. So können Fachleute die Beweise prüfen, Fehler aufdecken und die Ergebnisse weiterentwickeln.

OpenAI arbeitet an der Veröffentlichung seines KI-Modells

OpenAI will die mathematischen Arbeiten künftig mit ausführlicheren Erläuterungen und präziseren Quellenangaben versehen. Zudem sollen verbindliche Regeln die Überarbeitung bereits veröffentlichter Beweise erleichtern. Auch wissenschaftlich verwaltete Plattformen kommen dafür infrage. So können Mathematiker die Ergebnisse unabhängig überprüfen, mögliche Fehler korrigieren und auf den Erkenntnissen aufbauen.

Darüber hinaus plant OpenAI die Finanzierung von Workshops, Konferenzen und speziellen Forschungsprogrammen. Mathematiker sollen dort KI-generierte Beweise untersuchen, offene Fragen klären und neue Lösungsansätze diskutieren können.

Parallel arbeitet das Unternehmen an einer öffentlichen Bereitstellung des bislang internen Frontier-Modells. Einen konkreten Termin gibt es noch nicht. Damit bleibt vorerst auch unklar, wie zuverlässig das System bei neuen mathematischen Aufgaben arbeitet, die außerhalb der bisherigen Tests liegen. Unabhängige Wissenschaftler können bereits veröffentlichte Beweise kontrollieren, das zugrunde liegende Modell aber noch nicht selbst unter vergleichbaren Bedingungen erproben.

Kurz zusammengefasst:

KI löst jahrzehntealte Mathe-Rätsel: OpenAI hat 722 mathematische Manuskripte veröffentlicht, die Lösungen für Hunderte bislang ungelöste Probleme enthalten sollen.
Beweise lassen sich automatisch überprüfen: Mithilfe der Programmiersprache Lean können Computer viele der mathematischen Beweise Schritt für Schritt auf logische Fehler kontrollieren.
Wissenschaftliche Bestätigung steht noch aus: Zahlreiche Ergebnisse müssen unabhängig geprüft werden, während das verwendete KI-Modell bislang nicht öffentlich zugänglich ist.

Übrigens: Während KI inzwischen jahrzehntealte Mathe-Rätsel lösen soll, gelang zwei US-Schülerinnen ein außergewöhnlicher Erfolg ganz ohne künstliche Intelligenz: Sie entwickelten zehn neue trigonometrische Beweise für den Satz des Pythagoras, die lange als unmöglich galten – mehr dazu in unserem Artikel.