Lean Refactor: 通过代理策略搜索实现多目标可控的证明优化
Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
AI总结：
本文提出Lean Refactor框架，通过检索增强的代理策略搜索，解决多目标、可控和版本鲁棒的Lean证明重构问题，主要贡献是通过预注释的多目标重构策略数据库实现高效的证明优化。
摘要：
我们提出了Lean Refactor，一个插件式的检索增强型代理框架，用于多目标、可控和版本鲁棒的Lean证明重构。LLM生成的证明虽然正确但冗长且易碎，现有重构工作忽视了三个实际挑战：1）Lean重构本质上是多目标的（证明长度、编译成本和版本兼容性常存在矛盾）；2）Lean仓库具有脆弱的兼容性，而LLM发布不了解Lean/Mathlib版本；3）基于训练的流水线需要每次新LLM发布时重复微调，无法随模型变化或Lean发布周期扩展。Lean Refactor通过检索预注释的多目标重构策略数据库中的冻结代理LLM，每个策略都密集注释了元数据，如支持的Lean/Mathlib版本和预期的编译成本减少。实验显示在竞争基准上压缩超过70%的token级别，在研究仓库上压缩超过20%，并达到高达60%的编译时间减少，优于先前工作和Claude Code。版本过滤检索进一步提高了目标Lean版本的压缩效果，重构后的miniF2F证明在零样本版本迁移至未来Lean发布时表现优于未重构的对应物。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
