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）的实验显示，随着证明上下文被移除，成功率下降、成本上升。
正文 · 原文
Abstract:Coding agents achieve high success rates on existing benchmarks for Verus, a verifier for Rust programs. These benchmarks typically provide the auxiliary lemmas needed to complete a proof. In practice, however, such lemmas must be discovered and proved. To capture this challenge, we present SEVERUS, a context-aware technique to generate Verus benchmarks that organizes verification tasks into quests, each divided into levelsin a gamified manner. Using the original proof dependencies in verified projects, SEVERUS constructs one quest per verification target and progressively removes proof context to create individual levels. These levels range from the easiest, requiring completing only a single missing lemma, to the hardest, requiring proving the target without any supporting lemmas. An independent checker rejects changes to executable code, weakened specifications, and unsound proof constructs. A noisy binary search estimates the highest level that an agent can solve reliably. Applied to six open-source Verus projects, SEVERUS generates 819 quests comprising 10,095 levels. Experiments with Codex using GPT-6 Sol and GPT-6 Luna, and with Claude Code using Sonnet 4.6, show that success decreases and cost increases as proof context is withdrawn. The strongest agent solves the final level of 52 of 60 sampled quests, yet can only reliably solve 35% of their levels, with failures concentrated in longer quests. Successful GPT-6 Sol proofs rarely reproduce the withheld lemmas, instead, using alternative proof decompositions. By systematically varying proof context, SEVERUS provides a foundation for constructing verification benchmarks that can continue to challenge increasingly capable coding agents.
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI) |
| ACM classes: | D.2.0; F.4.3; I.2.2 |
| Cite as: | arXiv:2611.07194 [cs.SE] |
| (or arXiv:2611.07194v1 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2611.07194 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Martim Afonso [view email]
[v1]
Wed, 4 Nov 2026 22:34:57 UTC (321 KB)
来源：arXiv cs.AI · arxiv.org