发表机构
Lomonosov Moscow State University（莫斯科罗蒙诺索夫大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究提出BlueprintRepair修复接口，构建含142个案例的BlueprintTrace基准，对比三种修复方式，发现类型化修复成本最低且在有限令牌内覆盖率最高。
AI 中文摘要
基于大语言模型（LLM）的Lean证明系统日益将证明组织为蓝图：即形式化命题的依赖图。我们提出BlueprintRepair，一种修复接口，允许模型通过10种经模式检查的局部操作修改该图。操作会指定其编辑的节点，因此目标定理无法被更改。Lean会检查每一项应用的变更，且一项被接受的修复必须声明其证明所使用的每一个蓝图引理。我们还构建了BlueprintTrace，这是一个包含142个受控失败案例的基准，具备完整的已接受和已拒绝的修复轨迹。在匹配的源、反馈、模型和预算下，我们比较了类型化编辑、精确源补丁和完整模块重写，每个状态和接口对应一个回合。使用DeepSeek-V4-Flash时，这三种接口解决了基准中几乎相同数量的局部失败。类型化修复是每个已解决状态中成本最低的（打补丁的成本是其1.30倍，重写是其2.06倍），并且在每个任务10000个完成令牌内，它几乎达到了其最终覆盖率，而两种自由形式接口则远远落后。第二个模型Qwen3.6-Flash解决的状态更少，但仍保持类型化修复成本最低，在证明生成状态上领先，并重复了这一局部模式。
英文摘要
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.
Comments19 pages, 4 figures, 7 tables
