Mehr als 600 Schülerinnen und Schüler aus knapp 110 Ländern fanden sich im Juli 2024 im idyllischen englischen Städtchen Bath zusammen. Über mehr als elf Tage stellten sie sich einer der anspruchsvollsten Prüfungen auf der Welt, der Mathematik-Olympiade. Sie hatten jeweils viereinhalb Stunden Zeit, um sechs Aufgaben aus verschiedenen mathematischen Gebieten zu beantworten. Den ersten Platz mit einer vollen Punktzahl holte der chinesische Schüler Haojia Shi; im Landerranking lagen aber die USA vorne (Deutschland landete auf Platz 31). Das wirklich erstaunliche am diesjährigen Wettbewerb sind allerdings zwei Teilnehmer aus Silizium: Wie Google DeepMind berichtet, haben ihre KI-Programme insgesamt vier der sechs gestellten Aufgaben lösen können, was einer Silbermedaille entsprechen würde. »Das Programm hat 28 von insgesamt 42 möglichen Punkten erreicht. Damit schnitten nur 60 Schüler besser ab«, schreibt der Mathematiker Timothy Gowers auf X, der in der Vergangenheit selbst die Goldmedaille bei der Mathematik-Olympiade gewann und später mit der prestigeträchtigen Fields-Medaille ausgezeichnet wurde. Diese Punktzahl entspricht in der Bewertung einer Silbermedaille.

Um dieses beeindruckende Ergebnis zu erzielen, nutzte das DeepMind-Team zwei verschiedene, neue KI-Programme: AlphaProof und AlphaGeometry 2. Ersteres funktioniert ähnlich wie die Algorithmen, die in der Vergangenheit Großmeister bei Schach oder Go besiegten. Über »Reinforcement Learning« tritt das Programm dabei immer wieder gegen sich selbst an und verbessert sich dadurch Schritt für Schritt. Für Brettspiele lässt sich diese Methode – zumindest von der Grundidee her – recht einfach umsetzen: Die KI führt mehrere Spielzüge aus; wenn diese nicht zum Sieg führen, wird sie abgestraft und lernt, andere Strategien zu verfolgen.

Um diese Methode bei mathematischen Problemen umzusetzen, muss ein Programm aber prüfen können, ob es eine Aufgabe richtig gelöst hat oder nicht. Dafür nutzt AlphaProof so genannte Beweisprüfer: Das sind Algorithmen, die eine logische Argumentation Schritt für Schritt durchgehen, um nachzuvollziehen, ob alles korrekt ist. Zwar gibt es solche Beweisprüfer schon seit mehreren Jahrzehnten, allerdings sind sie sehr aufwändig zu verwenden. Man muss einen mathematischen Beweis erst sehr mühselig in eine für den Computer verständliche Sprache (etwa »Lean«) übersetzen, was teilweise mehrere Monate in Anspruch nehmen kann. Bislang wird diese Methode daher nur selten eingesetzt, weshalb es nur wenige Daten in Lean gibt. Damit eine KI solche Beweisprüfer anwenden kann, braucht sie aber hunderttausende oder Millionen von Beispielen, um daraus zu lernen.

Ein KI-Übersetzer für Matheaufgaben

Gewöhnliche Lösungen von Mathematikaufgaben gibt es hingegen in Hülle und Fülle. Im Internet finden sich etliche Rechenaufgaben, die Schritt für Schritt von Menschen gelöst wurden. Das Team von DeepMind hat daher ein großes Sprachmodell namens »Gemini« darauf traniert, eine Million solcher Aufgaben inklusive Lösungen in die Programmiersprache Lean zu übersetzen, damit ein Beweisprüfer sie verifizieren kann. »Mit einer Aufgabe konfrontiert, erzeugt AlphaProof mögliche Lösungen und beweist oder widerlegt sie, indem es mögliche Beweisschritte in Lean durchsucht«, schreiben die Entwickler. Auf diese Weise kann AlphaProof wie bei einem Schachspiel nach und nach lernen, welche Rechenschritte sinnvoll sind und welche nicht. Am Ende war AlphaProof in der Lage, Aufgaben aus der Algebra und Zahlentheorie zu meistern.

Geometrische Aufgaben, die ebenfalls in der Mathematik-Olympiade auftauchen, erfordern meist eine völlig andere Herangehensweise. Bereits im Januar 2024 hatte DeepMind eine KI namens AlphaGeometry vorgestellt, die solche Probleme erfolgreich lösen kann. Dafür ließen die Fachleute 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 Forschenden einen deduktiven Algorithmus, der daraus weitere Eigenschaften des Dreiecks folgert, beispielsweise welche Winkel übereinstimmen und welche Linien senkrecht aufeinanderstehen. Indem die Fachleute die geometrischen Ausgangssituationen mit den abgeleiteten Eigenschaften kombinierten, konnten sie einen geeigneten Trainingsdatensatz erstellen, der Aufgaben und die dazugehörigen Lösungen enthält. Ein Kernpunkt bestand aber darin, dieses Vorgehen mit einem Sprachmodell zu koppeln, das manchmal auch Hilfskonstruktionen nutzt: Es fügt etwa einem Dreieck einen weiteren Punkt hinzu, um daraus ein Viereck zu machen, was dabei helfen kann, eine Aufgabe zu lösen. Das DeepMind-Team hat diesen Ansatz nun verbessert: Sie trainierten das Modell mit noch mehr Daten und schafften es, den Algorithmus zu beschleunigen. Das Ergebnis ist AlphaGeometry 2.

»Hätte man den menschlichen Konkurrenten so viel Zeit pro Aufgabe zugestanden, hätten sie zweifellos mehr Punkte erzielt«Timothy Gowers, Mathematiker

Um ihre Programme zu testen, ließen die Forschenden von DeepMind die beiden KI-Systeme bei der diesjährigen Mathematik-Olympiade antreten. Dafür musste das Team die Aufgaben zunächst per Hand in die Programmiersprache Lean übersetzen. AlphaGeometry 2 schaffte es, innerhalb von nur 19 Sekunden das vorgelegte geometrische Problem richtig zu lösen. Und auch AlphaProof konnte zwei algebraische und ein zahlentheoretisches Problem meistern; darunter eines, das nur fünf der menschlichen Bestreiter knackten. An den kombinatorischen Aufgaben scheiterte die KI allerdings, was daran liegen könnte, dass sich solche Probleme nur sehr schwer in Programmiersprachen wie Lean übersetzen lassen.

Für eine der Aufgaben benötigte AlphaProof jedoch mehr als 60 Stunden – deutlich länger als die viereinhalb Stunden, die den Schülerinnen und Schülern zur Verfügung standen. »Hätte man den menschlichen Konkurrenten so viel Zeit pro Aufgabe zugestanden, hätten sie zweifellos mehr Punkte erzielt«, schreibt Timothy Gower auf X. »Dennoch: Das geht weit über das hinaus, was Beweisprüfer bisher leisten konnten. Und die Rechenzeit wird wahrscheinlich sinken, wenn die Programme effizienter werden.«

Gowers und der Mathematiker Joseph Myers, der ebenfalls eine Goldmedaille in vergangenen Mathematik-Olympiaden geholt hatte, bewerteten die Lösungen der beiden KI-Systeme nach denselben Kriterien wie die der menschlichen Teilnehmer. Nach diesen Maßstäben erzielten die Programme beeindruckende 28 Punkte. Damit ist der KI nur knapp die Goldmedaille entgangen, die es ab 29 erreichten Punkten gab.

»Stehen wir kurz vor dem Punkt, an dem Mathematiker überflüssig sind? Das ist schwer zu sagen«Timothy Gowers, Mathematiker

Auf X betont Gowers, dass die KI-Programme mit einer recht breiten Menge an Aufgaben trainiert wurden und sich ihre Einsatzgebiete nicht nur auf Mathematik-Olympiaden beschränken. »Wir könnten kurz davor stehen, ein Programm zu haben, das es Mathematikern ermöglicht, Antworten auf eine breite Palette von Fragen zu erhalten«, schreibt er. »Stehen wir kurz vor dem Punkt, an dem Mathematiker überflüssig sind? Das ist schwer zu sagen.«