💻 computer science

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search

Lean Refactor 是一种检索增强型智能体框架，它通过动态选择精心策划的重构策略而无需重新训练模型，从而针对多个目标（包括令牌压缩、编译速度和版本兼容性）优化 Lean 证明。

原作者： Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang, Weiran Sun, Wuyang Chen

发布于 2026-05-21

📖 1 分钟阅读☕ 轻松阅读

原作者： Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang, Weiran Sun, Wuyang Chen

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

以下是用通俗语言和创意类比对论文《Lean Refactor》的解释。

问题：过度设计的“证明”

想象一位才华横溢但过于热情的建筑师（AI），刚刚建造了一座房子（数学证明）。这座房子结构稳固——不会倒塌，也通过了所有安全检查。然而，建筑师用 500 块砖砌了一堵只需 50 块砖的墙。他们是用大锤去砸坚果。

在 Lean（一种用于编写计算机可验证数学证明的语言）的世界里，AI 模型生成的证明往往是正确但极其冗长、杂乱且编译缓慢的。

太长：证明难以让人类阅读。
太慢：由于证明充斥着不必要的步骤，计算机验证其有效性需要很长时间。
脆弱：Lean 语言频繁变更（就像软件更新一样）。为"1.0 版本”编写的证明，即使数学逻辑依然正确，当计算机升级到"2.0 版本”时也可能完全失效。

现有的工具试图通过重新训练 AI（昂贵且缓慢）或仅仅要求它“更简洁”（往往导致证明运行更慢）来解决这个问题。

解决方案：“智能图书管理员”系统

作者创建了 Lean Refactor。他们没有尝试重新训练 AI，而是构建了一个即插即用的系统，充当 AI 的超级智能图书管理员。

以下是其工作原理的比喻：

1. 策略库（图书馆）

想象一个巨大的图书馆，里面装满了“重构卡片”。每张卡片描述了一种缩短证明的具体技巧。

技巧：“与其逐个列出每个数字，不如使用这个魔法公式。”
元数据：至关重要的是，每张卡片都有一个标签。它标明了：
- 节省了多少时间？（例如：“节省 30% 的编译时间”）。
- 适用于哪个语言版本？（例如：“适用于 Lean v4.16 和 v4.22"）。
- 能让证明缩短多少？

论文声称，他们建立了有史以来最大的此类卡片库，其中包含从数十万条证明示例中提炼出的超过 9,000 种独特策略。

2. 智能体（建筑师 + 图书管理员）

当 AI 需要修复证明时，它不会靠猜测。它遵循一个循环：

规划者：AI 审视杂乱的证明，说道：“这部分看起来需要‘魔法公式’技巧。”
图书管理员（检索）：系统前往图书馆，提取与该部分匹配的具体卡片。
- 如果你想要最短的证明：它会提取承诺最大体积缩减的卡片。
- 如果你想要最快的编译：它会提取承诺最大速度提升的卡片。
- 如果你使用的是旧版 Lean：它会过滤掉任何不适用于你版本的卡片。
重构者：AI 应用卡片中的技巧来重写证明。
调试器：计算机检查新证明。如果出错，AI 会尝试在局部修复错误，而不会推翻整个改进。

为何如此特别（论文的声明）

1. 平衡相互竞争的目标（“多目标”魔法）
通常，你必须做出选择：“我是希望证明更短，还是希望它编译更快？”

旧方法：你只能选一个，另一个就会受损。
Lean Refactor：你可以告诉系统：“我想要它既短，又快。”系统查看图书馆卡片，找出那些能同时提供两者的卡片，并选择最佳平衡点。
结果：在竞赛数学问题上，他们将证明缩短了 70% 以上，并将编译时间减少了 60% 以上。

2. 抵御软件更新（“版本鲁棒性”）
由于图书馆卡片标明了它们适用的具体软件版本，系统可以立即过滤掉“过时”的技巧。

结果：如果你请求一个适用于"Lean v4.16"的证明，系统只会使用适用于 v4.16 的卡片。这防止了 AI 幻觉（编造）该版本中不存在的工具。

3. 适用于任何 AI（“模型无关”特性）
你不需要为此训练一个新的 AI。该系统适用于任何“冻结”（预训练）的 AI 模型，无论是来自 Google（Gemini）、Anthropic（Claude）还是 OpenAI（GPT）。“智能”来源于策略库，而非 AI 的大脑。

结果：他们在不同的 AI 模型上进行了测试，它提升了所有模型的性能，甚至击败了一个名为"Claude Code"的专用编码智能体。

核心结论

Lean Refactor 就像是给施工队提供了一套蓝图和一个包含预先测试、带标签的快捷方式的工具箱。他们不再猜测如何建造房子，而是根据他们拥有的工具和正在使用的建筑规范版本，查阅建造特定墙壁的最佳方法。

论文声称这种方法：

在数学竞赛中将证明缩短了 70% 以上。
使编译速度提高了 60%。
即使软件语言更新，也能保持其有效性。
无需重新训练 AI 模型即可实现这一切。

技术摘要：Lean 重构

问题陈述

使用强化学习（RL）训练的大语言模型（LLM）在 Lean 中进行形式化定理证明时，往往生成的证明虽然正确，但以其冗长、脆弱且计算成本高昂而臭名昭著。尽管现有的重构工作已经存在，但在应用于 Lean 生态系统时，它们面临三个根本性的局限：

多目标张力：Lean 重构本质上是多目标的。优化证明长度通常与最小化编译成本相冲突（例如，更短的证明可能会调用重型策略，从而增加编译时间），而现有方法缺乏原则性的机制来平衡这些权衡，或在推理时适应未见过用户目标。
版本脆弱性：Lean 及其标准库 Mathlib 几乎每周都在演进，伴随着频繁的 API 变更和引理重命名。前沿大语言模型具有静态的知识截止点，导致其幻觉出过时的策略，并与当前的工具链不兼容。
数据稀缺：与主流编程语言不同，Lean 缺乏训练型重构流水线所需的大规模配对数据集（噪声 - 清洁代码对）。此外，基于训练的方法需要针对每一个新的大语言模型发布进行重复的微调，无法随模型更替或 Lean 的发布周期进行扩展。

方法论：Lean 重构

作者提出了 Lean Refactor，这是一个即插即用、检索增强的智能体框架，旨在无需微调底层大语言模型即可重构 Lean 证明。该系统通过将知识外部化为一个结构化的、密集注释的数据库，将重构逻辑与模型解耦。

1. 密集注释的策略库

该框架的核心是一个精心策划的数据库，包含从超过 200,000 对长 - 短证明 中提炼出的 9,237 个独特重构策略。

结构：每个策略包括标题、描述、前提条件（“何时应用”）、逐步应用指南以及抽象的“之前/之后”示例。
元数据：至关重要的是，每个策略都标注了大语言模型无法从训练数据中推断出的元数据：
- 编译时间减少：应用该策略时观察到的中位数相对加速比。
- 版本兼容性：一组经过验证的 Lean/Mathlib 工具链（例如 v4.14.0、v4.16.0、v4.22.0），在这些工具链下重构后的证明能够成功编译。这是通过在多个版本上重新编译缩短后的证明来确定的。

2. 多目标检索与重排序

在推理阶段，该框架采用检索流水线，无需重新训练模型即可适应用户指定的目标：

最短证明：仅基于与证明片段的语义相似度（余弦相似度）检索策略。
编译时间感知：检索一大组语义相似的候选项，然后基于注释的编译成本减少元数据对其进行重排序。
特定版本：过滤候选池，仅包含其兼容性元数据中包含用户目标 Lean 版本的策略。

3. 智能体循环

该框架将这些组件封装在一个与模型无关的智能体循环中，包括：

规划器：根据检索到的策略将重构任务分解为具体步骤。
重构器：执行计划以生成更短的证明。
调试器：利用编译器反馈在闭环中修复错误（最多 $D$ 轮）。
骨干模型无关性：规划器、重构器和调试器可以由任何冻结的前沿大语言模型（例如 Gemini、Claude、GPT 系列）实例化，允许系统在不重新训练的情况下跨模型迁移。

主要贡献

数据集发布：作者发布了迄今为止最大的 Lean 重构数据集，包含超过 20 万对长 - 短证明和 9,000 个重构策略，每个策略均标注了编译成本和版本兼容性。
性能：Lean Refactor 在竞赛基准测试（miniF2F、PutnamBench）上实现了 >70% 的令牌级压缩，在研究级仓库（Analysis、FLT、PhysLean）上实现了 >20% 的压缩。它还将竞赛基准测试上的编译时间减少了高达 60%。
可控性与鲁棒性：该系统通过检索规则而非模型权重支持多目标控制（长度 vs. 速度 vs. 兼容性）。与未重构的对应物及先前的优化方法相比，重构后的证明表现出更强的零样本版本迁移能力，能够适应未来的 Lean 发布版本。
模型无关性：该框架提高了不同大语言模型骨干（Gemini 3 Flash、Claude Haiku 4.5）的性能，并且优于通用编程智能体（如 Claude Code），即使后者被赋予了相同的策略检索工具。

实验结果

长度缩减：在竞赛基准测试上，Lean Refactor 优于先前的最先进方法 ProofOptimizer，在 miniF2F 上实现了 88.40% 的缩减，在 PutnamBench 上实现了 70.38% 的缩减（而 ProofOptimizer 为 57.20%）。在研究级证明上，它实现了平均 20–33% 的缩减，显著优于消融基线。
编译时间：通过基于编译成本元数据对策略进行重排序，该框架在 PutnamBench 上实现了 42.62% 的相对编译时间减少，而标准检索方法为 37.11%。
版本兼容性：当针对特定 Lean 版本（例如 v4.16.0）时，经过版本过滤的检索始终比未过滤的检索产生更好的长度缩减。与 ProofOptimizer 或原始冗长证明生成的证明相比，重构后的证明在更多未来的 Lean 发布版本（高达 v4.29.0）中保持了类型检查能力。
依赖项减少：重构后的证明在 42–67% 的案例中减少了外部和内部项目依赖项，表明这是真正的逻辑简化，而不仅仅是将工作卸载到重型库引理上。

意义

本文认为，Lean Refactor 解决了维护形式化数学库的关键瓶颈：证明简洁性与编译效率之间的张力，以及代码在快速演变的工具链中的脆弱性。通过将重构知识外部化为富含元数据的策略库，该框架实现了可控的、多目标的优化，而无需昂贵的模型微调。这种方法使系统能够抵御 Lean/Mathlib 版本漂移，并立即适应新的大语言模型骨干，为更具可维护性和版本韧性的形式化证明奠定了基础。