Lean Refactor: Multi-objectieve controleerbare bewijsoptimalisatie via agentische strategiezoektocht

Samenvatting

We presenteren Lean Refactor, een plug-and-play retrieval-versterkt agentisch raamwerk voor multi-objectieve, controleerbare en versie-robuuste refactoring van Lean-bewijzen. LLM-gegenereerde bewijzen zijn berucht correct-maar-uitgebreid en breekbaar over bibliotheekversies heen, maar bestaande refactoringwerken zien drie praktische uitdagingen over het hoofd: 1) Lean-refactoring is van nature multi-objectief (bewijslengte, compilatiekosten en versiecompatibiliteit staan vaak op gespannen voet); 2) Lean-repositories hebben kwetsbare compatibiliteit, terwijl LLM-releases zich niet bewust zijn van Lean/Mathlib-versies; 3) Op training gebaseerde pijplijnen vereisen herhaalde fine-tuning bij elke nieuwe LLM-release en schalen noch met modelwisselingen noch met de releasecyclus van Lean. Lean Refactor stuurt een bevroren agentische LLM met ophaalacties uit een samengestelde database van multi-objectieve refactoringstrategieën, elk dicht geannoteerd met metadata zoals ondersteunde Lean/Mathlib-versies en verwachte vermindering van compilatiekosten. Experimenten tonen meer dan 70% compressie op token-niveau op competitiebenchmarks, meer dan 20% op onderzoeksrepositories en tot 60% vermindering van compilatietijd, waarmee eerdere werken en Claude Code worden overtroffen. Versie-gefilterde ophaling verbetert verder de compressie op de beoogde Lean-versie, en gerefactorde miniF2F-bewijzen vertonen sterkere zero-shot versieoverdracht naar toekomstige Lean-releases dan hun ongerefactorde tegenhangers.

English

We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. LLM-generated proofs are notoriously correct-but-verbose and brittle across library versions, yet existing refactoring works overlook three practical challenges: 1) Lean refactoring is natively multi-objective (proof length, compilation cost, and version compatibility are often in tension); 2) Lean repositories have fragile compatibility, whereas LLM releases are unaware of Lean/Mathlib versions; 3) Training-based pipelines require repeated fine-tuning with each new LLM release, scaling neither with model churn nor with Lean's release cycle. Lean Refactor steers a frozen agentic LLM with retrievals from a curated database of multi-objective refactoring strategies, each densely annotated with metadata such as supported Lean/Mathlib versions and expected compilation-cost reduction. Experiments show over 70% token-level compression on competition benchmarks, over 20% on research repositories, and up to 60% compilation-time reduction, outperforming prior work and Claude Code. Version-filtered retrieval further improves compression on the target Lean version, and refactored miniF2F proofs exhibit stronger zero-shot version transfer to future Lean releases than their unrefactored counterparts.