RefactorProof

LLM 生成的代码证明在重构下表现出脆弱性 · arXiv 研究

一项题为“LLM 生成的证明在程序重构下有多稳定？”的新研究引入了 RefactorProof，这是一个旨在测试程序重构后代码生成证明的韧性的基准。该基准包含 458 个源自 185 个 VERINA 任务的 Lean 认证变体，保持了原始规范和证明。结果表明，参考系统和专门的 LLM 证明器生成的证明都存在显著的脆弱性，失败率从 4.3% 到 26.8% 不等。尽管如此，专门的证明器比参考证明器表现出更高的稳定性，其中 DeepSe…