基准通常只在单一实现上检验可验证代码生成的证明。我们提出 RefactorProof，在保持行为不变的前提下，对 185 个 VERINA 任务进行结构化重构，生成 458 个 Lean 认证的变体，并保持规格和证明文本逐字不变。VERINA 为 46 个基础任务提供参考证明，其中 21‑25 个为短小非递归任务用于模型‑参考对比。结构化重构揭示了显著的脆弱性：任务归一化结构化 PSR 为 4.3%（参考实现），而专用证明器为 13.3%‑26.8%。在匹配任务上，专用证明器的整体不变证明存活率仍高于参考实现，DeepSeek‑Prover‑V2‑7B 提升 15.6 分，Goedel‑Prover‑V2‑32B 提升 18.8 分，Goedel‑Prover‑V2‑8B 提升 20.3 分，三者 95% 置信区间均不包含零。该排序在排除全局存活的 T1 变体、采用家族平衡聚合以及不同可部署有效证明选择规则后仍保持。需要注意的是，不变证明失效并不等同于高修复成本：预定义的单标识符编辑能够修复 51/54 条参考结构失效和 58/85 条证明器失效。RefactorProof 因此衡量的是程序重构下不变证明的稳定性，而非破坏后维护成本的高低。
点评