arXiv cs.AI· \'Alvaro F. Silva, Martim Afonso, Nuno Saavedra, Emily First, Alexandra Mendes, Jo\~ao F. Ferreira·· 11 小时前AI 评分31
SeVerus：面向 Rust 验证的上下文感知游戏化基准测试
SeVerus: Context-Aware, Gamified Benchmarking for Rust Verification
AI 导读
SeVerus 是一种上下文感知的 Verus 基准生成技术，将验证任务组织成游戏化关卡，逐步移除证明上下文。在六个开源 Verus 项目上生成 819 个任务、10,095 个关卡；Codex（GPT-6 Sol、GPT-6 Luna）与 Claude Code（Sonnet 4.6）的实验显示，随着证明上下文被移除，成功率下降、成本上升。
正文 · AI 翻译
摘要：编码智能体在 Verus（一种 Rust 程序验证器）的现有基准测试中取得了很高的成功率。这些基准测试通常会提供完成证明所需的辅助引理。然而在实践中，这类引理必须被自行发现并证明。为应对这一挑战，我们提出了 SEVERUS，一种上下文感知的技术，用于生成 Verus 基准测试，它将验证任务组织成“任务关卡”（quests），并以游戏化方式将每个任务划分为多个层级。利用已验证项目中原有的证明依赖关系，SEVERUS 为每个验证目标构建一个任务关卡，并逐步移除证明上下文以创建各个层级。这些层级从最简单的（仅需补全一个缺失的引理）到最难的（在没有任何辅助引理的情况下证明目标）。一个独立的检查器会拒绝可执行代码的改动、被弱化的规约以及不健全的证明构造。一种带噪声的二分搜索用于估计智能体能够可靠求解的最高层级。应用于六个开源 Verus 项目，SEVERUS 生成了 819 个任务关卡，共包含 10,095 个层级。使用 GPT-6 Sol 和 GPT-6 Luna 的 Codex，以及使用 Sonnet 4.6 的 Claude Code 进行的实验表明，随着证明上下文被移除，成功率下降而成本上升。最强的智能体能够解出 60 个抽样任务关卡中 52 个的最终层级，但只能可靠地解出其中 35% 的层级，失败集中在较长的任务关卡中。GPT-6 Sol 的成功证明很少复现被移除的引理，而是采用替代的证明分解方式。通过系统地改变证明上下文，SEVERUS 为构建能够持续挑战能力日益增强的编码智能体的验证基准测试提供了基础。
| 学科： | 软件工程（cs.SE）；人工智能（cs.AI） |
| ACM 分类： | D.2.0; F.4.3; I.2.2 |
| 引用为： | arXiv:2611.07194 [cs.SE] |
| （或 arXiv:2611.07194v1 [cs.SE] 为此版本） | |
| https://doi.org/10.48550/arXiv.2611.07194 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Martim Afonso [查看邮箱]
[v1]
2026年11月4日星期三 22:34:57 UTC（321 KB）
来源：arXiv cs.AI · arxiv.org