arXiv cs.AI· Aravind Mandiga, Guoming Li·· 11 小时前AI 评分31
LLM 生成的证明在程序重构下有多稳定？RefactorProof 对可验证代码生成的压力测试
How Stable Are LLM-Generated Proofs Under Program Refactoring? A Stress Test for Verifiable Code Generation
AI 导读
研究团队提出 RefactorProof，从 185 个 VERINA 任务中派生出 458 个 Lean 认证变体，在规格与证明逐字节固定的前提下检验程序重构后证明是否仍有效。
正文 · AI 翻译
摘要：可验证代码生成的基准测试通常针对一个固定实现来检验证明。我们追问：在保持行为不变的程序重构之后，同一证明是否仍然有效。我们提出 RefactorProof，它从在我们固定环境中可编译的 185 个 VERINA 任务中派生出 458 个经 Lean 认证的变体，同时保持规范和所评估的证明逐字节不变。VERINA 为 46 个任务提供了参考证明，全部来自其 basic 划分；主要的模型与参考对比进一步匹配了 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 衡量的是程序重构下未变证明的稳定性，而非证明被破坏后维护它的成本。
| 评论： | 已被 NeurIPS 2026 可验证编码 AI 研讨会接收 |
| 主题： | 人工智能（cs.AI）；计算机科学中的逻辑（cs.LO）；软件工程（cs.SE） |
| 引用为： | arXiv:2610.36328 [cs.AI] |
| （或 arXiv:2610.36328v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.36328 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Aravind Mandiga [查看电子邮件]
[v1]
2026 年 10 月 26 日星期一 21:56:03 UTC（1,473 KB）
来源：arXiv cs.AI · arxiv.org