Google AI knapp an IMO-Goldmedaille vorbei: Löst Aufgabe in 19 Sekunden und schockiert Jury, geometrische Fähigkeiten übertreffen menschliche

DeepMinds neuestes mathematisches Modell hat bei der Internationalen Mathematik-Olympiade (IMO) eine Silbermedaille errungen und eine herausragende Leistung gezeigt. Das Modell löste 4 von 6 Aufgaben perfekt und verfehlte die Goldmedaille nur um einen Punkt. Besonders beeindruckend war die Leistung bei Aufgabe 4, wo das Modell in nur 19 Sekunden eine Lösung lieferte. Die Geschwindigkeit und Qualität der Problemlösung erstaunte die menschlichen Prüfer.

AlphaProof

AlphaProof ist ein System, das in der Lage ist, mathematische Sätze in der formalen Sprache Lean zu beweisen. Es kombiniert ein vortrainiertes großes Sprachmodell mit dem AlphaZero-Verstärkungslernalgorithmus.

Um die Einschränkungen formaler Sprachen im maschinellen Lernen aufgrund begrenzter von Menschen geschriebener Daten zu überwinden, überbrückten Forscher die Lücke zwischen natürlicher Sprache und formalen Aussagen durch:

  1. Feinabstimmung des Gemini-Modells, um automatisch natürlichsprachliche Problemstellungen in formale Aussagen zu übersetzen
  2. Erstellung einer großen Bibliothek formalisierter Probleme unterschiedlicher Schwierigkeit

Bei der Problemlösung generiert AlphaProof Lösungskandidaten und beweist oder widerlegt diese, indem es in Lean nach möglichen Beweisschritten sucht.

AlphaGeometry 2

AlphaGeometry 2 ist ein neural-symbolisches Hybridsystem, das von Grund auf mit Geminis Sprachmodell trainiert wurde. Es kann schwierigere Geometrieprobleme lösen als sein Vorgänger, einschließlich solcher, die Objektbewegung, Winkel, Verhältnisse und Entfernungsgleichungen beinhalten.

Wichtige Verbesserungen umfassen:

  1. Training auf synthetischen Daten, die eine Größenordnung größer sind als bei der vorherigen Version
  2. Eine symbolische Engine, die zwei Größenordnungen schneller ist als zuvor
  3. Ein neuartiger Mechanismus zum Wissensaustausch, der fortgeschrittene Kombinationen verschiedener Suchbäume ermöglicht, um komplexere Probleme zu lösen

AlphaGeometry 2 hat beeindruckende Fähigkeiten gezeigt und löst 83% der IMO-Geometrieprobleme der letzten 25 Jahre, verglichen mit 53% für seinen Vorgänger. Bei der diesjährigen IMO löste es Aufgabe 4 in nur 19 Sekunden nach Erhalt der formalisierten Frage.

Die Leistung der KI in der IMO zeigt bedeutende Fortschritte in den mathematischen Argumentationsfähigkeiten und bringt KI näher an menschliches Problemlösungsniveau in fortgeschrittener Mathematik heran.