When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus
中文摘要
由模型生成 · 人工抽检论文发现：在 Verus/Rust 形式化验证中，正确性反馈会抑制规范完整性审计所需的证据。无反馈独立发现产生的认证见证率（59.0%）远超纠正反馈循环（27.1%），且该优势跨模型家族成立。保留这些见证可显著提升规范修复成功率（81.3% vs 62.5%），提示审计与修复目标相悖，应先保留并认证失败证据再修复。
全文
已译中文arXiv:2610.20676v1 公告类型：新
摘要：正确性反馈会压制规范完备性审计本应揭示的证据：那些满足书面契约但违反预期行为的程序。我们在 12 个 Verus/Rust 任务上、跨四个模型家族、在匹配的调用预算下展示了这种目标反转。独立无反馈发现所产生的认证见证产出是 IntentShield 纠正反馈循环的两倍以上（59.0% 对 27.1%）。一个格式匹配的迭代对照组表明，这一差距的较大份额来自反馈内容，而非独立重启。该优势在每个模型家族中都成立，并且在解析器修复后依然存在。一个单独的相位分离执行在不复用响应的情况下达到了相同的总体产出；大多数认证见证也未通过留出用例。保留这些见证可带来更强的规范修复：Phase-Revised 契约达到 81.3% 的实现成功率，而 IS-Revised 为 62.5%，Direct-Revised 紧随其后。两种无反馈见证来源都显著优于弱化后的契约。该效应在可用的 Dafny 和 Lean 评估中未能复现，从而为所研究的 Verus/Rust 工作流确立了一个经验边界。完备性审计与正确性修复具有相反的即时目标。在修复之前，先保留并认证已承认的失败。
本译文由模型自动生成，仅供参考与快速理解；涉及数字、版本、命令、法律条文等请以原文为准。
原文附件
2 个 · 均跳转原站，本站不托管文件正文为原站公开内容的抓取与清洗结果，英文条目附模型生成的中文译文；两者均仅供参考， 准确内容请以原站为准。内容版权归原作者所有，若认为侵权请联系我们下线。