AlphaGeometry: Ein KI-System für Geometrie auf Olympiade-Niveau

 (deepmind.google)
1 Punkte von GN⁺ 2024-01-18 | 1 Kommentare | Auf WhatsApp teilen
  • Während die Internationale Mathematik-Olympiade zum Prüfstein für mathematisches Schlussfolgern von KI geworden ist, löste AlphaGeometry 25 von 30 Geometrieaufgaben innerhalb des Zeitlimits und kam damit nahe an den Durchschnitt menschlicher Goldmedaillengewinner von 25,9 Aufgaben heran
  • Der Kern ist die Kombination eines neuronalen Sprachmodells mit einer regelbasierten symbolischen Inferenz-Engine, die intuitive Konstruktionsvorschläge und formallogische Verifikation in einer Schleife verarbeitet
  • 100 Millionen einzigartige synthetische Beispiele, die ohne menschliche Demonstrationen erzeugt wurden, reduzierten den Trainingsengpass; 9 Millionen davon enthielten Hilfskonstruktionen, die für Beweise nötig sind
  • Alle Olympiade-Lösungen wurden per Computer verifiziert, und Evan Chen bewertete die Ausgaben als maschinell überprüfbar, zugleich aber menschenlesbar und den klassischen Geometrieregeln folgend, die auch Schüler verwenden
  • Da bei einer IMO-Runde von 6 Aufgaben meist nur 2 Geometrie sind, ist der Anwendungsbereich begrenzt; dennoch ist es das erste KI-Modell, das allein mit seiner Geometrieleistung die Bronze-Medaillen-Grenze der IMO 2000 und 2015 überschreiten kann

Ergebnisse im IMO-Geometrie-Benchmark

  • Das in Nature veröffentlichte AlphaGeometry löst komplexe Geometrieprobleme auf einem Niveau, das dem menschlicher Olympiade-Goldmedaillengewinner nahekommt
  • Der Benchmark besteht aus 30 Geometrieaufgaben des IMO-AG-30, ausgewählt aus den Olympiaden von 2000 bis 2022
    • AlphaGeometry: 25 Aufgaben innerhalb des Zeitlimits gelöst
    • Bester bisheriger Ansatz, Wu’s method: 10 Aufgaben gelöst
    • Durchschnitt menschlicher Goldmedaillengewinner: 25,9 Aufgaben gelöst
  • Google DeepMind hat den AlphaGeometry-Code und das Modell als Open Source veröffentlicht

Aufbau des neuro-symbolischen Systems

  • AlphaGeometry ist ein neuro-symbolisches System, in dem ein neuronales Sprachmodell und eine symbolische Inferenz-Engine gemeinsam Beweise für komplexe geometrische Sätze finden
  • Das Sprachmodell identifiziert aus Daten schnell allgemeine Muster und Beziehungen und sagt Konstruktionen voraus, die wahrscheinlich nützlich sind
    • Allerdings kann es bei strengem Schlussfolgern oder der Erklärung von Entscheidungen Schwächen haben
  • Die symbolische Inferenz-Engine gelangt anhand formaler Logik und klarer Regeln zu Schlussfolgerungen
    • Sie ist erklärbar und rational, kann aber beim alleinigen Bearbeiten großer Probleme langsam und wenig flexibel sein
  • Werden beide Komponenten zusammen eingesetzt, schlägt das Sprachmodell neue Hilfskonstruktionen wie Punkte, Geraden und Kreise vor, und die Inferenz-Engine leitet darauf aufbauend zusätzliche Schlussfolgerungen über die Figur ab

Lösungsschleife zum Finden von Hilfskonstruktionen

  • Geometrieaufgaben auf Olympiade-Niveau lassen sich oft nicht direkt mit der gegebenen Figur lösen; stattdessen müssen neue geometrische Elemente hinzugefügt werden, die für die Lösung nötig sind
  • Der Lösungsprozess von AlphaGeometry arbeitet abwechselnd mit symbolischer Inferenz und Vorschlägen des Sprachmodells
    • Aus der gegebenen Figur und den Voraussetzungen des Satzes leitet die symbolische Inferenz-Engine neue Aussagen ab
    • Wenn sie keine Lösung findet oder keine neuen Aussagen mehr erzeugen kann, fügt das Sprachmodell eine Hilfskonstruktion hinzu, die wahrscheinlich nützlich ist
    • Die hinzugefügte Konstruktion eröffnet der Inferenz-Engine neue Wege, und dieser Prozess wird wiederholt, bis die Lösung gefunden ist
  • Bei Aufgabe 3 der Internationalen Mathematik-Olympiade 2015 bestand die von AlphaGeometry erzeugte Lösung aus 109 logischen Schritten

Erzeugung von 100 Millionen synthetischen Datenpunkten

  • Geometrie basiert auf dem Verständnis von Raum, Distanz, Form und relativer Position und ist grundlegend für viele Bereiche wie Kunst, Architektur und Ingenieurwesen
  • Der Ansatz von AlphaGeometry zur Erzeugung synthetischer Daten bildet im großen Maßstab nach, wie Menschen eine Figur betrachten und mit vorhandenem Wissen neue geometrische Eigenschaften und Beziehungen entdecken
  • Das System erzeugte mit hochgradig parallelisiertem Computing 1 Milliarde zufällige Figuren
    • Für jede Figur wurden alle Beziehungen zwischen Punkten und Geraden gründlich abgeleitet
    • Alle in der Figur enthaltenen Beweise wurden gefunden
    • Es wurde rückwärts verfolgt, welche zusätzlichen Konstruktionen nötig sind, um zu diesen Beweisen zu gelangen
  • Dieser Prozess wird symbolic deduction and traceback genannt
  • Der riesige Datenpool wurde so gefiltert, dass ähnliche Beispiele ausgeschlossen wurden; übrig blieben 100 Millionen einzigartige Trainingsbeispiele mit unterschiedlichem Schwierigkeitsgrad
    • 9 Millionen davon sind Fälle mit hinzugefügten Hilfskonstruktionen
    • Das Sprachmodell lernte aus vielen Beispielen, in denen Hilfskonstruktionen zu einem Beweis führten, und kann dadurch auch bei Olympiade-Aufgaben neue Konstruktionen vorschlagen

Verifizierbarkeit und Grenzen der Anwendbarkeit

  • Alle von AlphaGeometry gelieferten Lösungen für Olympiade-Aufgaben wurden per Computer geprüft und verifiziert
  • Die Ergebnisse wurden mit früheren KI-Methoden und menschlichen Olympiade-Leistungen verglichen
  • Der Mathematiktrainer und frühere Olympiade-Goldmedaillengewinner Evan Chen bewertete einige der Lösungen
    • Die Ausgaben von AlphaGeometry sind verifizierbar und sauber
    • Bei früheren KI-Lösungen für beweisbasierte Wettbewerbsaufgaben war oft menschliche Prüfung nötig, weil sie mal korrekt und mal falsch waren
    • Die Lösungen von AlphaGeometry haben eine Struktur, die maschinell verifizierbar und zugleich für Menschen lesbar ist
    • Statt mit einem Koordinatensystem massive algebraische Rechnungen zu erzwingen, verwendet das System wie Schüler klassische Geometrieregeln wie Winkel und ähnliche Dreiecke
  • Eine IMO-Runde besteht aus 6 Aufgaben, von denen sich meist nur 2 auf Geometrie konzentrieren
    • Daher ist AlphaGeometry nur auf etwa ein Drittel der Aufgaben einer Runde anwendbar
    • Dennoch ist es das erste KI-Modell, das allein mit seiner Geometriefähigkeit die Bronze-Medaillen-Grenze der IMO 2000 und 2015 erreichen kann

Ausweitung auf KI für mathematisches Schlussfolgern

  • AlphaGeometry zeigt, dass KI immer besser logisch schlussfolgern sowie neues Wissen entdecken und verifizieren kann
  • Das Lösen von Geometrieaufgaben auf Olympiade-Niveau ist ein wichtiger Meilenstein auf dem Weg zu tieferem mathematischem Schlussfolgern und weiter entwickelten allgemeinen KI-Systemen
  • Der Ansatz, KI mit groß angelegten synthetischen Daten von Grund auf zu trainieren, könnte die Entdeckung neuen Wissens nicht nur in der Mathematik, sondern auch in Wissenschaft und KI beeinflussen
  • AlphaGeometry baut auf den Arbeiten von Google DeepMind und Google Research zu KI für mathematisches Schlussfolgern auf
  • Das langfristige Ziel ist, auf mehrere mathematische Teilgebiete zu verallgemeinern, anspruchsvolle Problemlösungs- und Schlussfolgerungsfähigkeiten für allgemeine KI-Systeme zu entwickeln und KI-Systeme zu schaffen, die die Grenzen menschlichen Wissens erweitern

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2024-01-18
Hacker-News-Kommentare

  • Als jemand, der bei Wettbewerben wie der IMO Aufgabensteller war, habe ich diese Arbeit mit großem Interesse gelesen. Gleichzeitig denke ich, dass Geometrie unter den Themen dasjenige ist, das als Erstes der KI zum Opfer fallen musste, also einer klugen Indizierung von Wissen und Schlussfolgerungsmethoden.
    Unter den Themen der Mathematik-Olympiade sind Geometrieaufgaben in der Regel am „mechanischsten“. Wenn man ein Problem in Koordinaten darstellen kann, etwa in XY-Koordinaten oder der komplexen Ebene, gibt es für den Computer eine endliche Menge von Schritten, mit denen er nach einer Lösung suchen kann. Natürlich verhindern bei der IMO in der Praxis Zeitlimits und menschliche Fehler die Nutzbarkeit. Früher habe ich auf diese Weise Beweise für Geometrieprobleme und Vermutungen, die ich erstellt hatte, mit WolframAlpha überprüft.
    Algebra, insbesondere Ungleichungen, ist ähnlich: Wenn man starke Rechenpower einsetzt, kommt oft eine Antwort heraus.
    Das Gebiet, in dem ich wirklich sehen möchte, wie sich intelligente Systeme weiterentwickeln, sind Zahlentheorie und Kombinatorik. Der Suchraum ist viel komplexer, und oft muss man beweisen, dass etwas unmöglich ist. Solche Probleme lassen sich schwer mit roher Rechengewalt lösen.

    • Als jemand, der diese Probleme löst, bin ich dafür zunächst einmal dankbar. Selbst Jahrzehnte nach dem Schulabschluss löse ich sie gelegentlich noch mit Freude.
      Ich stimme zu, dass Geometrie wohl zuerst dran ist. Soweit ich das hier sehe, ist es kein „Brute Force“ im Sinn einer Abhängigkeit von algebraischer Geometrie, Vektoren oder komplexen Lösungswegen, aber im Sinn eines lückenlosen Durchsuchens nach „interessanten“ Hilfskonstruktionen kommt es dem schon nahe.
      Geometrie war immer mein schlechtestes Fach, aber ich hatte oft das Gefühl, dass ein Problem mit der richtigen Konstruktion viel einfacher wird. Allerdings habe ich nie die Intuition entwickelt, solche Konstruktionen schnell zu sehen. Diese KI scheint diese Intuition auch nicht zu haben, kann aber viel schneller Möglichkeiten ausspucken. Die Kandidaten, die man konstruieren kann — Senkrechten, Parallelen, Winkelhalbierende — sind letztlich begrenzt, und man kann sie ziemlich mechanisch auswerten, indem man etwa alle Winkel und Verhältnisse entfaltet oder Potenzen von Punkten ausprobiert.
      Sehr beeindruckend, aber im Sinn von „Engine vs AI“ wirkt es eher wie DeepMind:Kasparov::AlphaGeo:Terry Tao.
      Ich stimme zu, dass Algebra wahrscheinlich als Nächstes kommt. Wie in der Geometrie muss man meist nur ein oder zwei oder drei clevere Substitutionen finden, und die Auswahl ist begrenzt.
      Manche Probleme der Kombinatorik könnten ebenfalls zu dieser Suchstrategie passen. Zum Beispiel Probleme, bei denen man dasselbe Objekt auf zwei Arten zählt. Das ist aber eine weiter entfernte Brücke und würde nur einen Teil aller Probleme abdecken.
      Zahlentheorie scheint mir die letzte Grenze zu sein, bevor volle 42 Punkte erreicht werden.
    • Mir gefällt diese positive Sicht auf solche Fortschritte. Fragst du dich nicht, ob es sich wie ein Verlust anfühlt, dass selbst die Fähigkeit, sehr gut in Mathematik zu sein, eines Tages von Maschinen eingeholt werden könnte? Oder glaubst du, dass so etwas auf absehbare Zeit nicht passieren wird?
    • Mich würde interessieren, wie man in eine solche Aufgabenstellerrolle kommt. Gibt es dafür eine Art Bewerbungsverfahren?
      Und nachdem geprüft wurde, ob eine Aufgabe lösbar ist, würde mich auch interessieren, wie ihr bestimmte Aufgaben für den endgültigen Satz auswählt. Per Abstimmung oder nach einem anderen Bewertungssystem?
    • Anfangs dachte ich, dass Ungleichungen mit drei Variablen zuerst fallen würden. Denn dort gibt es weniger Unklarheit darüber, was als Beweis gelten soll. Aber ich wusste nicht, dass die späteren Probleme bereits 2000 gelöst wurden (http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf).
      Jemand sollte aus synthetischer Geometrie ein Adventure-Spiel machen. Man könnte eine einfachere Sprache zum Schreiben von Beweisen verwenden als Lean, und es auch visuell ansprechend gestalten.

  • Wenn ich den Artikel richtig gelesen habe, wirkt das wie echte Arbeit. Viel legitimer als das KI-Mathematik-Paper, das DeepMind letzten Monat irreführend damit beworben hat, offene mathematische Forschungsprobleme gelöst zu haben. Trotzdem fällt ziemlich auf, wie anders die Struktur im Vergleich zu dem ist, was man sich gewöhnlich unter automatischem Schließen/Intelligenz vorstellt
    So wie ich es verstanden habe, wird ein Transformer mit Millionen elementarer Geometriesätze trainiert und dann dazu verwendet, Beweise per brute-force zu durchsuchen. Wegen des Kontexts elementarer Geometrie ist die Struktur zwangsläufig elementar, und wahr/falsch lässt sich symbolisch leicht entscheiden. Wenn die brute-force-Suche fehlschlägt, fügt man zufällig zusätzliche Hilfskonstruktionen wie Mittelpunkte hinzu und schaut, ob die Suche mit diesem zusätzlichen Material funktioniert
    Edit: Wie Imnimo korrigiert hat, hatte ich es genau andersherum verstanden. Die brute-force-Suche ist reine brute-force-Suche, und der Transformer wird verwendet, um vorherzusagen, welche Hilfskonstruktion hinzugefügt werden sollte
    Außerdem wird im Blogpost nicht erwähnt, dass auch die eigentlichen Problemformulierungen umgeschrieben/adaptiert werden mussten. Zum Beispiel wird ein Originalsatz wie „Seien AH1, BH2, CH3 die Höhen des Dreiecks ABC …“ in etwas viel Expliziteres umgeschrieben, etwa: „Sei ABC ein Dreieck. Definiere Punkt I so, dass AI die Winkelhalbierende von Winkel BAC ist und CI die Winkelhalbierende von Winkel ACB …“, und am Ende erhält man die Form „Beweise, dass T1I=IZ“

    • Diese Erklärung scheint nicht ganz richtig zu sein. Die brute-force-Suche wird nicht vom Transformer, sondern vom symbolischen Solver durchgeführt. Wenn keine neuen Schlüsse mehr herauskommen, lässt man den Transformer mögliche Hilfskonstruktionen vorschlagen; sie werden nicht zufällig hinzugefügt
    • Ich verstehe nicht, warum das weit entfernt von der üblichen Vorstellung von automatischem Schließen/Intelligenz sein soll. Schließen ist im Kern ein Suchproblem
      Der beschriebene Prozess ist exakt derselbe wie bei Menschen. Man vermutet etwas, das nützlich aussieht, und arbeitet die Details mechanisch aus. Wenn man feststeckt, macht man eine andere Vermutung. Am Ende ähnelt es dem Durchsuchen eines Baums
      Menschen hatten diesen Prozess bereits 1955 erkannt und sogar einen funktionierenden Prototyp gebaut, der Theoreme beweisen konnte: https://en.wikipedia.org/wiki/Logic_Theorist Der Kern hängt davon ab, gute Heuristiken zu verwenden. Neuronale Netze können Heuristiken aus Daten extrahieren, und darin liegt hier ihr Wert
      Ich frage mich, was du als die allgemeine Vorstellung von „automatischem Schließen“ ansiehst. Eine magische Maschine, die jedes Problem in einem einzigen linearen Durchlauf löst?
    • Dieses Vorgehen nach dem Motto „Wenn die brute-force-Suche scheitert, füge Hilfskonstruktionen wie Mittelpunkte hinzu und schau, ob die Suche mit dem zusätzlichen Material funktioniert“ war genau die Art von Geometrie, die ich in der Schule gelernt habe, und ich habe sie wirklich gehasst
      Erst als ich an die Mathematikfakultät kam, habe ich gelernt, wie man es richtig macht, und konnte daran Gefallen finden
    • Für die Rolle des Einzeichnens von Hilfslinien ein LLM zu verwenden, ist viel zu ineffizient. Es ist schwer vorstellbar, Unmengen an Maschinen einzusetzen, um einfache IMO-Probleme zu lösen
      Das Gebiet ist noch in einem frühen Stadium, und es scheint noch viel unfertige Arbeit zu geben. Den Suchteil sollte man durch ein kleines neuronales Netz ersetzen, und der Schlussteil ist nicht schwierig und scheint keine großen Verbesserungen zu brauchen
      Jetzt wäre der Zeitpunkt, die Leistung durch Self-Play zu steigern. In Problemen der ebenen Geometrie könnte man die zu beweisende Schlussfolgerung als einen Punkt der Figur und die Bedingungen als einen anderen Punkt betrachten und zwei Spieler einander so weit wie möglich entgegengehen lassen, während sie Daten austauschen. Dabei ließe sich der Beitrag jedes Spielers analog zur Berechnung von Sieg und Niederlage im Go zur Leistungsverbesserung nutzen

  • Dieses konkrete Modell wirkt nicht besonders generalisierbar, aber der neuro-symbolische Ansatz erscheint sehr vielversprechend
    Er verbindet die immer leistungsfähigeren „System-1“-Werkzeuge, die derzeit den Großteil des Machine Learning ausmachen, mit strukturierten „System-2“-Werkzeugen wie der Erzeugung logischer Beweise. System 2 kann planen und die Wahrheit oder den Wert von Ausgaben überprüfen
    System 2 arbeitet, bis es feststeckt; dann liefert System 1 eine intuitive Vermutung darüber, welchen Teil des Zustandsraums man als Nächstes prüfen sollte
    Hier wurde ausgenutzt, dass man Beweise per Computer erzeugen kann, um einen Datensatz von 100 Millionen Beweisen zu erstellen und so skalierbares selbstüberwachtes Lernen zu ermöglichen. Der symbolische Bereich scheint eine Form zu haben, die diese Datengenerierung gut zulässt. Der Wert einzelner Instanzen mag gering sein, aber in der Masse könnten sie nützliches Pretraining ermöglichen
    Zusammengenommen ist das ein Ansatz, mit dem man ziemlich weit kommen könnte
    Der zentrale Meilenstein wäre ein Pretraining-System, das nicht mehr darauf angewiesen ist, sich auf einen bestimmten formalen/symbolischen Bereich zu stützen, sondern die in diesem Bereich gelernten Techniken verallgemeinern kann

    • Man muss nicht alles auf einmal lösen. Dieser Ansatz hat das Potenzial, sowohl Mathematik als auch Programmierung zu verändern. Denn er könnte formale Verifikation von einem Nischenwerkzeug mit begrenztem Einsatz zu einem allgemeinen Bestandteil des Werkzeugkastens aller Praktiker machen
      Außerdem löst er innerhalb der anwendbaren Bereiche eines der grundlegenden Probleme, das im heutigen KI-Diskurs als „Halluzination“ bezeichnet wird, vollständig. Möglich ist das allerdings nur, weil es ein nicht-KI-basiertes System gibt, das die Korrektheit beweist
      Im großen Bild ist dieser Ansatz nicht völlig neu. In der Biochemie nutzt man schon länger KI, um Kandidatenmoleküle zu finden, und überprüft sie dann durch physikalische Experimente
      Auch KI für kombinatorische Spiele verwendet KI schon lange als Eingabe für die altbekannte Monte-Carlo-Suche
    • Das wirkt wie die bislang nächstliegende Möglichkeit, irgendeine Form von allgemeiner künstlicher Intelligenz zu erreichen

  • Es ist erfreulich, dass zusammen mit dem Paper auch Code und Gewichte veröffentlicht wurden. Soweit ich mich erinnere, ist dies das erste bekannte DeepMind-Paper, das ausführbaren Inferenzcode und Checkpoints freigibt. Falls es frühere Beispiele gibt, lasse ich mich gern korrigieren
    Zwar sehe ich noch keinen veröffentlichten Trainingssatz oder Beispielcode fürs Training, aber es ist trotzdem ein guter Fortschritt, dass sie anderen Forschern etwas gegeben haben, worauf sie aufbauen können. Letztlich ist genau das auch der Zweck wissenschaftlicher Paper

    • Schade, dass auch der Datensatz fehlt. Es heißt, sie hätten 100 Millionen synthetische Beispiele erzeugt, aber wurden diese Beispiele mit AlphaGeometry generiert? Wo sind der Filtercode und die anfänglichen Inputs zur Erzeugung dieser synthetischen Daten?
      Wenn ich mich nicht irre, verwenden sie ein t5-Modell? Zumindest scheint das SentencePiece-t5-Vokabular verwendet zu werden
      Mich würde auch interessieren, wie viel GPU-Zeit sie für das Training dieses Modells eingesetzt haben und welche Trainingsparameter verwendet wurden
      Nicht falsch verstehen: Dieses System ist faszinierend und zeigt, wie angewandtes Engineering aussehen sollte. Ich würde nur gern mehr über die Trainingsdetails, die Ausgangsdaten und die Methode zur Erzeugung der synthetischen Daten erfahren

  • Ich frage mich sehr, wie oft das Sprachmodell nützliche Konstruktionen erzeugt. Sicher besser als Zufall, aber ich weiß nicht, ob es Tausende von Konstruktionen ausspuckt, bis es eine gute findet, oder ob es in einem ähnlichen Verhältnis wie ein menschlicher Experte nützliche Vorschläge macht.
    Im Paper heißt es: „Da der Decoding-Prozess des Sprachmodells k verschiedene Sequenzen zurückgibt, die k alternative Hilfskonstruktionen beschreiben, führen wir eine Beam-Suche über diese k Optionen durch, wobei wir den Score jedes Beams als Wertfunktion verwenden. Diese Konfiguration lässt sich sehr leicht über Beams hinweg parallelisieren und wird bei vorhandenen parallelen Rechenressourcen stark beschleunigt. In den Experimenten verwenden wir eine Beam-Größe von k=512, eine maximale Iterationszahl von 16 und einen Verzweigungsfaktor pro Knoten, also eine Decoding-Batch-Größe, von 32.“
    Ich verstehe aber nicht vollständig, wie sich 512 und 16 in die insgesamt vorgeschlagene Zahl an Konstruktionen übersetzen. Es heißt auch, dass die Leistung nur begrenzt abfällt, wenn man Beam-Größe und maximale Iterationszahl reduziert. Bedeutet das, dass das Modell tatsächlich nützliche Konstruktionen ziemlich gut weit oben einordnet und nur bei den schwierigsten Problemen Tausende nötig sind?

    • Meine persönliche Vermutung ist, dass man hier hart an die Grenzen von Sprache und der Mensch-Maschine-Analogie stößt.
      Wenn man es trotzdem versucht, lautet die Zusammenfassung 262.144, aber man sollte das nicht wörtlich nehmen.
      Die Ausgabe der Decoding-Funktion sind Tokens, etwa 3/4 eines Wortes, aber nehmen wir der Einfachheit halber einfach 1 Wort an.
      Pro Ausgabetoken ist die Zahl der betrachteten Tokens beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262,144.
      Man kann die Wörter in einer Beispiel-Lösung zählen: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      Die Lösung hat insgesamt 2289 Tokens, und die insgesamt betrachtete Token-Zahl beträgt 262,144 * 2289 = 600,047,616.
      Mit einer Gewaltrechnung kann man die „Anzahl betrachteter Lösungen“ als insgesamt betrachtete Tokens / insgesamt Tokens der Lösung ansetzen, was wieder 262.144 ergibt. Das ergibt in dem Sinn Sinn, dass es derselbe Wert ist wie die Zahl der in jedem Iterationsschritt betrachteten Tokens.

  • Interessant ist, dass der verwendete Transformer klein ist. Laut Paper wurde mit den Standardeinstellungen der Meliad-Bibliothek trainiert und hat 12 Schichten, eine Embedding-Dimension von 1.024, 8 Attention-Heads und dichte Zwischenlagen zwischen den Attention-Blöcken mit Dimension 4.096 und ReLU-Aktivierung.
    Abgesehen von den Embedding-Schichten für Input- und Output-Head hat der gesamte Transformer 151 Millionen Parameter. Der angepasste Tokenizer wurde mit dem „word“-Modus von SentencePiece trainiert und hat eine Vokabulargröße von 757. Die maximale Kontextlänge wurde auf 1.024 Tokens begrenzt, und es werden relative Positions-Embeddings im Stil von T5 verwendet. Da mehr als 90 % der Sequenzen kürzer als 200 sind, wird auch Sequence Packing verwendet.

    • Das ist schwer als klein zu bezeichnen. Außerhalb des LLM-Bereichs ist das eine ziemlich normale Größe. Das entspricht zum Beispiel einem Sprachmodell, Übersetzungsmodell oder Akustikmodell normaler Größe. Manche würden selbst das schon groß nennen.
    • Dieses Ergebnis deutet darauf hin, dass es für Transformer in den harten Wissenschaften noch mehr tief hängende Früchte geben könnte, wenn sich etwas nur sauber genug formalisieren lässt. Das hier scheint kein Problem des Skalierungsumfangs gewesen zu sein.

  • Für mich war die eigentliche Neuigkeit, dass auch das vorherige Spitzensystem schon 10 solcher Probleme lösen konnte. Ich hatte zwar gehört, dass es Entscheidungsalgorithmen für Probleme der ebenen Geometrie gibt, wusste aber nicht, dass sie praktisch brauchbar sind. Beim Nachsehen tauchte als Referenz http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf auf.

    • Genau. Und der nicht-neuronale Teil von AlphaGeometry, also die Komponenten für symbolische Verarbeitung und lineare Algebra, kann für sich genommen schon die frühere Bestleistung übertreffen. Ein erheblicher Teil der Arbeit steckt hier auch in den nicht-neuronalen Komponenten.
    • Interessant, aber wenn man einfach mit den Formeln aus Evan Chens Buch Baryzentrische Koordinaten brutal durchrechnet, könnte man wahrscheinlich auch auf einem modernen Laptop etwa 30 % der IMO-Probleme lösen. Das wirkt plausibel, da die meisten davon Dreiecksprobleme sind.

  • Bei Ergebnissen dieser Art bin ich normalerweise darauf vorbereitet zu zweifeln, weil sie meist in die Richtung „sieht nicht wie ein menschlicher Beweis aus“ gehen, aber ich habe meine Meinung geändert, nachdem Evan Chen sagte, es seien tatsächlich saubere und für Menschen lesbare Beweise.
    Evan Chen ist eine bekannte Figur in der Olympiaden-Mathematik-Community und zudem Autor eines bekannten Olympiaden-Geometriebuchs[1], daher muss ich diesmal anerkennen, dass die Maschine einige IMO-Probleme tatsächlich erobert hat.
    [1]: https://web.evanchen.cc/geombook.html

    • Allerdings schien es mir, als gäbe es im vollständigen Beweis im Ergänzungsmaterial[1], beim Beweis von IMO P3 Fig1.f und in Schritt 26, einen Fehler. Dort heißt es ∠GMD = ∠GO2D, aber das ist falsch; ich dachte, es müsste ∠GMD + ∠GO2D = π heißen. Ich habe versucht, der Logik zu folgen, konnte Schritt 25 aber nicht deuten. Ich fragte mich, ob dieser Schritt eine Halluzination ist.
      Die Idee, dass O2 auf dem Neun-Punkte-Kreis liegt, ist aber dennoch richtig.
      Edit: Ich nehme das zurück. Es scheint, als würden gerichtete Winkel[2] verwendet, und dann ist die Aussage korrekt.
      [1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      [2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...

  • Dazu ist auch https://www.nytimes.com/2024/01/17/science/ai-computers-math... lesenswert.
    Ich bin über https://news.ycombinator.com/item?id=39030186 hierhergekommen, und der betreffende Thread soll hierhin zusammengeführt werden.

  • Damit verwandt: https://aimoprize.com/
    Ein Preisgeld von 10 Millionen Dollar für ein Modell, das bei der IMO gut abschneidet.