正确性反馈竟压制审计证据！无反馈发现认证见证产出率翻倍至59%，远超纠正循环的27.1%
When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus
📖 AI 总结
本文研究正确性反馈对规范完整性审计的影响，指出反馈机制会抑制审计本应揭示的证据，即程序虽满足书面契约却违背预期行为。作者在12个Verus/Rust任务、四个模型家族、匹配调用预算下开展实验，发现无反馈独立发现的认证见证产出率为59.0%，远高于IntentShield纠正反馈循环的27.1%，且差距主要源于反馈内容而非独立重启。该优势在各模型家族中均成立，并能通过解析器修复。分离阶段执行可在不复用响应的情况下达到相同总产出，但多数认证见证仍无法通过留出用例。保留这些见证可带来更强的规范修复效果：Phase-Revised契约实现成功率达81.3%，高于IS-Revised的62.5%。该效应在Dafny和Lean评估中未能复现，界定了其适用范围。研究结论是，完整性审计与正确性修复的即时目标相互对立，应在修复前保留并认证已承认的失败。
🔑 关键词速览
| Verus | 一个用于Rust程序的验证工具，支持形式化规范与验证。 |
| 规范完整性审计 | 检查程序是否满足书面契约但可能违反预期行为的审计过程。 |
| 认证见证 | 在审计中发现的、能够证明程序存在规范完整性问题的具体实例或证据。 |
| IntentShield | 一种使用纠正反馈循环的方法，旨在修复程序以满足预期行为。 |
| 阶段分离执行 | 将审计和修复过程分为独立阶段，避免反馈干扰证据收集的执行策略。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅