Lean Refactor: Otimização Controlável de Provas Multiobjetivo via Busca de Estratégias com Agentes

Resumo

Apresentamos o Lean Refactor, um framework agêntico aumentado por recuperação plug-and-play para refatoração multiobjetivo, controlável e robusta a versões de provas em Lean. Provas geradas por LLMs são notoriamente corretas, mas prolixas e frágeis entre versões de bibliotecas; no entanto, os trabalhos existentes de refatoração ignoram três desafios práticos: 1) a refatoração em Lean é nativamente multiobjetivo (comprimento da prova, custo de compilação e compatibilidade de versões frequentemente estão em conflito); 2) repositórios em Lean apresentam compatibilidade frágil, enquanto os lançamentos de LLMs desconhecem as versões de Lean/Mathlib; 3) pipelines baseados em treinamento exigem ajuste fino repetido a cada novo lançamento de LLM, não escalando nem com a rotatividade de modelos nem com o ciclo de lançamento do Lean. O Lean Refactor direciona um LLM agêntico congelado com recuperações de uma base de dados curada de estratégias de refatoração multiobjetivo, cada uma densamente anotada com metadados como versões suportadas de Lean/Mathlib e redução esperada do custo de compilação. Experimentos mostram mais de 70% de compressão em nível de tokens em benchmarks de competição, mais de 20% em repositórios de pesquisa e até 60% de redução no tempo de compilação, superando trabalhos anteriores e o Claude Code. A recuperação filtrada por versão melhora ainda mais a compressão na versão alvo do Lean, e provas refatoradas do miniF2F exibem transferência de versão zero-shot mais robusta para lançamentos futuros do Lean do que suas contrapartes não refatoradas.

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.