Google Deepmind hat zwei neue KI-Systeme vorgestellt, die bei der diesjährigen Internationalen Mathematik-Olympiade (IMO) Silber gewonnen haben.
Die Systeme AlphaProof und AlphaGeometry 2 lösten vier der sechs gestellten Aufgaben und erreichten 28 von 42 möglichen Punkten. Das sei ein Schritt in Richtung künstliche allgemeine Intelligenz (AGI) mit fortgeschrittenen mathematischen Fähigkeiten, schreibt Deepmind. Eine Gold-Medaille gab es ab 29 Punkten, erreicht wurde sie von 58 der 609 Teilnehmenden.
AlphaProof kombiniert ein vortrainiertes Sprachmodell mit dem AlphaZero Reinforcement-Learning-Algorithmus, der bereits erfolgreich für Schach, Shogi und Go eingesetzt wurde, um mathematische Aussagen in der formalen Sprache Lean zu beweisen.
Das System trainiert sich selbst, indem es Millionen von mathematischen Problemen unterschiedlichen Schwierigkeitsgrades löst und daraus lernt, indem es in Lean nach möglichen Beweisschritten sucht. Jeder gefundene und verifizierte Beweis wird verwendet, um das Sprachmodell von AlphaProof zu erweitern und seine Fähigkeit zu verbessern, nachfolgende, anspruchsvollere Probleme zu lösen.
AlphaGeometry 2 ist eine deutlich verbesserte Version seines Vorgängers aus dem Januar 2024 und basiert auf einem Gemini-Sprachmodell, das mit einer größeren Menge synthetischer Daten trainiert wurde. Vor der diesjährigen IMO konnte AlphaGeometry 2 laut Google Deepmind bereits 83 Prozent aller historischen IMO-Geometrieprobleme der letzten 25 Jahre lösen.
Die Lösungen der KI-Systeme wurden nach den offiziellen Regeln der IMO von führenden Mathematikern bewertet, darunter Professor Sir Timothy Gowers, selbst Goldmedaillengewinner der IMO und Fields-Medaillengewinner.
"Die Tatsache, dass das Programm eine nicht offensichtliche Konstruktion wie diese hervorbringen kann, ist sehr beeindruckend und geht weit über das hinaus, was ich für den aktuellen Stand der Technik hielt", sagte Gowers.
Für den Einsatz bei der IMO wurden die Aufgaben zunächst manuell in eine formale mathematische Sprache übersetzt. Während die menschlichen Teilnehmer die Aufgaben in zwei 4,5-stündigen Sitzungen bearbeiteten, benötigten die KI-Systeme für eine Aufgabe nur wenige Minuten, für andere bis zu drei Tage.
Logik und LLMs - es ist kompliziert
Google Deepmind sieht in der Entwicklung von KI-Systemen mit fortgeschrittenen mathematischen Fähigkeiten das Potenzial, neue Bereiche in Wissenschaft und Technologie zu erschließen. Mit heutigen generativen KI-Modellen wie LLMs ist dies kaum möglich, da sie keine logischen Fähigkeiten besitzen und zum Teil haarsträubende Fehler machen.
Deepmind plant, in Zukunft weitere technische Details zu AlphaProof zu veröffentlichen und erforscht auch Ansätze für natürlichsprachliche Schlussfolgerungen auf Basis des Gemini-Modells.
Genau diese Kombination entspricht der Aussage von Google-Deepmind-CEO Demis Hassabis aus dem Sommer 2023: "Auf einer höheren Ebene kann man sich Gemini als eine Kombination einiger der Stärken von AlphaGo-Systemen mit den erstaunlichen Sprachfähigkeiten der großen Modelle vorstellen. Wir haben einige neue Innovationen, die sehr interessant sein werden." Bisher hat es allerdings noch keiner dieser Ansätze zur Marktreife geschafft.
Auch OpenAI will multimodalen KI-Modellen logisches Denken beibringen. Unter dem Codenamen "Strawberry" wird eine KI-Technologie mit erweiterten logischen Fähigkeiten entwickelt, die der "Quiet-STaR"-Methode der Stanford-Forscher ähneln soll. Ziel ist es, die Modelle des Unternehmens insbesondere für die autonome Internetsuche und komplexe Planungsaufgaben zu verbessern.
Laut Reuters-Bericht erreichte eine intern getestete OpenAI-KI im MATH-Benchmark für anspruchsvolle mathematische Aufgaben mehr als 90 Prozent. Zum Vergleich: GPT-4 lag bei 53 Prozent, GPT-4o bei 76,6 Prozent. OpenAI soll intern bereits angekündigt haben, an der Schwelle zur KI mit logischen Fähigkeiten zu stehen.
