Deepmind: Google-KI bei Mathematik-Olympiade fast auf Gold-Niveau
Googles KI-Tochter Deepmind arbeitet seit einiger Zeit an Modellen, die mathematische Probleme bearbeiten können. Getestet werden die gern mit den Aufgaben der internationalen Mathematikolympiade(öffnet im neuen Fenster) (IMO). Jährlich treten hier Schülerinnen und Schüler aus über 100 Ländern an, die in zwei viereinhalbstündigen Einheiten insgesamt sechs anspruchsvolle Aufgaben lösen.
Auf die Aufgaben des Jahres 2024 setzte Deepmind zuletzt zwei seiner Modelle an, Alphaproof und ein verbessertes Alphageometry, dessen erste Version bereits Anfang 2024 bei IMO-Aufgaben glänzte . Von den sechs Aufgaben konnten die Modelle, wie ein Blog-Eintrag(öffnet im neuen Fenster) beschreibt, vier korrekt lösen, scheiterten allerdings an den beiden kombinatorischen Aufgaben.
Das hätte für eine Silbermedaille gereicht, zur Goldmedaille fehlte nur ein Punkt. Damit liegt die KI zwar deutlich über dem Durchschnitt, hätte allerdings das Zeitlimit gerissen: Nach Angabe von Deepmind brauchte Alphaproof für eine der Lösungen drei Tage, während die geometrische Aufgabe bereits nach wenigen Minuten gelöst war.
Aufgebohrte Sprachmodelle
Beide Modelle basieren teilweise auf einem Sprachmodell: Es dient dazu, die Aufgaben für das Modell verständlich zu machen. Während es bei Alphageometry mit einer symbolischen Einheit interagiert und in den Lösungsprozess integriert ist, übersetzt es bei Alphaproof in die Beschreibungssprache des formalen Beweisassistenten Lean(öffnet im neuen Fenster) .
Für diese Problembeschreibung erzeugt dann ein auf Alphazero basierendes Modell, als Solver Network bezeichnet, einen Beweisvorschlag, der mittels Lean überprüft wird. Alphazero hatte Deepmind zuvor für das Spiel Go und zum Erzeugen von Algorithmen genutzt.
Was zunächst wie ein Umweg erscheint, macht laut den Entwicklern das Modell erst handhabbar. Ein reines Sprachmodell könne fehlerhafte Zwischenschritte vorschlagen, was oft als Halluzination bezeichnet wird. Da die Lean-Beschreibung maschinell verifiziert werden kann, lassen diese sich wesentlich einfacher identifizieren als bei einem sprachlich formulierten Beweisvorschlag.
Problem: Die Trainingsdaten
Als große Herausforderung bei der Entwicklung von Alphaproof nennt Deepmind, dass unzureichende Trainingsdaten verfügbar gewesen seien. Deshalb habe man zunächst ein spezielles, auf Gemini basierendes Modell trainiert. Das habe aus rund einer Million informell, also sprachlich beschriebenen Problemen rund 100 Millionen in Lean beschriebene Probleme erzeugt. Auf dieser Basis wurde dann Solver Network trainiert.
Bei Deepmind sieht man KI-Modelle für mathematisches Schließen als wichtigen Beitrag für die Wissenschaft: Sie könnten Forscher unterstützen, indem sie neue Ansätze für Beweise liefert. Die richtige Idee ist in der Mathematik oft entscheidend für neue Erkenntnisse, wie beispielsweise eine kürzlich gefundene bessere Abschätzung im Kontext der Riemann-Hypothese(öffnet im neuen Fenster) zeigt.