Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts
本文介绍了 Proof-Refactor，这是一个代理框架，它通过采用过程引导的四阶段重构工作流，而非依赖于证明长度等单一指标优化，来提高大语言模型生成的形式化证明的可读性、模块化程度和可维护性。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
问题的核心：数学界的“快餐” vs. “家常菜”
想象一下，你要求一个非常聪明的机器人（大语言模型）写一段正式的数学证明。这个机器人很擅长它的工作：它遵循规则，得出正确答案，而且计算机也会说：“是的，这是正确的。”
然而，它写的证明往往就像是一个快餐汉堡。它能完成任务，但很凌乱。它把所有东西挤在一起，使用了一些只针对这一顿饭的奇怪配料；如果你以后想把其中的一部分用于另一顿饭，它就无法适配。它难以阅读，难以修复，也难以与他人分享。
在形式化数学的世界里（使用像 Lean 这样的工具），这些证明通常是“单体式”的——即一个巨大的代码块，虽然能运行，但维护起来简直是噩梦。目前优化这些证明的方法是尝试让它们变得更短。但让证明变短就像是在“打高尔夫”（试图用最少的杆数击球）；这往往会导致产生一些聪明但难以阅读的技巧，而不是清晰、逻辑严密的结构。
解决方案：“装修队”（Proof-Refactor）
该论文的作者提出了一种名为 Proof-Refactor 的新方法。他们并不试图缩短证明，而是将证明视为一次房屋装修。
他们认为，修复一个凌乱证明的最佳方式不是仅仅压缩它，而是对其进行重构（Refactor）。这意味着将那些凌乱的部分拆解开来，重新构建成干净、可复用的房间，使其能够融入一个标准的社区（数学库）。
为了实现这一点，他们构建了一个由 AI 智能体组成的团队，该团队分为四个不同的阶段，非常像一个施工队：
拆除队（提取 - Extraction）：
首先，他们观察凌乱的证明，并识别出正在执行特定任务的小型逻辑块。他们将这些块从主证明中“切”出来，并将它们变成独立的、临时的蓝图，称为脚手架（Scaffolds）。这就像是从墙上拆下一个奇形怪状的定制架子，把它放在桌子上进行检查。建筑师（辅助设计 - Helper Design）：
这是最重要的一步。一位人类建筑师（或者在这种情况下，是一个外部 AI 助手）会观察这些临时蓝图。他们会问：“这只是这栋房子里一个奇怪的架子，还是一个可以在任何房子里使用的标准书架？”
他们重新设计这个架子，使其成为一个标准的、可复用的组件。他们赋予它一个清晰的名字和描述，使其符合社区的建筑规范。施工员（证明 - Proving）：
现在，团队回到实际工作中，去建造这些新的、标准的组件。他们证明这些新的、干净的蓝图确实有效。这比一次性建造整栋房子要容易得多，因为他们每次只建造一个精巧的小房间。完工员（修复 - Repair）：
最后，他们回到原来的凌乱房子里。他们拆掉旧的、奇怪的墙壁，换上刚才建造的新的、标准的书架。房子依然屹立不倒，但现在它更整洁、更容易理解，而且那个新书架也可以被用于其他的房子。
为什么这种方法更好
论文在困难的数学问题（来自 Putnam 竞赛）上测试了这种方法。他们将他们的“装修队”与一个仅仅试图缩短证明长度的标准机器人进行了对比。
- 结果： Proof-Refactor 团队创建的证明在可读性、模块化（易于拆解）和可复用性方面都表现得更好。
- 权衡： 有时，新的证明并没有变得更短。事实上，它们有时甚至变得更长了！但这没关系。就像一个组织良好的厨房可能比一个杂乱的厨房占用更多空间一样，一个结构良好的证明对于人类阅读以及计算机长期验证都更有利。
秘诀：“双脑协作”
他们成功的关键在于劳动力分离。
- 一个 AI（“施工员”）擅长与计算机代码交流、检查错误并输入命令。
- 另一个 AI（“建筑师”）擅长高层思考和数学概念。
论文发现，如果你要求“施工员”在尝试修复代码错误的同时，还要兼顾“建筑师”的工作（设计新的结构），它会感到力不从心并导致设计糟糕。通过让“建筑师”独立地思考宏观蓝图，最终的结果质量会高得多。
总结
Proof-Refactor 不仅仅是试图缩短数学证明。它将证明视为需要清理的软件代码。它将凌乱的证明拆解，重新设计其中的组件使其标准化且可复用，然后将它们重新缝合在一起。其结果是，数学不再仅仅是“正确”的，而且是优美的、易于理解的，并且对未来的数学家们是有用的。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。