Die Sicht eines Mathematikers auf die mathematischen Fähigkeiten von KI

• Das neue Sprachmodell o3 von OpenAI erreichte 25 % im schwierigen Mathematik-Benchmark FrontierMath und bringt damit die Einschätzung erneut ins Wanken, ob Mathematik-KI über das Bachelor-Niveau hinauskommen kann
• FrontierMath ist ein nicht öffentlicher Datensatz von Epoch AI, der aus Hunderten schwieriger Mathematikaufgaben besteht, die statt „beweise diesen Satz“ automatisch überprüfbare numerische Antworten verlangen
• Die fünf veröffentlichten Beispiele waren selbst für forschende Mathematiker nicht einfach; Tao bezeichnete sie als „extrem anspruchsvoll“, während Borcherds der Ansicht ist, dass das Finden einer Zahl nicht dasselbe ist wie ein origineller Beweis
• Nachdem Elliot Glazer von Epoch AI erklärt hatte, 25 % der Aufgaben seien „IMO-/Bachelor-artige Aufgaben“, bleibt wegen des nicht öffentlichen Datensatzes schwer zu beurteilen, welches Schwierigkeitsniveau o3 mit seinen 25 % tatsächlich erreicht hat
• Das für Mathematiker wichtigere Ziel ist nicht „finde diese Zahl“, sondern einen Satz korrekt zu beweisen und ihn für Menschen verständlich zu erklären; Sprachmodelle und Lean-basierte Ansätze haben dabei unterschiedliche Grenzen

---

o3 und FrontierMath verschieben die Messlatte

• o3 ist das neue Sprachmodell von OpenAI und erreichte bei FrontierMath eine Punktzahl von 25 %
• Seit ChatGPT verbessern sich öffentlich verfügbare Sprachmodelle rasant, und auch ihre Fähigkeit zum Lösen mathematischer Probleme wird in diesem Kontext bewertet
• FrontierMath ist ein nicht öffentlicher Datensatz mathematischer Aufgaben von Epoch AI; im Abstract des Papers heißt es, er enthalte „Hunderte“ schwieriger Mathematikaufgaben
• Würde der Datensatz veröffentlicht, könnten Sprachmodelle die Aufgaben und Antworten lernen; deshalb werden selbst grundlegende Angaben wie die Anzahl der Aufgaben vorsichtig behandelt
  • Wenn Aufgaben und Antworten veröffentlicht werden, kann ein Modell bereits gesehene Antworten reproduzieren
  • Dadurch lassen sich tatsächliche Schwierigkeit und Repräsentativität eines nicht öffentlichen Benchmarks von außen nur schwer überprüfen

Format und Schwierigkeit der FrontierMath-Aufgaben

• FrontierMath-Aufgaben entsprechen weniger dem Format „Beweise diesen Satz“, sondern eher „Finde diese Zahl“
• Die Aufgaben müssen eine eindeutige, berechenbare Antwort haben und automatisch überprüfbar sein
• Die Antworten der fünf veröffentlichten Beispielaufgaben sind allesamt positive ganze Zahlen
  • Zu den Beispielantworten gehören 9811 und 367707
  • Die übrigen drei Antworten sind größer und so konzipiert, dass sie durch zufälliges Raten schwer zu treffen sind
• Die veröffentlichten Beispiele sind selbst für forschende Mathematiker nicht trivial
  • Der Autor versteht die Aussagen aller fünf Aufgaben
  • Die dritte Aufgabe konnte er relativ schnell lösen; bei der fünften Aufgabe wusste er, wie man sie mit der Standardmethode über die Weil-Vermutungen für Kurven lösen kann, berechnete die 13-stellige Antwort aber nicht
  • Die erste und zweite Aufgabe hielt er für nicht lösbar; bei der vierten glaubte er, mit Aufwand Fortschritte machen zu können, las aber die Lösung, ohne es zu versuchen
• Für gewöhnlich sehr gute Mathematik-Studierende im Bachelor könnten selbst einzelne dieser Aufgaben schwer zu lösen sein
  • Für die erste Aufgabe sei vermutlich mindestens Niveau eines Promotionsstudiums in analytischer Zahlentheorie nötig

Stärken und Grenzen von Benchmarks mit numerischen Antworten

• Der Hauptgrund, warum FrontierMath Aufgaben mit numerischen Antworten verwendet, sind die Bewertungskosten
• Um Hunderte Antworten des Typs „Beweise diesen Satz“ zu bewerten, braucht man menschliche Experten
  • Stand 2024 erscheint es schwierig, eine Bewertung auf diesem Niveau Maschinen zu überlassen
• Eine Liste numerischer Antworten kann ein Computer dagegen sehr schnell vergleichen
• Borcherds ist der Ansicht, dass forschende Mathematiker den größten Teil ihrer Zeit nicht mit Zahlen, sondern mit der Suche nach Beweisen und Ideen verbringen
• Dennoch ist FrontierMath für das Feld der Mathematik-KI wertvoll
  • Es gibt nur sehr wenige schwierige Datensätze
  • Solche Datensätze zu erstellen ist sehr schwierig oder teuer
  • Ein aktueller Beitrag von Frieder und anderen behandelt die Grenzen von Datensätzen für Mathematik-KI ausführlicher

Warum o3s 25 % überraschend waren

• Nach bisheriger Wahrnehmung lag Mathematik-KI eher auf Bachelor- oder Vor-Bachelor-Niveau
• KI wird bei olympiadeartigen Aufgaben, wie sie begabte Schüler lösen, sehr stark
• Es gilt als klar, dass KI innerhalb eines Jahres Bachelor-Prüfungen in Mathematik bestehen wird
  • Bachelor-Prüfungen enthalten häufig Standardaufgaben, die Studierende bestehen können, wenn sie den Kurs grundsätzlich verstanden haben
  • Maschinen können solche Aufgaben leicht richtig lösen
• Der Sprung von der Wiederverwendung standardmäßiger Ideen hin zu innovativen Ideen auf fortgeschrittenem Bachelor- oder frühem Promotionsniveau gilt jedoch als groß
• Die jüngsten ChatGPT-Antworten zur Putnam-Prüfung blieben hinter den Erwartungen zurück
  • Die einzige angemessene Antwort der Maschine schien B4 zu sein
  • Die meisten anderen Antworten wurden als etwa 1 bis 2 von 10 Punkten eingeschätzt
• Aus diesen Gründen wurde erwartet, dass FrontierMath über mehrere Jahre hinweg kaum zu knacken sein würde

Die Unsicherheit nicht öffentlicher Datensätze

• Elliot Glazer von Epoch AI erklärte auf Reddit, dass 25 % der FrontierMath-Aufgaben IMO-/Bachelor-artige Aufgaben seien
• Diese Aussage scheint nicht gut zu den fünf veröffentlichten Aufgaben zu passen
  • Selbst die leichteste der veröffentlichten Beispielaufgaben ließ sich mit den Weil-Vermutungen für Kurven angehen
  • Alternativ könnte ein mühsames Brute-Force-Verfahren nötig sein, bei dem ein kubisches Polynom vom Grad 10^12 über einem endlichen Körper faktorisiert wird
• Diese Information lässt Fragen zur tatsächlichen Schwierigkeit des nicht öffentlichen Datensatzes und dazu offen, ob die fünf veröffentlichten Aufgaben eine repräsentative Stichprobe sind
• Da der Datensatz nicht öffentlich ist, lässt sich diese Frage nicht leicht klären
• Wenn 25 % Bachelor-Niveau-Aufgaben sind, könnte o3s 25-%-Punktzahl weniger überraschend sein
• Der erwartete große Durchbruch wäre der Zeitpunkt, an dem KI bei den nächsten 50 % der Aufgaben, die als „qual level“ beschrieben wurden, eine sinnvolle Leistung zeigt

„Beweise diesen Satz“ bleibt ein anderes Problem

• In der mathematischen Forschung lautet die wichtige Frage meist „Beweise diesen Satz“
• Selbst wenn es Maschinen mit übermenschlicher Leistung bei Aufgaben zur Zahlensuche gäbe, könnte ihre Anwendbarkeit in vielen Bereichen der mathematischen Forschung begrenzt sein
• Als größter Erfolg des Jahres 2024 gilt DeepMinds AlphaProof
  • AlphaProof löste 4 der 6 Aufgaben der IMO 2024
  • Die Aufgaben waren vom Typ „Beweise diesen Satz“ oder „Finde eine Zahl und beweise, dass sie korrekt ist“
  • Drei davon wurden als vollständig formalisierte Lean-Beweise ausgegeben
• Lean ist ein interaktiver Theorem Prover, und mathlib ist eine mathematische Bibliothek, die viele für IMO-Aufgaben nötige Techniken und darüber hinaus enthält
• Die Lösungen des DeepMind-Systems wurden von Menschen geprüft und als Lösungen mit „voller Punktzahl“ verifiziert
• Allerdings verwenden die Lösungen von IMO-Aufgaben, auch wenn diese sehr schwierig sind, nur Techniken auf Schulniveau; damit kehrt man gewissermaßen wieder zu Aufgaben auf Highschool-Niveau zurück
• Für 2025 wird erwartet, dass Maschinen eine Leistung auf IMO-Goldmedaillen-Niveau zeigen werden

Wer bewertet die Antworten der Maschinen?

• Man kann sich vorstellen, dass im Juli 2025 bei der IMO nicht nur menschliche Schüler, sondern auch Maschinen teilnehmen
• Maschinelle Systeme könnten in zwei Typen fallen
  • Systeme, die Antworten in einer Sprache für Computer-Beweisprüfer wie Lean, Rocq oder Isabelle einreichen
  • Sprachmodelle, die Antworten in menschlicher Sprache einreichen
• Bei Antworten in einer Sprache für Beweisprüfer muss nur überprüft werden, ob die Aufgabenstellung korrekt übersetzt wurde
  • Wenn der Beweis anschließend kompiliert, weiß man praktisch, dass es eine Lösung mit „voller Punktzahl“ ist
• Anders ist es bei Sprachmodellen, die natürlichsprachliche Antworten einreichen
  • Selbst wenn eine Antwort plausibel aussieht, müssen menschliche Korrektoren sie sorgfältig lesen und bewerten
  • Es gibt keine Garantie, dass es eine Lösung mit voller Punktzahl ist
• Sprachmodelle gelten beim logischen Schließen als mindestens eine Größenordnung weniger präzise als menschliche Experten
• Es besteht die Sorge, dass ein Sprachmodell-„Beweis“ der Riemannschen Vermutung inmitten von zehn Seiten korrekter Mathematik vage oder ungenaue Behauptungen einstreut
• Theorem Prover gelten umgekehrt als mindestens eine Größenordnung präziser
  • Wenn Lean ein Argument aus der menschlichen mathematischen Literatur nicht akzeptierte, lag in den dem Autor bekannten Fällen der Fehler auf menschlicher Seite

Offene Ziele: korrekte Beweise und menschliches Verständnis

• Was Mathematiker wollen, ist nicht einfach „Beweise diesen Satz“, sondern ein korrekter Beweis und eine für Menschen verständliche Erklärung
• Beim Sprachmodell-Ansatz bleibt „Korrektheit“ eine große Sorge
• Beim Ansatz über Theorem Prover ist die Sorge, ob die Ergebnisse „für Menschen verständlich“ sind
• Es bleibt noch sehr viel zu tun
• Das Entwicklungstempo ist hoch, aber niemand weiß, wann die Bachelor-Hürde überschritten wird