arXiv cs.AI· Adarsh Agrawal (Independent Researcher)·· 2 天前AI 评分23
Verus 中的正确性反馈为何会抹除证据：阶段分离的完整性审计
When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus
AI 导读
在 12 个 Verus/Rust 任务、四个模型家族、匹配调用预算下，无反馈独立发现产生的认证见证产出率（59.0%）是 IntentShield 纠正反馈循环（27.1%）的两倍以上，差距主要来自反馈内容而非独立重启。
正文 · AI 翻译
摘要：正确性反馈恰恰抑制了规范完整性审计旨在揭示的证据：那些满足书面契约但违反预期行为的程序。我们在 12 个 Verus/Rust 任务、四个模型家族、匹配调用预算的条件下展示了这一目标反转。独立无反馈发现所获得的认证见证产出是 IntentShield 纠正反馈循环的两倍以上（59.0% 对 27.1%）。格式匹配的迭代对照将这一差距的更大份额归因于反馈内容，而非独立重启。这一优势在每个模型家族中都成立，并且在解析器修复后依然存在。单独的阶段分离执行在不复用响应的情况下达到了相同的总体产出；大多数认证见证也未通过留出案例。保留这些见证可带来更强的规范修复：Phase-Revised 契约达到 81.3% 的实现成功率，而 IS-Revised 为 62.5%，Direct-Revised 紧随其后。两种无反馈见证来源都显著优于弱化契约。该效应在可用的 Dafny 和 Lean 评估中未能复现，从而围绕所研究的 Verus/Rust 工作流确立了一个经验边界。完整性审计与正确性修复具有相反的即时目标。在修复之前，先保留并认证已承认的失败。
| 评论： | 论文被 NeurIPS 2026 可验证编码 AI 研讨会接收 |
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2610.20676 [cs.AI] |
| （或使用 arXiv:2610.20676v1 [cs.AI] 获取此版本） | |
| https://doi.org/10.48550/arXiv.2610.20676 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Adarsh Agrawal [查看电子邮件]
[v1]
2026年10月14日星期三 14:43:24 UTC（1,388 KB）
来源：arXiv cs.AI · arxiv.org