BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints
BlueprintRepair 是一种修复接口，允许模型通过十种 schema 检查的局部操作修改 Lean 证明蓝图。Lean 检查每次应用更改，接受的修复必须声明其证明使用的每个蓝图引理。BlueprintTrace 基准包含 142 个受控失败及完整轨迹。在 DeepSeek-V4-Flash 下，三种接口解决的局部失败数量几乎相同，但类型化修复每个解决状态成本最低（补丁为 1.30 倍，重写为 2.06 倍），且在 10,000 个完成 token 内达到几乎全部最终覆盖率。Qwen3.6-Flash 解决状态较少，但类型化修复仍最便宜。
Development
- First ReportBlueprintRepair: Typed Local Edits for Failed Lean Proof BlueprintsarXiv cs.AI
- Current Assessment该工作表明，在形式验证领域，结构化接口可能比自由形式编辑更高效，这影响 LLM 辅助证明工具的设计。成本优势可能推动工具采用类型化编辑，减少 token 消耗。可验证信号：是否有其他团队采用类似接口，或 BlueprintTrace 被引用。Agent Pulse · analysis
LLM 驱动的 Lean 证明系统将证明组织为蓝图（形式语句的依赖图）。BlueprintRepair 引入一种修复接口，允许模型通过十种 schema 检查的局部操作修改此图。操作指定编辑的节点，因此目标定理不可更改。Lean 检查每次应用更改，接受的修复必须声明其证明使用的每个蓝图引理。作者构建了 BlueprintTrace 基准，包含 142 个受控失败及完整接受/拒绝修复轨迹。在匹配源、反馈、模型和预算下比较类型化编辑、精确源补丁和完整模块重写。使用 DeepSeek-V4-Flash，三种接口解决的局部失败数量几乎相同，但类型化修复每个解决状态成本最低（补丁为 1.30 倍，重写为 2.06 倍），且在 10,000 个完成 token 内达到几乎全部最终覆盖率，而自由形式接口落后。Qwen3.6-Flash 解决状态较少，但类型化修复仍最便宜，并在证明编写上领先。
类型化局部编辑在证明修复中提供了成本优势，表明约束接口可以减少搜索空间。每个操作命名节点，防止意外修改目标定理，并通过 schema 检查强制结构正确性。接受的修复必须声明所有使用的引理，确保可验证性。成本优势（补丁 1.30 倍，重写 2.06 倍）表明结构化编辑比自由形式补丁更高效。下一步可验证信号：在更大模型或更复杂证明上，类型化修复是否保持成本优势，以及 BlueprintTrace 是否成为标准基准。
该工作表明，在形式验证领域，结构化接口可能比自由形式编辑更高效，这影响 LLM 辅助证明工具的设计。成本优势可能推动工具采用类型化编辑，减少 token 消耗。可验证信号：是否有其他团队采用类似接口，或 BlueprintTrace 被引用。
对于开发 LLM 证明工具的公司，类型化修复可降低推理成本（补丁 1.30 倍，重写 2.06 倍），提高效率。可验证信号：工具是否采用类似接口，或成本数据被引用。
类型化修复可能成为 LLM 证明助手的默认接口，降低修复成本。未来可能扩展到其他形式验证任务。可验证信号：后续工作是否在更大规模证明上验证，或集成到主流证明助手。