Technische Samenvatting: Optimalisatie van de Kosten-Kwaliteit-Afweging van Agentische Theoreembewijzers in Lean

Probleemstelling

Large language models (LLM's) hebben aanzienlijke vooruitgang geboekt in geautomatiseerd bewijs binnen de Lean proof assistant door het gebruik van agentische workflows. Deze workflows deconstrueren complexe problemen doorgaans in kleinere lemma's, genereren talrijke bewijspogingen en maken gebruik van compiler-feedback om de zoektocht te sturen. Hoewel deze aanpak hoge prestaties levert op uitdagende benchmarks zoals PutnamBench, lijdt het onder prohibitieve computationele kosten. Huidige systemen alloceren vaak vaste, vooraf gespecificeerde budgetten voor decompositie en bewijsgeneratie aan elk probleem, ongeacht de moeilijkheidsgraad. Dit "fixed-step" beleid leidt tot aanzienlijke verspilling, aangezien agenten vaak aanzienlijke rekenkracht besteden aan onhaalbare problemen of foutief geformaliseerde stellingen die onwaarschijnlijk succesvol zullen zijn. De kernuitdaging die wordt geadresseerd is het gebrek aan dynamische kostenbewustheid in bestaande agenten, die er niet in slagen de afweging tussen computationele uitgaven en de succesratio van bewijzen te optimaliseren.

Methodologie

De auteurs stellen een nieuwe Action Routing Agent architectuur voor, ontworpen om statische policies te vervangen door dynamische, datagestuurde routeringsbeslissingen. Het systeem is conceptueel verdeeld in twee vlakken:

1. Datavlak (Bewijsgeneratie)

Geïnspireerd door eerder werk (bijv. Chen et al., 2025c; Varambally et al., 2025), handelt het datavlak de feitelijke generatie van bewijzen af. Het opereert via vier modules:

• Breakdown Module: Een algemeen model (GPT-OSS-20B) deconstrueert het oorspronkelijke probleem in natuurlijke taal lemma's en bewijs-schetsen.
• Formalizer: De agent formaliseert deze lemma's naar Lean-code met behulp van GOEDEL-FORMALIZER-V2-8B, waarbij de beste kandidaat wordt geselecteerd die compileert zonder syntactische of typefouten.
• Formal Breakdown Prover: Het systeem probeert het bovenliggende theorema te bewijzen met behulp van de geformaliseerde lemma's als axioma's, gestuurd door de natuurlijke taal schets.
• Lemma Prover: Zodra de breakdown bewezen is, probeert de agent recursief de individuele lemma's te bewijzen die vereist zijn voor het bewijs, waarbij nieuwe afhankelijkheden op een stack worden geplaatst.

2. Controlevlak (Kosten-Kwaliteit Routering)

Het controlevlak observeert het traject van mislukte bewijs-pogingen en besluit of de huidige doelstelling moet worden voortgezet of dat het traject moet worden beëindigd om te herstarten met een nieuwe breakdown. Het maakt gebruik van een lichtgewicht routeringsbeleid gebaseerd op een kosten-kwaliteit afweging:

• Toestand ($s$): Vat de geschiedenis van mislukte pogingen samen, inclusief bewijs-pogingen, compileringsresultaten, foutmeldingen en output-lengtes.
• Actieruimte: $\{ \text{ATTEMPT}, \text{TERMINATE} \}$. De agent probeert ofwel een ander bewijs voor de huidige doelstelling, of verwerpt de huidige breakdown.
• Nutfunctie: De router berekent een nutsscore $\tau(s) = \hat{q}(s) - \lambda\hat{c}(s)$, waarbij:
  • $\hat{q}(s)$ de voorspelde waarschijnlijkheid van succes voor de volgende poging is (Kwaliteit).
  • $\hat{c}(s)$ de voorspelde kosten van de volgende poging is (gemeten in LLM-generatie tokens/SFLOPs).
  • $\lambda$ een hyperparameter is die de straf voor computationele kosten reguleert.
• Beslisregel: Als $\tau(s) > 0$, gaat de agent door; anders, beëindigt hij de huidige trajectorie.

Estimators:

• Kosten Estimator: Gaat ervan uit dat de kosten van pogingen onafhankelijk en identiek verdeeld zijn, gebruikmakend van de gemiddelde kosten van voorgaande pogingen in het traject.
• Kwaliteit Estimator: Een logistische regressie die getraind is om de succeswaarschijnlijkheid te voorspellen op basis van traject-kenmerken, specifiek:
  • Bewijs Gelijkenis: De gemiddelde pairwise fuzzy string ratio van genormaliseerde bewijzen (lage gelijkenis suggereert verwarring).
  • Fout Diversiteit: De ratio van unieke compileringsfouten tot het totaal aantal fouten (lage diversiteit suggereert een hardnekkige foutmodus).
  • Pogingsaantal: Het aantal voorgaande pogingen.

Belangrijkste Bijdragen

1. Identificatie van Inefficiëntie: Het artikel identificeert dat fixed-step schaling in Lean-agenten kritiek inefficiënt is en dat het verminderen van onnodige pogingen essentieel is voor een betere kosten-kwaliteit afweging.
2. Nieuwe Architectuur: De ontwikkeling van een lemma-stijl Lean prover uitgerust met een online, adaptieve kosten-kwaliteit router die dynamisch de marginale waarde van extra rekenkracht evalueert.
3. Empirische Validatie: Demonstratie dat de voorgestelde router de verspilde rekenkracht aanzienlijk vermindert terwijl de competitieve nauwkeurigheid behouden blijft, wat bewijst dat mislukte trajecten acteerbare signalen bevatten voor middelenallocatie.

Experimentele Resultaten

Het systeem werd geëvalueerd op een subset van 85 problemen uit PutnamBench, waarbij de dynamische routeringsagent werd vergeleken met een fixed-step baseline en een "oracle" agent met toegang tot grondwaarheid succes-waarschijnlijkheden.

• Kostenreductie: Bij een gelijkwaardige nauwkeurigheid verminderde de voorgestelde agent het benodigde budget gemiddeld met 25,8% vergeleken met de fixed-step baseline.
• Verbetering van Nauwkeurigheid: Bij een gelijkwaardige kostenstructuur bereikte de agent een verbetering van 7,8% in de solve rate.
• Specifieke Afwegingen:
  • Om een solve rate van ~43,6% te bereiken, had de fixed-step baseline 31,6 M SFLOPs nodig, terwijl de routeringsagent slechts 22,6 M SFLOPs vereiste (een kostenreductie van 28,4%).
  • In een medium-budget regime (~41,6% solve rate), verminderde de agent de kosten met 29,6% (17,5 M vs. 24,9 M SFLOPs).
• Ablatie Studies:
  • Kenmerk Belang: "Fout diversiteit" werd gevonden als het meest kritieke kenmerk voor kwaliteitschatting.
  • Impact van Datavlak: De lemma-stijl decompositie architectuur zelf verbeterde de solve rate met bijna 100% ten opzichte van een whole-proof generatie aanpak met dezelfde 8B model, waarbij het de prestaties van een 32B model benaderde.
  • Oracle Gat: Hoewel de routeringsagent de fixed baseline aanzienlijk overtrof, blijft er een gat bestaan vergeleken met de oracle agent (die een 59,9% kostenreductie bereikte), wat wijst op ruimte voor verbetering in feature engineering en estimator architectuur.

Betekenis en Claims

Het artikel claimt dat mislukte Lean trajecten acteerbare signalen bieden voor kostenbewuste middelenallocatie in agentische theoreem bewijzing. Door af te stappen van statische, fixed-step policies naar dynamische routering, kunnen agenten de computationele verspilling aanzienlijk verminderen zonder prestaties op te offeren. De auteurs positioneren dit werk als een fundamentele stap naar "kostenbewuste controle" voor formeel wiskundig bewijzen, waarbij zij suggereren dat toekomstige agenten de berekening dynamisch moeten alloceren op basis van geobserveerde progressie en foutpatronen in plaats van inferentie-budgetten statisch toe te wijzen. De resultaten geven aan dat fixed-step policies substantiële ruimte laten voor efficiëntieverbeteringen, en dat routeringsstrategieën effectief onnodige kosten kunnen mitigeren.