💻 computer science

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search

Lean Refactor is een retrieval-augmented agentic framework dat Lean-bewijzen optimaliseert voor meerdere doelen, waaronder tokencompressie, compilatiesnelheid en versiecompatibiliteit, door dynamisch gecureerde refactoringsstrategieën te selecteren zonder dat modelhertraining vereist is.

Oorspronkelijke auteurs: Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang, Weiran Sun, Wuyang Chen

Gepubliceerd 2026-05-21

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang, Weiran Sun, Wuyang Chen

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Het Probleem: Het "Over-geoptimaliseerde" Bewijs

Stel je een briljante maar overdreven enthousiaste architect (de AI) voor die net een huis heeft gebouwd (een wiskundig bewijs). Het huis is structureel veilig – het valt niet om en het slaat alle veiligheidsinspecties. De architect heeft echter 500 bakstenen gebruikt om een muur te bouwen waarvoor slechts 50 nodig waren. Ze hebben een sloopkogel gebruikt om een noten te kraken.

In de wereld van Lean (een taal die wordt gebruikt om wiskundige bewijzen te schrijven die door computers kunnen worden geverifieerd), produceren AI-modellen vaak bewijzen die correct zijn, maar ongelooflijk lang, rommelig en traag om te compileren.

Te lang: Het bewijs is moeilijk leesbaar voor mensen.
Te traag: Omdat het bewijs vol zit met onnodige stappen, duurt het lang voordat de computer controleert of het geldig is.
Fragiel: De Lean-taal verandert regelmatig (zoals software-updates). Een bewijs geschreven voor "Versie 1.0" kan volledig kapotgaan wanneer de computer upgradet naar "Versie 2.0", zelfs als de wiskunde nog steeds klopt.

Bestaande tools probeerden dit op te lossen door de AI opnieuw te trainen (wat duur en traag is) of door haar simpelweg te vragen "korter te zijn" (wat vaak het bewijs trager maakt om uit te voeren).

De Oplossing: Het "Slimme Bibliothecaris"-systeem

De auteurs creëerden Lean Refactor. In plaats van de AI opnieuw te trainen, bouwden ze een "plug-and-play"-systeem dat fungeert als een super-slimme bibliothecaris voor de AI.

Hier is hoe het werkt, gebruikmakend van een metafoor:

1. De Strategiebank (De Bibliotheek)

Stel je een enorme bibliotheek voor gevuld met "Refactoring-kaarten". Elke kaart beschrijft een specifieke truc om een bewijs te verkorten.

De Truc: "In plaats van elk getal één voor één op te sommen, gebruik deze ene magische formule."
De Metadata: Cruciaal is dat elke kaart een label heeft. Het zegt:
- Hoeveel tijd bespaart dit? (bijv. "Bespaart 30% compilatietijd").
- Op welke versie van de taal werkt dit? (bijv. "Werkt op Lean v4.16 en v4.22").
- Hoeveel korter maakt het het bewijs?

Het paper beweert dat ze de grootste bibliotheek ooit van deze kaarten hebben gebouwd, met meer dan 9.000 unieke strategieën die zijn afgeleid uit honderdduizenden bewijsvoorbeelden.

2. De Agent (De Architect + De Bibliothecaris)

Wanneer de AI een bewijs moet repareren, gokt ze niet. Ze volgt een lus:

De Planner: De AI kijkt naar het rommelige bewijs en zegt: "Dit gedeelte lijkt een 'Magische Formule'-truc nodig te hebben."
De Bibliothecaris (Retrieval): Het systeem gaat naar de bibliotheek en pakt de specifieke kaarten die bij dat gedeelte passen.
- Als je het kortste bewijs wilt: Het pakt kaarten die de grootste grootte-reductie beloven.
- Als je de snelste compilatie wilt: Het pakt kaarten die de grootste snelheidswinst beloven.
- Als je een oude versie van Lean gebruikt: Het filtert alle kaarten weg die niet werken op jouw versie.
De Refactorer: De AI past de truc van de kaart toe om het bewijs te herschrijven.
De Debugger: De computer controleert het nieuwe bewijs. Als het stuk gaat, probeert de AI de fout lokaal op te lossen zonder de hele verbetering ongedaan te maken.

Waarom Dit Speciaal Is (De Claims van het Paper)

1. Het balanceert concurrerende doelen (De "Multi-Doel"-Magie)
Meestal moet je kiezen: "Wil ik dat het bewijs kort is, of wil ik dat het snel compileert?"

Oude Manier: Je kiest er één, en het andere lijdt eronder.
Lean Refactor: Je kunt het systeem vertellen: "Ik wil het kort, maar ook snel." Het systeem kijkt naar de bibliotheekkaarten, ziet welke beide bieden, en kiest de beste balans.
Resultaat: Bij wiskundewedstrijden verkortten ze bewijzen met meer dan 70% en verkleinden ze de compilatietijd met meer dan 60%.

2. Het overleeft software-updates (De "Versie-Robuustheid")
Omdat de bibliotheekkaarten zijn gelabeld met de specifieke softwareversies waarvoor ze werken, kan het systeem direct "verouderde" trucs filteren.

Resultaat: Als je om een bewijs vraagt voor "Lean v4.16", gebruikt het systeem alleen kaarten die werken voor v4.16. Dit voorkomt dat de AI hallucineert (uitvindt) tools die in die versie niet bestaan.

3. Het werkt met elke AI (De "Model-Onafhankelijke" Eigenschap)
Je hoeft geen nieuwe AI te trainen voor dit doel. Het systeem werkt met elk "bevroren" (voorgetraind) AI-model, of het nu van Google (Gemini), Anthropic (Claude) of OpenAI (GPT) is. De "intelligentie" komt uit de bibliotheek van strategieën, niet uit het brein van de AI.

Resultaat: Ze testten het op verschillende AI-modellen, en het verbeterde de prestaties van allemaal, zelfs een gespecialiseerd coderingsagent genaamd "Claude Code" verslaan.

De Conclusie

Lean Refactor is als een bouwteam een set blauwdrukken en een gereedschapskist met voorgeteste, gelabelde shortcuts geven. In plaats van te gokken hoe ze een huis moeten bouwen, kijken ze op de beste manier om een specifieke muur te bouwen, gebaseerd op de gereedschappen die ze hebben en de versie van de bouwcode die ze gebruiken.

Het paper beweert dat deze aanpak:

Bewijzen verkort met 70%+ bij wiskundewedstrijden.
Ze 60% sneller laat compileren.
Ze werkend houdt, zelfs wanneer de programmeertaal update.
Dit allemaal doet zonder de AI-modellen opnieuw te hoeven trainen.

Technische Samenvatting: Lean Refactor

Probleemstelling

Grote Taalmodellen (LLMs) die met versterkingsleer (RL) zijn getraind voor formeel stellingenbewijs in Lean, genereren vaak bewijzen die correct zijn, maar berucht zijn om hun omvang, broosheid en hoge rekenkosten. Hoewel er bestaande refactoringsinspanningen zijn, lopen deze tegen drie fundamentele beperkingen aan wanneer ze worden toegepast op het Lean-ecosysteem:

Spanning tussen meerdere doelen: Lean-refactoring is inherent multi-objectief. Het optimaliseren voor bewijslengte botst vaak met het minimaliseren van compilatiekosten (bijvoorbeeld: kortere bewijzen kunnen zware tactieken oproepen die de compilatietijd doen toenemen), en bestaande methoden missen principiële mechanismen om deze afwegingen in evenwicht te brengen of zich aan te passen aan onbekende gebruikersdoelen tijdens de inferentie.
Versiefragiliteit: Lean en zijn standaardbibliotheek, Mathlib, evolueren op bijna wekelijkse basis met frequente API-wijzigingen en hernoemingen van lemma's. Frontier-LLMs hebben statische kennis-cutoffs, wat leidt tot hallucinaties van verouderde tactieken en incompatibiliteit met huidige toolchains.
Data-schaarste: In tegenstelling tot mainstream programmeertalen ontbreekt het Lean aan grote, gekoppelde datasets (ruisige-schone codeparen) die nodig zijn voor op training gebaseerde refactoringspijplijnen. Bovendien vereisen op training gebaseerde benaderingen herhaaldelijke fine-tuning voor elke nieuwe LLM-release, waardoor ze niet schalen met modelwisselingen of het release-cyclus van Lean.

Methodologie: Lean Refactor

De auteurs stellen Lean Refactor voor, een plug-and-play, retrieval-versterkt agentiek framework dat is ontworpen om Lean-bewijzen te refactoren zonder de onderliggende LLM te fine-tunen. Het systeem ontkoppelt refactoringslogica van het model door kennis te externaliseren naar een gestructureerde, dicht geannoteerde database.

1. Dicht Geannoteerde Strategiebank

De kern van het framework is een curatie database van 9.237 unieke refactoringsstrategieën die zijn gedistilleerd uit meer dan 200.000 lange-korte bewijsparen.

Structuur: Elke strategie bevat een titel, beschrijving, preconditie ("wanneer toe te passen"), stap-voor-stap toepassingsgids en abstracte voor/na-voorbeelden.
Metadata: Cruciaal is dat elke strategie is geannoteerd met metadata die de LLM niet kan afleiden uit trainingsdata:
- Compilatietijd-reductie: De mediaan relatieve versnelling die wordt waargenomen bij toepassing van de strategie.
- Versiecompatibiliteit: Een set gevalideerde Lean/Mathlib-toolchains (bijv. v4.14.0, v4.16.0, v4.22.0) waaronder het gerefactoreerde bewijs succesvol compileert. Dit wordt bepaald door de ingekorte bewijzen opnieuw te compileren over meerdere versies.

2. Multi-Objectief Retrieval en Reranking

Tijdens inferentie hanteert het framework een retrievalpijplijn die zich aanpast aan door de gebruiker gespecificeerde doelen zonder modelhertraining:

Kortste bewijs: Haalt strategieën op puur op basis van semantische gelijkenis (cosine-gelijkenis) met het bewijssegment.
Compilatietijd-bewust: Haalt een brede pool semantisch vergelijkbare kandidaten op en rerankt deze vervolgens op basis van de geannoteerde metadata voor compilatiekostenreductie.
Versiespecifiek: Filtert de kandidatenpool zodat deze alleen strategieën bevat wiens compatibiliteitsmetadata de door de gebruiker beoogde Lean-versie omvat.

3. Agentieke Lus

Het framework omhult deze componenten in een model-onafhankelijke agentlus die bestaat uit:

Planner: Deconstrueert de refactoringsopdracht in specifieke stappen op basis van opgehaalde strategieën.
Refactorer: Voert het plan uit om een korter bewijs te genereren.
Debugger: Gebruikt compilerfeedback om fouten te herstellen in een gesloten lus (tot $D$ rondes).
Backbone-onafhankelijkheid: De planner, refactorer en debugger kunnen worden geïnstancieerd door elke bevroren frontier-LLM (bijv. Gemini, Claude, GPT-serie), waardoor het systeem zonder hertraining over modellen kan worden overgedragen.

Belangrijkste Bijdragen

Dataset-release: De auteurs publiceren de grootste Lean-refactoringdataset tot nu toe, bestaande uit meer dan 200K lange-korte bewijsparen en 9K refactoringsstrategieën, elk geannoteerd met compilatiekosten en versiecompatibiliteit.
Prestaties: Lean Refactor bereikt >70% token-niveau compressie op competitie-benchmarks (miniF2F, PutnamBench) en >20% op onderzoeksrepository's (Analysis, FLT, PhysLean). Het reduceert ook de compilatietijd met tot 60% op competitie-benchmarks.
Controleerbaarheid en Robuustheid: Het systeem ondersteunt multi-objectief beheer (lengte versus snelheid versus compatibiliteit) via retrievalregels in plaats van modelgewichten. Gerefactoreerde bewijzen vertonen een sterkere zero-shot versie-overdracht naar toekomstige Lean-releases in vergelijking met niet-gerefactoreerde tegenhangers en eerdere optimalisatiemethoden.
Model-onafhankelijkheid: Het framework verbetert de prestaties over verschillende LLM-backbones (Gemini 3 Flash, Claude Haiku 4.5) en presteert beter dan algemene coderingsagenten zoals Claude Code, zelfs wanneer laatstgenoemde toegang krijgt tot hetzelfde strategie-retrievalhulpmiddel.

Experimentele Resultaten

Lengtereductie: Op competitie-benchmarks presteert Lean Refactor beter dan de vorige state-of-the-art, ProofOptimizer, met een reductie van 88,40% op miniF2F en 70,38% op PutnamBench (tegenover 57,20% voor ProofOptimizer). Op bewijzen op onderzoeksniveau bereikt het een gemiddelde reductie van 20–33%, wat aanzienlijk beter is dan ablatie-baselines.
Compilatietijd: Door strategieën te reranken op basis van compilatiekosten-metadata, bereikt het framework een 42,62% relatieve reductie in compilatietijd op PutnamBench, vergeleken met 37,11% voor de standaard retrievalbenadering.
Versiecompatibiliteit: Bij het richten op specifieke Lean-versies (bijv. v4.16.0) levert versie-gefilterde retrieval consistent betere lengtereductie op dan ongefilterde retrieval. Gerefactoreerde bewijzen behouden hun typecontrolecapaciteit over meer toekomstige Lean-releases (tot v4.29.0) dan die geproduceerd door ProofOptimizer of de originele omvangrijke bewijzen.
Afname van afhankelijkheden: De gerefactoreerde bewijzen verminderen externe en intra-project afhankelijkheden in 42–67% van de gevallen, wat wijst op echte logische vereenvoudiging in plaats van louter uitbesteding aan zware bibliotheeklemma's.

Betekenis

Het artikel betoogt dat Lean Refactor de kritieke knelpunten adresseert bij het onderhouden van formele wiskundige bibliotheken: de spanning tussen bewijsconcisie en compilatie-efficiëntie, en de fragiliteit van code over snel evoluerende toolchains. Door refactoringskennis te externaliseren naar een metadata-rijke strategiebank, maakt het framework controleerbare, multi-objectief optimalisatie mogelijk zonder de noodzaak van dure model-fine-tuning. Deze aanpak stelt het systeem in staat om robuust te blijven tegenover Lean/Mathlib-versiedrift en direct aanpasbaar te zijn aan nieuwe LLM-backbones, waardoor de grondslag wordt gelegd voor meer onderhoudbare en versie-resiliente formele bewijzen.