Agentisches Refactoring mit Strategie-Index statt Feinabstimmung

Von Sprachmodellen erzeugte Beweise in Lean sind zwar korrekt, aber üblicherweise umständlich und empfindlich gegenüber Versionswechseln der Bibliothek. Wer sie aufräumen will, verfolgt drei Ziele, die einander in die Quere kommen: kurze Beweise, geringe Kompilierzeit und Verträglichkeit mit einer bestimmten Lean- beziehungsweise Mathlib-Version. Erschwerend kommt hinzu, dass Modelle nichts über den Versionsstand wissen, gegen den sie gerade schreiben — und dass eine trainierte Lösung mit jedem neuen Modell und jedem neuen Lean-Release erneut angepasst werden müsste.

Der Prototyp Lean Refactor geht den anderen Weg und lässt das Modell unangetastet. Das Wissen liegt daneben, in einer kuratierten Sammlung von Refactoring-Strategien. Jeder Eintrag trägt Metadaten: welche Lean- und Mathlib-Versionen er abdeckt, welche Ersparnis bei der Kompilierzeit zu erwarten ist. Der Agent zieht sich zur Laufzeit die passenden Einträge heran, gefiltert auf die Zielversion.

Die Arbeit berichtet über 70 Prozent weniger Tokens bei Beweisen aus Wettbewerbsaufgaben, über 20 Prozent in Forschungs-Repositories und bis zu 60 Prozent kürzere Kompilierzeit — nach eigener Messung besser als vorherige Ansätze und als Claude Code. Aufgeräumte Beweise übertragen sich zudem zuverlässiger auf spätere Lean-Versionen als die ursprünglichen.

Einordnung

Beweisassistenten sind ein enges Feld, das Muster dahinter ist es nicht. Jedes Projekt mit schnell wandernden Abhängigkeiten kennt denselben Effekt: Der Agent schreibt sauberen Code gegen die API vom vorletzten Jahr. Die übliche Antwort lautet Feinabstimmung und ist teuer, weil sie bei jedem Modellwechsel von vorn beginnt. Die Alternative hier — Wissen als versionierte, durchsuchbare Einträge neben einem unveränderten Modell — lässt sich mit Bordmitteln nachbauen und altert kontrollierter.

Der Preis steht in derselben Zeile: Jemand muss diese Einträge schreiben, annotieren und pflegen; die Metadaten sind die eigentliche Arbeit und veralten ihrerseits. Die Zahlen stammen aus einem Preprint ohne Begutachtung, der Vergleich richtet sich gegen Werkzeuge, deren Stand sich wöchentlich verschiebt. Belastbar ist weniger der Vorsprung als die Bauweise.