一句话：提出 NL2VBench 基准，包含 762 个自然语言到 Verus 可验证 Rust 的生成任务及验证工具链。
NL2VBench 是一个用于评估大语言模型（LLM）从自然语言描述生成 Verus 可验证 Rust 程序的基准数据集。它包含 762 个经过整理的任务，分为 Simple、Loops、Complex 三类；每个任务提供自然语言描述、函数签名以及经 Verus 验证的参考实现。工件还包含 12 个 prompt 模板、实验脚本和验证脚本，以支持端到端评测。该工作旨在填补自然语言到可验证系统代码生成缺乏标准化基准的空白，并为 LLM 在程序合成与形式验证交叉方向提供可复现的评估基础设施。
NL2VBench is a benchmark dataset for evaluating LLMs on generating Verus-verified Rust programs from natural language descriptions. It contains 762 curated tasks across 3 categories (Simple, Loops, Complex). Each task includes a natural-language description, function signature, and a reference verified Verus implementation. The artifact also includes 12 prompt templates, experiment scripts, and a verification script.
@inproceedings{paperbot12500,
title = {NL2VBench: A Benchmark for End-to-End Natural-Language to Verifiable Rust Generation},
author = {Lianhe Hu and Cheng Wen and Dugang Liu and Zhiwu Xu and Zhuohua Li and Jie Su and Bin Yu and Shengchao Qin},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834619}
}