大模型arXiv cs.AI4 天前
When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus
论文发现：在 Verus/Rust 形式化验证中，正确性反馈会抑制规范完整性审计所需的证据。无反馈独立发现产生的认证见证率（59.0%）远超纠正反馈循环（27.1%），且该优势跨模型家族成立。保留这些见证可显著提升规范修复成功率（81.3% vs 62.5%），提示审计与修复目标相悖，应先保留并认证失败证据再修复。