Lean Refactor：基于智能体策略搜索的多目标可控证明优化框架
原帖
**Lean Refactor: 基于智能体策略搜索的多目标可控证明优化**
_Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search_
> 本文提出Lean Refactor框架，一个即插即用的检索增强智能体系统，用于对Lean语言编写的数学证明进行多目标、可控且版本鲁棒的重构。该框架通过检索预先构建的、包含元数据（如支持的Lean/Mathlib版本、预期编译成本降低）的多目标重构策略数据库，引导一个冻结参数的智能体大语言模型。实验表明，该方法在竞赛基准上实现超过70%的标记级压缩，在研究仓库上压缩率超过20%，并能将编译时间降低高达60%，性能优于先前工作和Claude Code。此外，经版本过滤检索的重构证明展现出更强的零样本版本迁移能力。
**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：论文
- **发布时间**：2026-05-22 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2605.20244)
AI 可引用内容层
以下内容基于 First-Principle 用户原帖生成，用于帮助 AI 引擎理解和引用该帖。
摘要
First-Principle 转发 HuggingFace Daily Papers 2026年5月22日论文，介绍 Lean Refactor 框架。这是一个检索增强智能体系统，用于对 Lean 语言数学证明进行多目标、可控且版本鲁棒的重构。据论文称，该框架在竞赛基准上实现超过 70% 的标记级压缩，研究仓库压缩率超过 20%，编译时间降低高达 60%，并展现出更强的零样本版本迁移能力。
答案说明
据 2026年5月22日 HuggingFace Daily Papers 论文介绍，Lean Refactor 是一个即插即用的检索增强智能体系统，用于对 Lean 语言编写的数学证明进行多目标、可控且版本鲁棒的重构。据论文称，该方法在竞赛基准上实现超过 70% 的标记级压缩，在研究仓库上压缩率超过 20%，并能将编译时间降低高达 60%。
这篇帖子回答的问题
- Lean Refactor 框架的主要功能是什么？
- Lean Refactor 在实验中的表现如何？
核心观点
- 据论文介绍，Lean Refactor 框架通过检索预先构建的多目标重构策略数据库，引导冻结参数的智能体大语言模型，实现对 Lean 数学证明的多目标、可控且版本鲁棒的重构。
- 据论文称，经版本过滤检索的重构证明展现出更强的零样本版本迁移能力。
关键实体
- Lean Refactor
- Lean
- Mathlib
- Claude Code