Die Internationale Mathematik-Olympiade (IMO) ist der wohl renommierteste Schülerwettbewerb. Um die begehrten Bronze-, Silber- und Goldmedaillen wetteifern jedes Jahr Schülerinnen und Schüler aus aller Welt (2023 nahmen 112 Länder teil) – und schon bald könnten ihnen KI-Programme Konkurrenz machen.

Ein Team um Trieu H. Trinh von Google DeepMind und der New York University hat am 17. Januar 2024 in der Fachzeitschrift »Nature« ein neues KI-Programm namens AlphaGeometry vorgestellt, das 25 von 30 gestellten Geometrie-Aufgaben aus vergangenen Mathematik-Olympiaden erfolgreich lösen konnte. Damit hatte die KI eine ähnliche Erfolgsquote wie die besten menschlichen Teilnehmer und Teilnehmerinnen, die beim Wettbewerb eine Goldmedaille gewinnen konnten. Außerdem fand AlphaGeometry eine allgemeinere Lösung zu einem Problem von der IMO im Jahr 2004, die Fachleuten bisher entgangen war.

»Mathematik-Olympiaden sind die weltweit renommiertesten Wettbewerbe zum Lösen von Theoremen«, schreiben Trinh und seine Kollegen in ihrer aktuellen Veröffentlichung. An zwei Tagen müssen die Schülerinnen und Schüler jeweils drei Aufgaben aus verschiedenen mathematischen Gebieten bearbeiten. Teilweise sind die Probleme so kompliziert, dass selbst Fachleute sie nicht lösen können. Die Aufgaben besitzen in der Regel kurze, elegante Lösungen, die jedoch viel Kreativität verlangen. Das macht sie aus Sicht der KI-Forschung besonders interessant. Denn bisher versagten selbst große Sprachmodelle wie GPT-4 von OpenAI bei solchen Aufgaben.

Einer der Gründe, warum KI-Programme bislang an höherer Mathematik scheiterten, sind die mangelnden Datensätze. Große Sprachmodelle wie GPT-4 werden mit zweistelligen Gigabyte an Textdateien trainiert, was etwa 20 Millionen gefüllten DIN-A4-Seiten entspricht. Zwar gibt es viele mathematische Arbeiten, aber einen Beweis in eine für Computer verständliche Programmiersprache wie »Lean« zu übersetzen, erfordert sehr viel Arbeit. Im Bereich der Geometrie fällt das extrem schwer ins Gewicht: Dort sind die Beweise meist noch schwieriger zu formalisieren. Es gibt zwar speziell für die Geometrie entwickelte Programmiersprachen, doch diese lassen kaum Methoden aus anderen Bereichen zu. Wenn ein Beweis also einen Zwischenschritt erfordert, bei dem etwa komplexe Zahlen (mit Wurzeln aus negativen Werten) auftauchen, lässt sich diese Geometrie-Sprache nicht nutzen.

Eine riesige Sammlung an mathematischen Beweisen

Deshalb haben die Forscher um Trinh einen eigenen Datensatz erstellt, ohne dafür von Menschen geführte Beweise in eine formale Sprache übersetzen zu müssen. Sie ließen zunächst einen Algorithmus geometrische Ausgangssituationen erzeugen: etwa ein Dreieck mit eingezeichneten Höhen und zusätzlich markierten Punkten entlang der Seiten. Dann nutzten die Forscher einen deduktiven Algorithmus, der daraus weitere Eigenschaften des Dreiecks folgert, beispielsweise welche Winkel übereinstimmen und welche Linien senkrecht aufeinanderstehen. Solche Programme gibt es schon seit mehreren Jahrzehnten: Sie greifen auf vorgegebene geometrische und algebraische Rechenregeln zurück, um Aussagen über geometrische Objekte zu treffen.

Indem die Forscher die geometrischen Ausgangssituationen mit den abgeleiteten Eigenschaften kombinierten, konnten sie einen geeigneten Trainingsdatensatz erstellen, der Aufgaben und die dazugehörigen Lösungen enthält. Zum Beispiel könnte das Problem lauten, ein bestimmtes Merkmal eines Dreiecks nachzuweisen (etwa, dass zwei Winkel gleich sind). Die entsprechende Lösung besteht dann aus den logischen Schritten, die den deduktiven Algorithmus zu dieser Eigenschaft geführt haben. Trinh und sein Team haben auf diese Weise einen Datensatz mit mehr als 100 Millionen Aufgaben inklusive Beweisen erzeugt.

Eine KI kommt zu Hilfe

Allerdings genügen solche Methoden nicht, um Aufgaben auf dem Niveau von Mathematik-Olympiaden zu bewältigen. Die dort gestellten Probleme erfordern meist mehr als die bloße Anwendung von simplen Deduktionen. »Entscheidend ist die Einführung neuer Beweisbegriffe«, schreiben Trinh und sein Team. Möchte man beispielsweise etwas über ein Dreieck beweisen, ist es manchmal nötig, neue Punkte und Linien einzuführen, die in der Aufgabenstellung nicht genannt wurden. Genau dieses Einführen neuer Hilfsobjekte, um sich einem Beweis zu nähern, sollte ein großes KI-Sprachmodell ähnlich wie GPT übernehmen.

Sprachmodelle erzeugen Texte, indem sie gemäß einer Wahrscheinlichkeitsverteilung nach und nach Wörter ausgeben. Wegen der enormen Datenmengen, mit denen sie trainiert werden, gelingt es KI-Programmen wie ChatGPT teilweise sinnvoll auf Fragen zu antworten und sogar menschenähnliche Dialoge zu führen. Trinh und sein Team konnten nun die eigens angefertigte Datenbank nutzen, um AlphaGeometry mit mathematischen Aufgaben und Beweisen zu trainieren. Das große KI-Sprachprogramm sollte dabei aber nicht die deduktiven Schritte eines Beweises lernen. Diese Arbeit übernehmen weiterhin die darauf spezialisierten deduktiven Algorithmen. Das KI-Modell sollte sich vielmehr darauf konzentrieren, nützliche Hilfskonstruktionen zu finden.

»Die Methode klingt plausibel und in gewisser Weise ähnlich wie das Training von Teilnehmern der Internationalen Mathematik-Olympiade«Peter Scholze, Mathematiker

Übergibt man AlphaGeometry eine Aufgabe, leitet zunächst ein deduktiver Algorithmus verschiedene Eigenschaften aus dem beschriebenen System ab. Wenn die zu beweisende Aussage nicht darin enthalten ist, erzeugt das Sprachmodell eine Hilfskonstruktion. Es kann etwa entscheiden, zu einem Dreieck ABC einen vierten Punkt X hinzuzufügen, so dass ABCX ein Parallelogramm darstellt – weil sich ein solcher Schritt in anderen Situationen, die die KI während des Trainings kennen gelernt hat, bereits bewährt hatte. Damit erhält der deduktive Algorithmus neue Informationen, die er nutzen kann, um weitere Eigenschaften des geometrischen Objekts abzuleiten. Das kann man wiederholen, bis die KI und das deduktive Programm zum gewünschten Schluss kommen.

»Die Methode klingt plausibel und in gewisser Weise ähnlich wie das Training von Teilnehmern der Internationalen Mathematik-Olympiade«, sagt Fields-Medaillenträger Peter Scholze, der in der Vergangenheit selbst dreimal die IMO-Goldmedaille gewonnen hat. Um AlphaGeometry zu testen, wählten die vier Wissenschaftler 30 geometrische Aufgaben aus, die seit dem Jahr 2000 in Mathematik-Olympiaden erschienen sind. Während das bisher genutzte Standardprogramm zur Bewältigung geometrischer Probleme (»Wu’s method«) gerade einmal zehn Aufgaben richtig bearbeitete und GPT-4 an allen scheiterte, gelang es AlphaGeometry, 25 davon zu lösen. Wie die Forscher angeben, übertrifft die KI damit die meisten IMO-Teilnehmer, die im Durchschnitt 15,2 von 30 Aufgaben bewältigen. Goldmedaillen-Gewinner gelänge es hingegen, im Mittel 25,9 Aufgaben zu beweisen. Allerdings bearbeiten die menschlichen Kandidaten nicht bloß geometrische Probleme: Die IMO-Aufgaben umfassen auch andere Bereiche der Mathematik wie Algebra, Zahlentheorie und Kombinatorik. »Die genannten Leistungen von AlphaGeometry bei den IMO-Geometrie-Aufgaben finde ich schon sehr beeindruckend«, sagt der Mathematiker Uwe Leck von der Europa-Universität Flensburg, der die Mathematik-Olympiade in Deutschland koordiniert.

Als die Forscher die KI-erzeugten Beweise durchsahen, fiel ihnen auf, dass das Programm bei einer Aufgabe aus dem Jahr 2004 nicht alle mitgelieferten Informationen der Aufgabenstellung genutzt hatte. Damit hat AlphaGeometry eine allgemeinere Aufgabe gelöst als die gestellte. Zudem ließ sich erkennen, dass komplizierte Aufgaben (bei denen IMO-Teilnehmer schlecht abschnitten) in der Regel auch der KI längere Beweisführungen abverlangten. Damit scheint sich die Maschine mit denselben Aufgaben schwerzutun wie Menschen.

»Es würde mich auch nicht überraschen, wenn in einigen Jahren KI-Systeme so gut abschneiden wie die allerbesten Schülerinnen und Schüler«Uwe Leck, Mathematiker

Eine richtige Chance, an der Internationalen Mathematik-Olympiade teilzunehmen, hat AlphaGeometry bis jetzt noch nicht: Da die Geometrie-Aufgaben meist nur ein Drittel der gestellten Probleme ausmachen, kann die KI im Vorfeld nicht genug Punkte für die Zulassung sammeln. Doch Trinh und seine Kollegen betonen, dass sich ihr Ansatz auch auf andere mathematische Bereiche anwenden lässt. »Ich erwarte, dass es sehr bald KI-Modelle gibt, die bei der IMO konkurrenzfähig wären. Es würde mich auch nicht überraschen, wenn in einigen Jahren KI-Systeme so gut abschneiden wie die allerbesten Schülerinnen und Schüler«, sagt Leck.