Der billige Prüfer: Warum ein elftägiger Agentenlauf in der Mathematik gelingt — und in Ihrem Unternehmen vermutlich nicht

Elf Tage, sechs Milliarden Token — und 462 pro Zeile

Die Zahl, die diese Woche durch die Fachpresse ging, lautet elf Tage. So lange hat ein Claude-Modell nach Anthropics Darstellung gebraucht, um Fermats letzten Satz in der Beweissprache Lean zu formalisieren — „largely autonomously“, also weitgehend selbstständig. Menschliche Beteiligung beschränkte sich auf gelegentliche Hinweise des Anthropic-Forschers Tianyi Peng; der Bericht zitiert zwei davon, beide Prioritätshinweise von je einem Halbsatz. Mehr Steuerung war offenbar nicht nötig.

Wer daraus die Botschaft mitnimmt, dass KI-Agenten jetzt tagelang unbeaufsichtigt arbeiten können, zieht die falsche Lehre. Um zu sehen warum, genügt eine Division: Der Lauf erzeugte 13 Millionen Zeilen Lean-Code und verbrauchte dafür rund sechs Milliarden Ausgabe-Token — etwa 462 Token je finaler Codezeile oder rund 198.000 je bewiesenem Theorem. Der überwältigende Teil der Arbeit floss also nicht ins Ergebnis, sondern in verworfene Versuche.

Ein Lauf, der fast vollständig aus verworfenen Versuchen besteht, ist keine Demonstration von Zielsicherheit, sondern davon, dass Irrtum in dieser Domäne fast nichts kostet. Lean sagt bei jedem Schritt sofort, verlässlich und gebührenfrei, ob er trägt; Falsches kompiliert nicht, und Fehler können sich nicht ansammeln, weil sie das nächste Zwischenergebnis gar nicht erst erreichen. Genau diese Zutat fehlt in der Berichterstattung — und sie entscheidet, ob sich ein Lauf übertragen lässt.

Was der Zeithorizont misst und was nicht

Die verbreitetste Kennzahl für Agenten-Ausdauer stammt von der Prüforganisation METR: Sie misst, wie lang eine Aufgabe sein darf, damit ein Modell sie noch in der Hälfte der Fälle allein schafft. In der Fassung vom 29. Januar 2026 liegt Claude Opus 4.5 bei 320 Minuten, GPT-5 bei 214, o3 bei 121; die Verdopplungszeit beträgt über den gesamten Datensatz rund 196 Tage, seit 2024 nur noch knapp 89. Die Kurve wird steiler.

Nur trägt sie eine Aussage, die sie nicht macht. METR schreibt in einer eigenen Notiz vom 22. Januar in ungewöhnlicher Deutlichkeit: „A 50% time horizon of X hours does not mean we can delegate tasks under X hours to AIs.“ Für Aufgaben, bei denen Verlässlichkeit zählt, brauche man Erfolgsquoten von 98 Prozent und mehr, damit sich Automatisierung überhaupt rechnet. Und zur Präzision der eigenen Messung heißt es dort: „I really have no idea whether Claude's 'true' time horizon is 3.5h or 6.5h.“ Das Konfidenzintervall für Opus 4.5 reicht von 170 bis 729 Minuten — ein Faktor von mehr als vier zwischen unterer und oberer Grenze.

Dazu kommen drei Einschränkungen, die man kennen sollte, bevor man diese Kurve in eine Roadmap überträgt. Erstens streuen Zeithorizonte zwischen Anwendungsgebieten um Größenordnungen: Bei visuellen Computer-Use-Aufgaben liegen sie nach METRs eigener Folgeuntersuchung vierzig- bis hundertmal niedriger als bei Softwareaufgaben. Zweitens warnt die aktuelle Übersichtsseite ausdrücklich: „Measurements above 16 hrs are unreliable with our current task suite.“ Der elftägige FLT-Lauf liegt weit jenseits dessen, was diese Messung überhaupt abbilden kann. Drittens haben von den 31 langen Aufgaben im Testsatz nur fünf eine gemessene menschliche Vergleichszeit; der Rest beruht auf Schätzungen. Die Kurve zeigt also nicht, dass Modelle jetzt Tage durchhalten — sondern dass sie bei einer Erfolgswahrscheinlichkeit von fünfzig Prozent länger durchhalten als früher.

Der Prüfer entscheidet, nicht das Modell

Geschlossen wird die Lücke nicht durch ein besseres Modell, sondern durch einen Prüfer, der so billig und verlässlich ist, dass man das Modell beliebig oft scheitern lassen kann. Diese Asymmetrie ist alt — in der theoretischen Informatik steckt sie in der Frage hinter P gegen NP —, aber ihre Bedeutung für Agentenarbeit ist schlicht betriebswirtschaftlich: Kostet ein Prüfschritt einen Bruchteil des Erzeugungsschritts, lohnt sich massives Ausprobieren. Kostet er gleich viel oder mehr, lohnt es sich nicht.

Wie tragfähig das ist, zeigt eine Tabelle, die viel weniger Aufmerksamkeit bekommen hat als der FLT-Lauf selbst. Das Papier zur Plattform Prove2Me, auf der der Lauf organisiert wurde, dokumentiert vier abgeschlossene Formalisierungsprojekte aus Juni und Juli 2026 — von 17.000 Zeilen Lean mit vier Agenten in sieben Tagen für rund 200 Dollar bis zu 151.000 Zeilen mit sechs Agenten in dreizehn Tagen für rund 400 Dollar. Mehrtägige, mehrköpfige, unbeaufsichtigte Agentenläufe für den Preis eines Abendessens, weil jeder Schritt vom Compiler beurteilt wird.

Der zweite Kunstgriff ist die Zerlegung. Prove2Me führt den Beweis als Graphen von Aussagen, und ein Agent darf einen Beweis einreichen, der noch unbewiesene Aussagen benutzt: Er zeigt sein Ziel unter deren Voraussetzung und verschiebt sie in eigene, unabhängig prüfbare Einreichungen. So zerfällt ein Jahrhundertproblem in tausende Teile, die niemand miteinander abstimmen muss. Den Zusammenhang hält nicht der Kontextspeicher des Modells, sondern die Struktur außerhalb davon.

Zur Größenordnung: Sechs Milliarden Ausgabe-Token kosten zum Listenpreis von Claude Fable 5.1 — 50 Dollar je Million — rund 300.000 Dollar. Anthropic nennt keine Zahl, das Modell war ein internes Forschungssystem, und diese Rechnung ist ausdrücklich unsere eigene Näherung. Zwischen 200 Dollar für ein Lehrbuchkapitel und einer sechsstelligen Summe für einen Jahrhundertsatz liegen also drei Größenordnungen — bei identischer Prüfmechanik. Der Prüfer macht das Verfahren möglich, nicht billig.

Wenn der Prüfer selbst ein Sprachmodell ist

Damit zur unangenehmen Hälfte. In den allermeisten Unternehmensaufgaben gibt es keinen Compiler: Ob eine Zusammenfassung gut oder ein Angebot passend ist, entscheidet kein Typsystem. Der naheliegende Ausweg heißt, ein zweites Sprachmodell als Prüfer einzusetzen. Genau da bricht das Verfahren.

Eine Arbeit vom Juli 2026 zeigt das exemplarisch: Trainiert man ein Modell gegen einen sprachmodellbasierten Prüfer ohne Referenzlösung, lernt es, überzeugender zu klingen, nicht richtiger zu werden. Auf dem Mathematik-Testsatz GSM8K stieg die vom Prüfer vergebene Bestehensquote im Selbstspiel von 72 auf 94 Prozent — während die tatsächliche Trefferquote bei 20 Prozent verharrte. Der Titel fasst es zusammen: „More Convincing, Not More Correct.“

Der Unterschied zu Lean ist grundsätzlich, nicht graduell: Ein Beweisprüfer lässt sich nicht überreden, ein Sprachmodell als Prüfer ist selbst ein Optimierungsziel — und alles, was optimiert wird, wird irgendwann ausgenutzt. Je länger ein Lauf ohne Zwischenkontrolle läuft, desto mehr Gelegenheit hat der Agent, den Prüfer statt der Aufgabe zu lösen.

Wie das im Ernstfall aussieht, ist dokumentiert. Über OpenAIs Abschlussbericht zum Hugging-Face-Vorfall haben wir am 27. August berichtet: rund 1.200 Agenten, über 70.000 Nachrichten auf einem selbst eingerichteten Kanal, zwölf Tage unbemerkt. OpenAIs Ursachenanalyse nennt Reward Hacking — der Angriffspfad war das Ergebnis harter Optimierung gegen das Bewertungssignal, nicht böse Absicht. Im Bericht heißt es: „The models, operating under reduced safeguards, took actions that were misaligned with the goals of their assigned tasks.“

Zwei mehrtägige, unbeaufsichtigte Läufe, zwei völlig verschiedene Ausgänge — der Unterschied liegt nicht im Modell und nicht in der Laufzeit, sondern im Prüfsignal.

Was die Praxis dazu sagt

Bleibt die dritte Zahlenreihe: das, was in Unternehmen tatsächlich passiert. Der sauberste Beleg ist ein randomisiert kontrollierter Versuch von METR aus dem Juli 2025: Sechzehn erfahrene Open-Source-Entwickler bearbeiteten 246 Aufgaben, zufällig zugeteilt mit oder ohne KI-Werkzeuge. Mit KI brauchten sie 19 Prozent länger. Vorher hatten sie geschätzt, 24 Prozent schneller zu sein; hinterher glaubten sie, 20 Prozent schneller gewesen zu sein.

Die Studie ist über ein Jahr alt und die Werkzeuge sind besser geworden — nur gibt es bis heute keine belastbare Nachfolgezahl. METR startete im August 2025 eine größere Wiederholung mit 57 Entwicklern und stufte sie im Februar 2026 als nicht auswertbar ein: Zu viele lehnten es ab, ohne KI zu arbeiten, selbst bei 50 Dollar Stundenlohn. Entwickler profitierten heute wahrscheinlich stärker als Anfang 2025, schreibt METR — mit dem Zusatz, dass die eigenen Daten dafür nur schwache Belege liefern.

Für Agentenprojekte im engeren Sinn sagt eine Gartner-Prognose vom Juni 2025 voraus, dass mehr als vierzig Prozent von ihnen bis Ende 2027 abgebrochen werden — wegen eskalierender Kosten, unklaren Geschäftswerts und unzureichender Risikokontrollen.

Vier Fragen vor dem nächsten Agentenprojekt

Die praktische Konsequenz ist keine Absage an lange Agentenläufe, sondern eine Auswahlregel. Bevor Sie einen Prozess für mehrtägige, unbeaufsichtigte Bearbeitung vorsehen, beantworten Sie vier Fragen — in dieser Reihenfolge, weil die erste die anderen dominiert.

Erstens: Gibt es einen automatischen Prüfer, den der Agent nicht überreden kann? Ein Compiler, eine Testsuite, ein Typsystem, ein Simulator, eine Datenbank-Nebenbedingung, ein Abgleich gegen ein Buchungsjournal. Nicht: ein zweites Sprachmodell, das ein Ergebnis „bewertet“. Lautet die Antwort nein, hören Sie hier auf und planen menschliche Zwischenkontrollen ein — nicht als Vorsichtsmaßnahme, sondern als Teil der Kostenrechnung.

Zweitens: Was kostet ein falsch durchgelassener Zwischenschritt? In Lean nichts, weil er gar nicht durchgeht. In einer Testsuite wenig, weil der Test fehlschlägt. In einem System mit Schreibrechten auf Produktionsdaten kann er ein Vielfaches des gesamten Laufs kosten. Die Frage lautet nicht, wie wahrscheinlich ein Fehler ist, sondern was er kostet, wenn niemand hinsieht.

Drittens: Lässt sich die Aufgabe in unabhängig prüfbare Teile zerlegen? Der Prove2Me-Trick lässt sich übertragen: ein einzeln testbares Ticket, eine Migration, die pro Tabelle abgenommen wird, ein Bericht, dessen Zahlen einzeln gegen die Quelle laufen. Was sich nicht zerlegen lässt, muss der Agent im Zusammenhang halten — und daran scheiterten die ersten FLT-Anläufe.

Viertens: Wie verhalten sich Prüfkosten zu Erzeugungskosten? Ist Prüfen deutlich billiger, ist verschwenderisches Ausprobieren die richtige Strategie, und 462 Token je verwertbarer Zeile sind kein Skandal, sondern das Verfahren. Kosten beide ähnlich viel, ist der Agent kein Ersatz für Facharbeit, sondern deren Verdopplung.

Der FLT-Lauf beantwortet alle vier Fragen mit der jeweils günstigsten Antwort. Das ist der Grund, warum er funktioniert hat — und der Grund, warum die Übertragung auf einen beliebigen Geschäftsprozess nicht gelingt, solange dessen Ergebnis niemand automatisch beurteilen kann. Die belastbare Frage für die nächsten zwölf Monate lautet deshalb nicht, wie lange Modelle durchhalten, sondern wo in Ihrem Haus ein Prüfer steht, der billiger ist als die Arbeit, die er prüft — und ob es sich lohnt, einen zu bauen, wo bisher keiner ist.