论文用RefactorProof测试程序重构后LLM证明是否仍有效。
资讯摘要
论文提出RefactorProof，用于检验可验证代码生成中证明在保持行为的程序重构后是否仍然有效。作者从VERINA任务中构建458个经Lean认证的变体，规格与证明逐字节固定。结果显示结构重构下证明普遍脆弱：任务归一化结构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%置信区间均不含零。作者指出未改动证明失败不等于修复成本高。
要点速读
- RefactorProof从185个VERINA任务派生458个Lean认证变体，保持规格与证明逐字节不变。
- 结构重构下任务归一化结构PSR：参考证明4.3%，专用证明器13.3%–26.8%。
- 匹配任务上专用证明器未改动证明存活率高于参考证明，三个模型分别高15.6、18.8、20.3个百分点，置信区间均不含零。
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/29 08:00:21（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。