Lean Refactor : Optimisation contrôlable multi-objectif de preuves par recherche agentique de stratégies

Résumé

Nous présentons Lean Refactor, un cadre agentique prêt à l'emploi augmenté par recherche pour le refactoring multi-objectif, contrôlable et robuste aux versions des preuves Lean. Les preuves générées par LLM sont notoirement correctes mais verbeuses et fragiles face aux versions de bibliothèques, pourtant les travaux existants sur le refactoring négligent trois défis pratiques : 1) Le refactoring Lean est naturellement multi-objectif (la longueur de la preuve, le coût de compilation et la compatibilité de version sont souvent en tension) ; 2) Les dépôts Lean présentent une compatibilité fragile, tandis que les versions de LLM ignorent les versions de Lean/Mathlib ; 3) Les pipelines basés sur l'entraînement nécessitent un réglage fin répété à chaque nouvelle version de LLM, ne passant à l'échelle ni avec le renouvellement des modèles ni avec le cycle de publication de Lean. Lean Refactor oriente un LLM agentique figé à l'aide de recherches dans une base de données organisée de stratégies de refactoring multi-objectif, chacune densément annotée avec des métadonnées telles que les versions de Lean/Mathlib supportées et la réduction attendue du coût de compilation. Les expériences montrent une compression de plus de 70 % au niveau des tokens sur les bancs d'essai de compétition, plus de 20 % sur les dépôts de recherche, et une réduction du temps de compilation allant jusqu'à 60 %, surpassant les travaux antérieurs et Claude Code. La recherche filtrée par version améliore en outre la compression sur la version cible de Lean, et les preuves miniF2F refactorisées présentent un transfert de version zero-shot plus fort vers les futures versions de Lean que leurs homologues non refactorisés.

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.