KI forscht wie Mathematiker: Benchmark TCSExam prüft Beweise maschinell

Worum es geht

Kann eine KI tatsächlich mathematisch forschen – oder nur Übungsaufgaben lösen, deren Antworten irgendwo im Netz stehen? Dieser Frage geht ein neues Paper nach, an dem zwei prominente Namen der chinesischen KI-Szene erstmals gemeinsam beteiligt sind: Andrew Chi-Chih Yao (Yao Qizhi), Turing-Preisträger, Mitglied der Chinesischen Akademie der Wissenschaften und Dekan des Instituts für interdisziplinäre Informationswissenschaften der Tsinghua-Universität, sowie Yang Zhilin, Gründer von Moonshot AI (Yuezhi Anmian), dem Unternehmen hinter dem Chatbot Kimi.

Das Ergebnis heißt TCSExam: ein Prüfungssystem aus 100 Forschungsaufgaben der theoretischen Informatik (englisch Theoretical Computer Science, kurz TCS). Getestet wurden aktuelle KI-Agenten – also KI-Systeme, die selbstständig über viele Schritte arbeiten, Code schreiben und Werkzeuge nutzen. Das Paper ist auf arXiv erschienen (arxiv.org/pdf/2611.07962v1). Das chinesische Tech-Portal Leiphone hat die Arbeit ausführlich aufbereitet; dieser Artikel stützt sich auf diesen Bericht.

Die Schlagzeile: eine Kante mehr

Aufhänger des Leiphone-Berichts ist ein auf den ersten Blick winziges Ergebnis: Kimi hat bei einer Graphen-Konstruktion den bisherigen Referenzrekord von 629 Kanten auf 630 verbessert. Ein Graph ist in der Mathematik ein Netz aus Punkten (Knoten) und Verbindungslinien (Kanten); hier geht es um einen Graphen mit 124 Knoten. Bei solchen sogenannten Extremalkonstruktionen sucht man das größte oder kleinste Objekt, das bestimmte strenge Regeln gerade noch erfüllt. Welche Bedingung der Graph genau erfüllen muss, geht aus dem Bericht nicht hervor.

Warum ist eine Kante der Rede wert? Laut Leiphone muss für jede zusätzliche Kante oft die gesamte Struktur zwischen allen 124 Punkten neu arrangiert werden. Die Redaktion wertet das als erstes Mal, dass eine KI bei dieser Art von Forschungsaufgabe einen menschlichen Referenzwert übertroffen hat. Gleichzeitig wirft sie selbst die naheliegenden Fragen auf: Ist das ein echter Durchbruch oder ein Glückstreffer durch rohe Rechenkraft? Versteht die KI die Mathematik dahinter? Genau diese Unterscheidung soll TCSExam ermöglichen.

Wie TCSExam aufgebaut ist

Die 100 Aufgaben verteilen sich auf vier Bereiche:

Lean 4 ist eine Programmiersprache für mathematische Beweise: Man schreibt den Beweis so exakt auf, dass ein Computerprogramm jeden einzelnen Schritt prüfen kann. Ein „Solver“ ist ein Programm, das eine bestimmte Klasse von Problemen möglichst gut löst.

Das Grundprinzip nutzt eine Eigenschaft, die in der theoretischen Informatik zentral ist: Lösungen zu finden ist schwer, sie zu überprüfen ist leicht. Jede KI muss deshalb ein „Forschungszertifikat“ abliefern, das ein Prüfprogramm automatisch kontrollieren kann – Lean-Code bei Beweisen, lauffähige Programme bei Solvern, konkrete Objekte bei Konstruktionen. Das System prüft auch, ob ein Beweis unerlaubte Platzhalter für unfertige Stellen oder zusätzliche Annahmen (Axiome) enthält.

Ein unterschätztes Problem ist die Übersetzung in Maschinensprache: Wird beim Formalisieren eines Theorems versehentlich eine Einschränkung hinzugefügt – etwa eine Obergrenze für die Größe eines Graphen –, beweist die KI am Ende ein leichteres Problem. Deshalb erstellt ein Agent die formalen Aufgaben, ein zweiter Agent prüft Definitionen, Quantoren und Parameter, und Fachleute bestätigen die Forschungsrelevanz. Über 40 Kandidaten-Theoreme flogen schon in Testläufen raus, weil sie zu leicht gelöst wurden. Bei Solver-Aufgaben werden manche Testfälle mathematisch umgeformt, damit die KI nicht einfach bekannte Antworten wiederverwendet.

Teilerfolg ist kein Beweis

Bei Beweisen gibt es drei Hilfestufen: Bare (nur das Theorem und nötige Definitionen), Ladder (zusätzlich Zwischenschritte, sogenannte Lemmata) und Guided (dazu eine Beweisidee). Außerdem werden lange Beweise mit „Checkpoints“ in Zwischenziele zerlegt. Ein Checkpoint wird geprüft, indem die anderen vorübergehend als wahr angenommen werden. Das hat eine logische Falle: Stützt sich A auf B und B auf A, bestehen beide Einzelprüfungen, obwohl der Gesamtbeweis im Kreis läuft. Darum muss das Haupttheorem am Ende ohne unbewiesene Annahmen bestehen.

Wie wichtig das ist, zeigt ein Beispiel: Kimi K3 schaffte in einem Versuch 7 Checkpoints und damit 87,5 Prozent Abdeckung, aber nicht den letzten Schritt zum Haupttheorem – das System wertete das nicht als Beweis.

Die Zahlen zeigen: Mit Hilfen steigt die Erfolgsquote deutlich. Die eigentliche Schwierigkeit liegt laut den Forschern darin, die entscheidenden Lemmata selbst zu finden und verstreute Überlegungen zu einem vollständigen Beweis zu ordnen. Findet eine KI einen ganz anderen Weg am vorgegebenen Gerüst vorbei, wird das aber ebenfalls akzeptiert.

Insgesamt am stärksten war GPT-6 Astra: Es bewies 14 der 20 Forschungstheoreme. Bei einer Logiksynthese-Aufgabe aus dem Wettbewerb IWLS 2023 – es geht darum, Schaltungen mit möglichst wenigen Logikgattern zu bauen – lieferte Astra für alle 100 Testfälle gültige Schaltungen: 22 waren besser als die öffentlichen Referenzschaltungen, 31 gleich gut, 47 benötigten mehr UND-Gatter.

Der Beweis für 9 Dimensionen

Das eindrucksvollste Einzelergebnis betrifft die Alon–Jaeger–Tarsi-Vermutung. Vereinfacht: Zu jeder invertierbaren Matrix über einem endlichen Zahlenkörper soll es einen Vektor geben, dessen Einträge alle ungleich null sind und der auch nach der Multiplikation mit der Matrix keine Null enthält. Für den Körper mit fünf Elementen war das bis 8 Dimensionen gezeigt; Astra schaffte 9.

Weil schlichtes Durchprobieren bei 9 Dimensionen nicht machbar ist, ging Astra so vor: Es nahm ein kleinstes Gegenbeispiel an und nutzte die bereits bewiesenen kleineren Fälle, um dessen Eigenschaften einzuschränken. Statt einzelne Matrixeinträge zu betrachten, zählte es, wie viele Koordinaten vor und nach der Transformation ungleich null sind, und baute daraus zwei 10×10-Tabellen nichtnegativer Ganzzahlen. Paare von Matrixspalten teilte es in 7 Kategorien ein; da deren Anzahlen zusammen 9 ergeben müssen, blieben nur 5005 Kombinationen. Zusammen mit Bedingungen aus inverser und transponierter Matrix entstand ein lineares Gleichungssystem mit 204 nichtnegativen Variablen und 197 Gleichungen.

Astra kombinierte 143 davon mit passenden ganzzahligen Faktoren zu einer unmöglichen Gleichung: Alle 204 Koeffizienten sind nichtnegativ (93 positiv, 111 null), die rechte Seite aber negativ. Da die Variablen nicht negativ sein können, ist das ein Widerspruch – das Gegenbeispiel existiert nicht. Der gesamte Beweis wurde als Projekt mit 71 Lean-Modulen unabhängig neu kompiliert und auf seine Axiome geprüft.

Einordnung

TCSExam ist vor allem als Messinstrument interessant: Statt KI an Aufgaben mit bekannter Musterlösung zu testen, verlangt es Ergebnisse, die eine Maschine unabhängig verifizieren kann – und trennt sauber zwischen Teilerfolg und vollständigem Beweis. Das macht Aussagen wie „KI hat ein mathematisches Problem gelöst“ überprüfbarer als viele bisherige Ankündigungen.

Die Grenzen sind aber deutlich. Der 9-Dimensionen-Beweis betrifft einen Spezialfall; die allgemeine Vermutung bleibt offen. Von 30 offenen Vermutungen wurden 28 nicht gelöst, und die zwei akzeptierten Gegenbeispiele (zu Ryser und MIRUP) entstanden durch das Auffinden und Anpassen bereits veröffentlichter OpenAI-Ergebnisse. Ob die Kante mehr beim Graphen-Rekord auf tiefem Verständnis oder auf geschickter Suche beruht, beantwortet der Bericht nicht abschließend. Zudem ist eine Moonshot-Beteiligung bei einem Benchmark, in dem Kimi prominent auftaucht, ein Punkt, den man im Hinterkopf behalten sollte – auch wenn GPT-6 Astra in den genannten Zahlen besser abschneidet.

Das Fazit der Leiphone-Autoren trifft es: Bemerkenswert sind weniger „630 statt 629“ oder „9 statt 8“, sondern dass KI bei manchen Forschungsaufgaben inzwischen maschinell überprüfbare neue Ergebnisse liefert. Wichtige Lemmata selbst zu finden und lange Beweise eigenständig zu planen, gelingt ihr aber noch kaum.