arXiv:2504.20964v1 评估类型：交叉 摘要：我们介绍了一种新的基准测试OSVBench，用于评估大型语言模型（LLMs）生成与操作系统内核验证任务相关的完整规范代码的能力。该基准测试首先通过提供编程模型将规范生成问题定义为在语法和语义受限范围内的程序合成问题。模型需要理解提供的验证假设以及搜索的潜在语法和语义空间，然后在操作系统高层次功能描述的指导下生成潜在有缺陷的操作系统代码实现的完整规范。该基准测试基于现实世界的操作系统内核Hyperkernel构建，包含总共245个复杂的规范生成任务，每个任务都是大约20k-30k个标记的长上下文任务。我们对12个LLM的全面评估表明，现有LLM在操作系统验证的规范生成任务上表现有限。基准测试中它们在任务上的显著性能差异突显了它们处理长上下文代码生成任务的能力差异。评估工具包和基准测试可在https://github.com/lishangyu-hkust/OSVBench获取。