Proof-Refactor：将生成的形式证明重构为模块化工件

虽然大型语言模型 (LLM) 在生成形式证明方面表现出了强大的性能，但与成熟的形式数学库中的证明相比，其输出的可读性、模块化性、可维护性和可重用性往往较差。我们认为，这种差距部分源于大多数证明生成管道中隐含的编译优先目标，该目标鼓励整体或临时证明脚本而不是库质量的工件。现有的证明质量改进方法通常依赖于明确的、可计算的优化目标。然而，在实践中，最容易处理和经过实验验证的目标很大程度上是基于长度的，而可读性、模块化、可维护性和可重用性等更高级别的质量很难简化为可靠的自动指标。我们没有针对单个代理指标优化证明改进，而是采用受人类证明重构工作流程启发的流程引导方法。我们提出了一个代理框架$\textbf{Proof-Refactor}$，它将证明重构分解为四个阶段：提取候选证明片段、设计辅助声明、正式证明提取和设计的组件以及使用已验证的组件修复原始证明。在 PutnamBench 和 Putnam2025 生成的Lean证明上，Proof-Refactor 在强大的 Claude Code 重构基线上提高了基于 rubric 的重构分数，在签名质量和人类可读性方面获得了最大的收益。这些结果表明，流程引导的重构可以改进证明结构，而无需将证明长度作为主要目标。