BlueprintRepair：用于Lean证明蓝图的类型化局部编辑

BlueprintRepair是一种让大模型通过十种受模式检查的局部操作修改Lean证明蓝图的修复接口。研究构造了包含142个受控失败案例的BlueprintTrace基准，并对比了类型化编辑、精确源码补丁和完整模块重写三种方式。在DeepSeek-V4-Flash下，三种接口解决的局部失败数几乎相同，但类型化修复每个已解状态成本最低，补丁费用为其1.30倍，重写为其2.06倍。在每任务10000个补全token预算内，类型化修复几乎达到最终覆盖率，而两种自由形式接口明显落后。Qwen3.6-Flash解决的案例更少，但类型化修复依然最便宜，并在证明编写类状态上领先。