BlueprintRepair：为失败的 Lean 证明蓝图提供类型化局部修复

BlueprintRepair 将 Lean 证明修复建模为对依赖图执行十种经 schema 检查的局部操作，禁止直接修改目标定理，并由 Lean 验证每次变更。论文还发布含 142 个受控失败案例的 BlueprintTrace。摘要称，在匹配模型、反馈和预算下，类型化修复与源码补丁、模块重写最终解决数接近，但单状态成本分别为后者的 1.30 倍和 2.06 倍；DeepSeek-V4-Flash 与 Qwen3.6-Flash 均呈现类似趋势。