用检索增强的智能体框架，自动优化数学证明代码长度与兼容性。
Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
- 通过检索多目标重构策略库，控制生成更短、更快、兼容性更强的证明。
- 在竞赛数据集上压缩率超70%，编译时间减少最高60%。
- 适合需要跨版本稳定维护数学证明库的研究者与开发者。
我们提出 Lean Refactor，一个即插即用的检索增强型智能体框架，用于实现多目标、可控且对版本变化鲁棒的 Lean 证明重构。大语言模型生成的证明通常正确但冗长且在不同库版本间脆弱，而现有重构方法忽视三个实际挑战：1）Lean 重构本质上是多目标问题（证明长度、编译成本与版本兼容性常相互冲突）；2）Lean 库具有脆弱的兼容性，而大语言模型发布时并不知晓 Lean/Mathlib 版本；3）基于训练的流程需每次大模型更新后重新微调，无法适应模型频繁迭代和 Lean 发布周期。Lean Refactor 通过从精心构建的多目标重构策略数据库中检索，并以冻结的智能体大模型为驱动，每个策略都带有丰富元数据，如支持的 Lean/Mathlib 版本及预期编译成本降低幅度。实验表明，在竞赛基准上实现超过70%的标记级压缩，在研究仓库中超过20%，编译时间最高减少60%，优于先前工作及 Claude Code。经过版本过滤的检索进一步提升了目标版本上的压缩效果，重构后的 miniF2F 证明在零样本迁移至未来 Lean 版本时表现优于未重构版本。
原文摘要 · Abstract (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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。