Lean Refactor: Optimización de Pruebas Controlable Multiobjetivo mediante Búsqueda de Estrategias Basada en Agentes

Resumen

Presentamos Lean Refactor, un marco agéntico plug-and-play aumentado por recuperación para la refactorización multiobjetivo, controlable y robusta ante versiones de pruebas de Lean. Las pruebas generadas por LLM son notoriamente correctas pero verbosas y frágiles entre versiones de bibliotecas, sin embargo, los trabajos existentes de refactorización pasan por alto tres desafíos prácticos: 1) la refactorización de Lean es inherentemente multiobjetivo (la longitud de la prueba, el costo de compilación y la compatibilidad de versiones a menudo están en tensión); 2) los repositorios de Lean tienen compatibilidad frágil, mientras que las versiones de LLM desconocen las versiones de Lean/Mathlib; 3) los pipelines basados en entrenamiento requieren un ajuste fino repetido con cada nueva versión de LLM, no escalando ni con la rotación de modelos ni con el ciclo de versiones de Lean. Lean Refactor dirige un LLM agéntico congelado con recuperaciones de una base de datos curada de estrategias de refactorización multiobjetivo, cada una densamente anotada con metadatos como las versiones de Lean/Mathlib compatibles y la reducción esperada del costo de compilación. Los experimentos muestran más del 70% de compresión a nivel de tokens en puntos de referencia de competición, más del 20% en repositorios de investigación, y hasta un 60% de reducción del tiempo de compilación, superando trabajos anteriores y Claude Code. La recuperación filtrada por versión mejora aún más la compresión en la versión de Lean objetivo, y las pruebas miniF2F refactorizadas exhiben una transferencia de versión zero-shot más fuerte a versiones futuras de Lean que sus contrapartes no refactorizadas.

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.