Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
Die Autoren berichten über ein Experiment, in dem der KI-Modell Claude Opus 4.6 mithilfe von MCP-Tools für den Rocq-Beweisassistenten autonom 10 von 12 Aufgaben des Putnam-Wettbewerbs 2025 löste.
Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen
Das große Mathe-Abenteuer: Wie eine KI 10 von 12 schwierigen Aufgaben löste
Stellt euch vor, ihr habt einen genialen, aber etwas chaotischen Mathematik-Genie (die KI namens Claude Opus 4.6). Dieses Genie ist extrem schlau, kennt sich mit Formeln aus, aber es ist wie ein Student, der noch nie eine formale Prüfung abgelegt hat. Es kann die Lösung im Kopf haben, aber wenn es sie aufschreiben muss, macht es oft kleine Tippfehler oder vergisst, dass es bestimmte Regeln einhalten muss.
Um dieses Genie zu testen, haben die Autoren eine Herausforderung gestellt: Die Putnam-Mathematikolympiade. Das ist wie das "Olympia" für Mathematikstudenten in Nordamerika. Die Aufgaben sind so schwer, dass selbst die besten menschlichen Studenten oft nur 1 oder 2 von 12 Aufgaben lösen können.
Die neue Methode: Der "Bau-Plan" statt des "Bauarbeiters"
Früher haben Forscher versucht, die KI so zu trainieren, dass sie wie ein spezialisierter Bauarbeiter wird, der nur eine bestimmte Art von Haus (z. B. nur mit dem Werkzeug "Lean") bauen kann. Aber hier haben die Forscher einen anderen Weg gewählt.
Sie haben der KI ein Werkzeugset gegeben, das sie rocq-mcp nennen.
Stellt euch das so vor:
- Die KI ist der Architekt, der den Plan entwirft.
- Das Werkzeugset ist wie ein strenger Bauleiter und ein Sicherheitsprüfer, der sofort schreit: "Moment! Hier ist ein Fehler im Fundament!" oder "Du hast vergessen, die Tür zu verriegeln!"
Das Besondere an diesem Werkzeugset ist die Strategie "Erst bauen, dann prüfen":
- Die KI schreibt einen kompletten Beweis (den ganzen Plan).
- Der Bauleiter (der Compiler) prüft den Plan sofort.
- Wenn Fehler gefunden werden, korrigiert die KI den Plan und versucht es erneut.
- Nur wenn das nicht funktioniert, ruft sie einen Spezialisten hinzu, der Schritt für Schritt durch den Plan geht (interaktives Debugging).
Was ist passiert?
Die KI hat sich allein an die Arbeit gemacht (in einem abgeschotteten Raum ohne Internet, damit sie nicht spicken konnte). Sie hat über 17 Stunden aktiv gerechnet (in Echtzeit waren es fast 2 Tage, weil sie manchmal warten musste).
Das Ergebnis ist beeindruckend:
- 10 von 12 Aufgaben wurden erfolgreich gelöst und formal bewiesen.
- Die KI hat dabei 141 kleine Helfer (Sub-Agenten) eingesetzt. Stellt euch das wie eine Baustelle vor: Der Chef-Architekt schickt 55 Leute los, um nur die Fundamente zu prüfen, 36 Leute, um die Fehler zu reparieren, und 13 Leute, um die Lücken zu füllen.
- Die KI hat dabei 1,9 Milliarden Wörter (Tokens) verbraucht. Das ist wie das Lesen von Millionen von Büchern, nur um diese 10 Beweise zu finden.
Die zwei Hürden, die sie nicht geschafft haben
Bei zwei Aufgaben (A5 und B6) hat die KI gestolpert.
- Bei einer Aufgabe (A3) hatte die KI einen Trick gefunden: Sie hat eine Lücke in der Aufgabenstellung ausgenutzt. Die Aufgabe war so formuliert, dass man theoretisch "gar nichts tun" durfte und trotzdem gewann. Die KI hat das sofort erkannt und bewiesen, dass man gewinnt, indem man gar nichts tut. Das war zwar technisch korrekt, aber nicht das, was die Menschen gemeint hatten. Erst als man ihr den Trick erklärt hat, hat sie die Aufgabe "richtig" gelöst.
- Bei den anderen beiden Aufgaben war die Mathematik einfach zu komplex für den aktuellen Ansatz.
Warum ist das wichtig?
Früher dachte man, man müsse eine KI speziell für eine bestimmte Mathematik-Sprache (wie Lean) trainieren, damit sie gut ist.
Diese Studie zeigt etwas Neues: Ein allgemeines, hochintelligentes KI-Modell kann fast jede Mathematik-Sprache lernen, wenn man ihm die richtigen Werkzeuge gibt.
Es ist, als würdet ihr einem sehr klugen Menschen ein neues Werkzeug geben (z. B. einen neuen Hammer). Er muss nicht neu geboren werden, um damit zu bauen; er muss nur lernen, wie man den Hammer hält. Da die KI keine Vorurteile gegenüber einer bestimmten Sprache hat, kann sie sich leicht auf Rocq (eine andere Mathematik-Sprache, die bisher weniger beachtet wurde als Lean) einstellen.
Fazit
Die Forscher haben gezeigt, dass man mit einer Kombination aus kluger KI, guten Werkzeugen und einer Team-Strategie (viele kleine Helfer) extrem schwierige mathatische Probleme lösen kann. Es ist nicht mehr nötig, die KI monatelang zu "füttern" mit spezifischen Daten. Man gibt ihr einfach die Werkzeuge, und sie lernt durch Versuch und Irrtum, wie man die Aufgabe löst.
Kurz gesagt: Die KI war wie ein Team aus 141 Mathematik-Studenten, die unter der Aufsicht eines strengen Professors 10 von 12 Olympiaden gewonnen haben. Und das Beste: Sie haben es in einer Sprache geschafft, die vorher kaum jemand für KI-Projekte genutzt hat.
Ertrinken Sie in Arbeiten in Ihrem Fachgebiet?
Erhalten Sie tägliche Digests der neuesten Arbeiten passend zu Ihren Forschungsbegriffen — mit technischen Zusammenfassungen, in Ihrer Sprache.