提出可类型化局部编辑的修复接口，提升失败形式证明蓝图的修复效率。
BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints
- 通过十种受控的局部操作修改证明蓝图，保持目标定理不变
- 在142个受控失败案例中，类型化修复每解一状态成本最低
- 适合需要高效、精确修复形式证明的研究者和开发者
基于大模型的Lean证明系统逐渐将证明组织为依赖图形式的蓝图。本文提出BlueprintRepair，一种修复界面，允许模型通过十种模式检查的局部操作修改该图。操作需指定被编辑节点，确保目标定理不变；每个变更均由Lean验证，且被接受的修复必须声明其使用的每个蓝图引理。我们构建了BlueprintTrace，一个包含142个受控失败的基准数据集，完整记录了被接受与拒绝的修复轨迹。在相同源代码、反馈、模型与预算下，对比类型化编辑、精确源码补丁和完整模块重写。使用DeepSeek-V4-Flash时，三者解决的局部失败数相近。类型化修复每解一状态成本最低（补丁为1.30倍，重写为2.06倍），且在10,000次完成标记内达到接近最终覆盖率，而自由格式接口显著落后。另一模型Qwen3.6-Flash虽解决状态较少，但仍保持类型化修复成本最低，在证明撰写类状态中领先，并重复该局部修复模式。
原文摘要 · Abstract (English)
LLM-based Lean proving systems increasingly organize a proof as a blueprint: a dependency graph of formal statements. We introduce BlueprintRepair, a repair interface that lets a model change this graph through ten schema-checked local operations. An operation names the node it edits, so the target theorem cannot be changed. Lean checks every applied change, and an accepted repair must declare every blueprint lemma its proof uses. We also construct BlueprintTrace, a benchmark of 142 controlled failures with complete accepted and rejected repair trajectories. We compare typed edits, exact source patches, and complete module rewrites under matched source, feedback, model, and budget, one episode per state and interface. With DeepSeek-V4-Flash, the three interfaces solve almost the same number of the benchmark's localized failures. Typed repair is the cheapest per solved state (patching is 1.30x as expensive, rewriting 2.06x), and within 10,000 completion tokens per task it reaches almost all of its final coverage, while both free-form interfaces are well behind. A second model, Qwen3.6-Flash, solves fewer states but keeps typed repair cheapest, puts it ahead on the proof-authoring states, and repeats the localized pattern.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。