When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus

查看原文 / View Original 编辑 / Edit

Computer Science > Artificial Intelligence arXiv:2610.20676 (cs) [Submitted on 14 Oct 2026] Title: When Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus Authors: Adarsh Agrawal (Independent Researcher)

计算机科学 > 人工智能 arXiv:2610.20676 (cs) [提交于 2026 年 10 月 14 日] 标题：当正确性反馈抹除证据时：Verus 中的阶段分离完备性审计作者：Adarsh Agrawal（独立研究员）

Abstract: Correctness feedback suppresses the very evidence that specification-completeness auditing is designed to uncover: programs that satisfy a written contract but violate intended behavior. We demonstrate this objective reversal on 12 Verus/Rust tasks across four model families under matched call budgets.

摘要：正确性反馈抑制了规范完备性审计旨在揭示的证据，即那些满足书面契约但违反预期行为的程序。我们在匹配调用预算的情况下，针对四个模型家族的 12 个 Verus/Rust 任务演示了这种目标反转。

Independent no-feedback discovery more than doubles certified-witness yield relative to IntentShield’s corrective-feedback loop (59.0% versus 27.1%). A format-matched iterative control places the larger share of this gap in feedback content, not independent restarts.

相对于 IntentShield 的纠正性反馈循环，独立的无反馈发现使认证见证的产出增加了一倍以上（59.0% 对 27.1%）。格式匹配的迭代对照实验表明，这一差距的主要部分在于反馈内容，而非独立的重启。

The advantage holds in every model family and survives parser repair. A separate phase-separated execution matches the aggregate yield without reusing responses; most certified witnesses also fail held-out cases.

这种优势在每个模型家族中都成立，并且在解析器修复后依然存在。一种单独的阶段分离执行方式在不重用响应的情况下达到了相同的总产出；大多数认证见证也无法通过留出的测试用例。

Preserving these witnesses delivers stronger specification repair: Phase-Revised contracts achieve 81.3% implementation success, versus 62.5% for IS-Revised, with Direct-Revised close behind. Both no-feedback witness sources substantially outperform weakened contracts.

保留这些见证可以实现更强的规范修复：阶段修订（Phase-Revised）契约实现了 81.3% 的实现成功率，而 IS-Revised 为 62.5%，Direct-Revised 紧随其后。两种无反馈见证来源的表现均显著优于弱化契约。

The effect does not reproduce in the available Dafny and Lean evaluations, establishing an empirical boundary around the studied Verus/Rust workflow. Completeness auditing and correctness repair have opposing immediate objectives. Preserve and certify the admitted failure before repairing it.

这种效应在现有的 Dafny 和 Lean 评估中并未重现，从而为所研究的 Verus/Rust 工作流程确立了一个经验边界。完备性审计和正确性修复具有相反的即时目标。在修复之前，请先保留并认证已承认的失败。