Die neueste Studie von Google DeepMind ist gerade in der Zeitschrift Nature erschienen und enthüllt das stärkste mathematische Modell für den Internationalen Mathematik-Olympiade (IMO).
DeepMinds AlphaProof hat bei der IMO eine Silbermedaille erzielt, die nahe an der Goldmedaille liegt. Es kombiniert die Intuition großer Modelle, Reinforcement Learning und formalisierte Beweise in Lean, um mehrere schwierige Aufgaben zu lösen. Obwohl es noch Einschränkungen in Bezug auf Geschwindigkeit, Generalisierung und Aufgabeverständnis hat, hat es eine neue Phase der Zusammenarbeit zwischen menschlichen Mathematikern und KI eröffnet.
Jedes Sommer treffen junge Mathematikgenies aus der ganzen Welt zusammen, um an der Internationalen Mathematikolympiade (IMO), der sogenannten "Fußball-Weltmeisterschaft der Mathematik", teilzunehmen.
Bei der Konkurrenz müssen 6 Aufgaben in zwei Tagen gelöst werden. Jede Aufgabe ist mit maximal 7 Punkten bewertbar, was einen Gesamtwert von 42 Punkten ergibt. Die Schwierigkeit ist extrem hoch, und nur weniger als 1 % der Teilnehmer können alle Aufgaben richtig lösen.
Die horizontale Achse zeigt die Punktzahl (maximal 7 Punkte), die vertikale Achse die Anzahl der Teilnehmer.
In den letzten Jahren wird die IMO auch als eine der ultimativen Herausforderungen im Bereich KI angesehen und ist eine ideale Bühne, um die fortschrittlichen mathematischen Schlussfolgerungsfähigkeiten von KI zu testen.
Im Jahr 2024 ließ das Google DeepMind-Team einen besonderen "Teilnehmer" an der IMO teilnehmen - ein KI-System namens AlphaProof.
Es erreichte eine beeindruckende Punktzahl von 28 Punkten und fehlte die Goldmedaille nur um einen Punkt, was der Silbermedaille entspricht.
Dies ist das erste Mal, dass ein KI-System in einer Spitzenmeisterschaft wie der IMO eine Medaille-entsprechende Leistung erzielt hat, was ein neues Level der Fähigkeit von Maschinen bei der Lösung mathematischer Rätsel markiert.
AlphaProof: Der KI-Experte für mathematische Problemstellungen tritt auf die Bühne
AlphaProof ist ein neu entwickeltes "KI-System für mathematische Problemstellungen" von DeepMind, das speziell für das Beweisen komplexer mathematischer Sätze entwickelt wurde.
Einfach ausgedrückt, wenn man mathematische Probleme als "Labyrinthe" ansieht, die zu bewältigen sind, ist AlphaProof ein selbstgelehrter KI-Experte für das Lösen von Problemen.
Im Gegensatz zu Modellen wie ChatGPT, die rein in natürlicher Sprache "denken", geht AlphaProof einen einzigartigen Weg: Es führt Schlussfolgerungen in einer formalisierbaren Sprache durch, die von Computern verifiziert werden kann, um sicherzustellen, dass jeder Schritt der Ableitung streng korrekt ist und keine fehlerhaften "Einsichten" auftreten.
AlphaProof verwendet die in der Mathematik weit verbreitete formalisierte Beweissprache Lean, um Beweise zu schreiben.
Beispiel für die Lean-Sprache
Die Syntax von Lean ähnelt einer Kombination aus Mathematik und Programmiersprachen und ermöglicht es, dass jeder Schritt der Schlussfolgerung des KI-Ausgangs automatisch überprüft und verifiziert wird, um Fehler zu vermeiden, die bei herkömmlichen Sprachmodellen auftreten können.
Die Antworten, die AlphaProof liefert, basieren nicht auf menschlichen Begründungen, sondern auf einem strengen Beweis, der Zeile für Zeile von einem Computer überprüft wurde.
Diese Methode, die Denkweise der KI in eine maschinell überprüfbaren Form zu "verfestigen", sorgt dafür, dass AlphaProof auch bei den schwierigsten Aufgaben keine Glückseffekte hat.
Das technische Geheimnis: Die Verbindung von großen Modellen und Reinforcement Learning
Das Kerngeheimnis des Erfolgs von AlphaProof liegt in der geschickten Kombination der "klugen Intuition" eines vortrainierten großen Sprachmodells und des "harten Trainings" des AlphaZero-Reinforcement-Learning-Algorithmus.
Sprachmodelle lernen gut von riesigen Datenmengen die Erfahrungen und Muster menschlicher Problemlösungen.
Reinforcement Learning hingegen ermöglicht es der KI, durch ständiges Ausprobieren und Lernen von Fehlern ihre Strategien zu verbessern, ähnlich wie ein Kind, das schließlich lernt, Fahrrad zu fahren.
Das DeepMind-Team hat zunächst mit einem großen Modell die "Wissensbasis" für AlphaProof geschaffen und es dann in einer simulierten mathematischen Umgebung wiederholt trainiert, um selbst Lösungsstrategien zu finden.
Die Forscher haben zunächst fast eine Million mathematische Aufgaben (aus verschiedenen Bereichen und Schwierigkeitsgraden) gesammelt und mit Googles neuestem Gemini diese in natürlicher Sprache beschriebenen Aufgaben automatisch in formalisierte Lean-Code-Ausdrücke übersetzt.
Dieser Prozess entspricht der Schaffung eines bisher nie dagewesenen Aufgabenbanks für AlphaProof - das Team hat insgesamt etwa 80 Millionen formalisierte mathematische Sätze erhalten, die die KI zum Beweisen üben kann.
Nachdem AlphaProof diese "Meer von Aufgaben" hatte, wurde es zunächst durch überwachtes Lernen feinjustiert, um die grundlegenden Beweistechniken in Lean zu erlernen.
Dann trat es in die Phase des Reinforcement Learnings ein: Ähnlich wie AlphaGo beim Schach spielt, trainiert AlphaProof in der Lean-Beweisumgebung gegen sich selbst.
Wenn AlphaProof einen korrekten Beweis für eine Aufgabe findet und dieser verifiziert wird, wird das Modell sofort mit diesem erfolgreichen Fall optimiert, um in Zukunft effizienter auch schwierigere neue Aufgaben zu lösen.
Dieser Lernzyklus wird fortgesetzt, und AlphaProof verbessert sich ständig bei der Bewährung von Millionen von Aufgaben und erlernt schließlich die Schlüsselfertigkeiten für schwierige Aufgaben.
AlphaProof sucht nicht blindlings nach Beweisen. Es verwendet eine Strategie ähnlich der Monte-Carlo-Baumsuche in Schach-KI, um komplexe Probleme in Teilziele aufzuteilen und diese nacheinander zu lösen, und passt die Suchrichtung flexibel an.
In einigen Fällen kann AlphaProof in scheinbar unendlichen Ableitungen den richtigen Schritt machen und zeigt eine "Einsicht", die einem menschlichen Mathematiker ähnelt.
Dies ist sowohl der Intuition des großen Modells als auch der umfassenden Suchfähigkeit des Reinforcement Learnings zu verdanken - die Kombination beider macht AlphaProof besser als alle bisherigen KI-Systeme darin, in komplexen mathematischen Labyrinthen den Weg zu finden.
Silbermedaille bei der Olympiade: Ein Meilenstein für die KI in der Problemlösung
DeepMinds AlphaProof und AlphaGeometry 2 zusammen haben 4 von 6 Aufgaben bei der IMO 2024 gelöst und eine Punktzahl von 28 Punkten (von maximal 42 Punkten) erreicht, was der Leistung eines Silbermedaillengebers entspricht.
Diese Punktzahl fehlte der Goldmedaille nur um einen Punkt (29 Punkte) und ist somit fast an der Goldgrenze angelangt.
Von den gelösten Aufgaben hat AlphaProof 3 alleine gelöst (darunter 2 algebraische Aufgaben und 1 zahlentheoretische Aufgabe), darunter auch die schwierigste Aufgabe 6 der gesamten Konkurrenz - nur 5 von über 600 Spitzenstudenten konnten diese Aufgabe mit vollem Punktesatz lösen.
Die verbleibende geometrische Aufgabe wurde von dem speziell für Geometrie entwickelten Modell AlphaGeometry 2 gelöst, während zwei kombinatorische Aufgaben aufgrund der Schwierigkeit der Formalisierung und des Suchraums nicht gelöst werden konnten.
Schließlich erreichte dieses KI-System volle Punktzahl für 4 Aufgaben (die anderen 2 Aufgaben wurden mit 0 Punkten bewertet), was genau am oberen Ende des Silberbereichs liegt.
Es ist zu beachten, dass nur weniger als 10 % der menschlichen Teilnehmer eine Goldmedaille erhalten, und in diesem Jahr haben 58 Teilnehmer mindestens 29 Punkte erreicht.
Die Silbermedaille von AlphaProof ist vergleichbar mit der Leistung eines international angesehenen, jahrelang trainierten Highschool-Genies.
Dieses Ergebnis hat viele Experten beeindruckt: Der bekannte Mathematiker und Fields-Medaille-Träger Timothy Gowers sagte, dass einige der geschickten Konstruktionen, die AlphaProof liefert, "weit über das hinausgehen, was ich bisher für KI möglich hielt".
Die Leistung von AlphaProof bei der IMO hat einen Meilenstein darstellt.
Es ist das erste Mal, dass eine KI in einer so schwierigen mathematischen Konkurrenz die Leistung eines menschlichen Medaillengebers erreicht hat, was zeigt, dass die mathematischen Schlussfolgerungsfähigkeiten von KI einen großen Sprung gemacht haben.
In der Vergangenheit hatten große Modelle Schwierigkeiten, auch wenn sie eine riesige Menge an Lehrbüchern und Theoremen kannten, Olympiade-Aufgaben vollständig zu lösen, geschweige denn strenge Beweise zu liefern.
AlphaProof hingegen hat durch formalisierte Beweise und Reinforcement Learning die KI tatsächlich in die Lage versetzt, offene mathematische Rätsel zu lösen.
Die Tatsache, dass es die schwierigsten Aufgaben der IMO bewältigen konnte, gibt Hoffnung: Vielleicht hat die KI in Zukunft das Potenzial, menschlichen Mathematikern bei der Lösung ungelöster mathematischer Vermutungen zu helfen.
Einschränkungen und Zukunft: Der Aufstieg der KI-Mathematiker
Obwohl AlphaProof beeindruckend ist, hat es immer noch viele Einschränkungen.
Erstens ist die Effizienz bei der Problemlösung ein Problem.
Menschliche Teilnehmer müssen 3 Aufgaben in 4,5 Stunden lösen, während AlphaProof, obwohl es schließlich die Lösungen für 3 Aufgaben fand, fast 3 Tage benötigte.
Dies zeigt, dass es noch viel Raum für Verbesserungen bei der Suchgeschwindigkeit und der Berechnungsressourcen der aktuellen KI-Beweismethoden gibt.
Zweitens ist AlphaProof nicht allmächtig, und die zwei kombinatorischen Aufgaben, die es nicht lösen konnte, spiegeln wider, dass bestimmte Arten von Problemen für die KI immer noch schwierig sind.
Diese Aufgaben erfordern oft hochgradig unstrukturierte kreative Denkweise, die über das hinausgeht, was AlphaProof aus dem Training "gesehen" hat.
Daher ist es eine wichtige Herausforderung, die KI stärker zu verallgemeinern und anpassungsfähig zu machen, um neuartige, bisher nicht bekannte Probleme zu bewältigen.
Drittens muss AlphaProof derzeit von Menschen die Aufgaben in die formalisierte Lean-Sprache übersetzt werden, da es selbst natürliche Sprache nicht versteht.
Dies bedeutet, dass es keine Aufgaben selbst lesen kann und auch nicht in der Lage ist, wie ein menschlicher Mathematiker neue Probleme zu stellen oder zu beurteilen, welche Probleme sich lohnen, erforscht zu werden.
Wie Yanghui He vom London Institute of Mathematical Sciences feststellte, kann AlphaProof ein nützliches Werkzeug für Mathematiker bei der Beweisführung sein, aber es kann noch nicht den Menschen ersetzen, Forschungsthemen zu entdecken und auszuwählen.
Yanghui He
Angesichts dieser Einschränkungen hat das DeepMind-Team erklärt, dass es weiterhin verschiedene Wege erkunden wird, um die mathematischen Schlussfolgerungsfähigkeiten der KI zu verbessern.
Einer der zukünftigen Forschungsrichtungen ist, die KI von der manuellen Übersetzung unabhängig zu machen, sodass sie direkt mathematische Aufgaben in natürlicher Sprache verstehen und formalisierte Beweise liefern kann.
Zusätzlich müssen möglicherweise für verschiedene Arten von mathematischen Problemen (z. B. Kombinatorik oder Geometrie) spezialisiertere Strategien eingeführt werden, wie die Integration von symbolischer Berechnung, Wissensbanken oder domänenspezifischen Modellen, um die Problemlösungskapazität der KI insgesamt zu verbessern.
Einige Forscher stellen sich auch vor, dass Mathematiker in Zukunft mit einem solchen KI-Beweisassistenten zusammenarbeiten können:
Die KI kann schnell menschliche Vermutungen und kleine Lemmata verifizieren und sogar mutige Ideen ausprobieren, um langjährig ungelöste Probleme zu lösen.
Die Menschen können sich dann auf das Stellen sinnvoller Probleme und die Entwicklung von Gesamtbeweisvorstellungen konzentrieren.
Es ist vorhersehbar, dass mit der ständigen Verbesserung von Systemen wie AlphaProof eine neue Ära der Zusammenarbeit zwischen Menschen und Maschinen bei der Erforschung der mathematischen Frontiers beginnt.
Die formalisierte Schlussfolgerungsfähigkeit von AlphaProof hat auch Bedeutung für die Sicherheit und Zuverlässigkeit von KI.
Jeder Schritt der Schlussfolgerung, den es liefert, ist nachvollziehbar und verifizierbar, und dieser "strenge Beweisstil" könnte möglicherweise in zukünftigen großen Modellen genutzt werden, um abwegige Vermutungen bei der Beantwortung offener Fragen zu reduzieren.
Je stärker die KI wird, desto mehr möchten wir, dass