OSVBench

OSVBench是一个新的基准测试，用于评估大型语言模型（LLMs）在生成与操作系统内核验证任务相关的完整规范代码方面的能力。该基准测试首先通过提供编程模型将规范生成问题定义为一个在受限语法和语义范围内的程序合成问题。LLMs需要理解提供的验证假设以及潜在的语法和语义空间，然后在操作系统高级功能描述的指导下生成潜在有缺陷的操作系统代码实现的完整规范。该基准测试基于真实世界的操作系统内核Hyperkernel构建，共包含245个复杂的规范生成任务，每个任务是一个约20k-30k tokens的长上下文任务。

OSVBench is a novel benchmark designed to evaluate the capabilities of large language models (LLMs) in generating complete formal specifications relevant to operating system kernel verification tasks. This benchmark first defines the specification generation problem as a program synthesis task within a constrained syntax and semantic scope via a provided programming model. LLMs are required to comprehend the provided verification assumptions and the underlying syntax-semantic space, then generate complete formal specifications for potentially defective operating system code implementations under the guidance of high-level functional descriptions of the operating system. This benchmark is constructed based on the real-world operating system kernel Hyperkernel, and comprises 245 complex specification generation tasks in total, with each task being a long-context task containing approximately 20k to 30k tokens.

原始信息汇总

OSVBench数据集概述

数据集基本信息

• 名称: OSVBench
• 用途: 评估大型语言模型(LLM)在操作系统内核验证任务中生成完整规范代码的能力
• 数据量: 245个复杂规范生成任务
• 任务特点: 每个任务约20k-30k tokens的长上下文任务
• 基础系统: 基于真实操作系统内核Hyperkernel构建

数据集内容

• 基准文件: ./bench_prompts/benchmark.json
• 数据格式: json [ { "syscall": "系统调用名称", "declaration": "系统调用声明", "description": "功能描述", "code": "代码实现", "bug_type": "错误类型", "bug_num": "错误编号" }, ... ]

评估方法

1. 规范生成评估:

   • 通过API调用获取LLM生成的状态机规范
   • 主要参数:
     • --llm: 模型简称
     • --task: 规范生成任务
     • --problem_num: 任务数量
     • --example: 少样本示例文件

2. 功能正确性验证:

   • 使用生成的规范验证Hyperkernel功能正确性
   • 结果存储在./outputs目录

3. 结果统计:

   • 计算Pass@1率
   • 按错误类型分类统计
   • 统计语法和语义错误率

性能对比

机构	模型	错误指针(%)	权限错误(%)	内存泄漏(%)	缓冲区溢出(%)	边界检查(%)	正确代码(%)	总体(%)
OpenAI	GPT-4o	33.80	34.82	32.43	33.33	36.11	42.86	38.78
DeepSeek	DeepSeek-Chat	38.02	39.29	36.49	44.44	43.52	51.02	46.53
Anthropic	Claude-3.5-sonnet	39.44	41.96	39.19	48.15	39.81	46.94	44.90
ByteDance	Doubao-1.5-pro	50.70	48.21	45.95	40.74	52.78	63.27	55.10

许可信息

• 代码许可: Apache License 2.0
• 数据许可: CC BY-NC 4.0

引用文献

BibTex @misc{li2025osvbenchbenchmarkingllmsspecification, title={OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification}, author={Shangyu Li and Juyong Jiang and Tiancheng Zhao and Jiasi Shen}, year={2025}, eprint={2504.20964}, archivePrefix={arXiv}, primaryClass={cs.CL}, url={https://arxiv.org/abs/2504.20964}, }

搜集汇总

数据集介绍

构建方式

OSVBench数据集基于真实操作系统内核Hyperkernel构建，将规范生成问题转化为受限语法和语义范围内的程序合成问题。该数据集包含245个复杂的规范生成任务，每个任务涉及约20k-30k tokens的长上下文，通过提供编程模型、验证假设和高级功能描述，要求大语言模型生成完整的操作系统规范代码。数据集的构建过程严格遵循科学验证流程，确保每个任务都能有效评估模型在操作系统验证领域的性能。

特点

OSVBench数据集具有显著的专业性和挑战性，其任务设计紧密围绕操作系统内核验证的核心问题。数据集覆盖多种典型错误类型，包括指针错误、权限错误、内存泄漏等，全面检验模型在不同场景下的表现。每个任务的长上下文特性对模型的代码理解和生成能力提出更高要求，而基于真实内核的设定则增强了数据集的实用价值。数据集还提供多组few-shot示例，支持不同复杂度的评估需求。

使用方法

使用OSVBench数据集需通过特定命令行工具进行模型评估。用户可选择不同的大语言模型，配置few-shot示例数量，并指定评估任务范围。评估过程分为三个阶段：首先通过API调用获取模型生成的规范代码，随后使用这些规范验证Hyperkernel的功能正确性，最后统计模型在各错误类型上的通过率。数据集提供详细的统计脚本，可自动计算Pass@1率等关键指标，支持研究者进行全面的性能分析。整个过程可通过标准化脚本实现自动化，确保评估结果的可重复性。

背景与挑战

背景概述

OSVBench是由Shangyu Li、Juyong Jiang等学者于2025年提出的创新型基准测试，专注于评估大语言模型在操作系统内核验证任务中生成完整规范代码的能力。该数据集基于真实操作系统内核Hyperkernel构建，包含245个复杂规范生成任务，每个任务涉及约20k-30k tokens的长上下文处理。其核心研究问题在于将规范生成转化为受限语法语义范围内的程序合成问题，要求模型在理解验证假设的基础上，根据操作系统高级功能描述生成精确规范。这项工作显著推进了程序验证与人工智能的交叉领域发展，为衡量大语言模型在系统软件层面的推理能力提供了重要标尺。

当前挑战

OSVBench面临的挑战主要体现在两个维度：在领域问题层面，操作系统验证需要处理复杂的状态机建模和并发控制逻辑，现有模型在长上下文代码生成中表现出显著的性能差异，尤其对指针错误、权限控制等系统级漏洞的识别准确率亟待提升；在构建技术层面，数据集需要平衡真实内核代码的复杂性与评估任务的可行性，既要保持Hyperkernel原始语义完整性，又需设计可量化的评估指标。此外，规范生成涉及多层次的抽象推理，如何构建有效的提示模板和少样本示例来引导模型理解验证假设，成为技术实现的关键难点。

常用场景

经典使用场景

在操作系统内核验证领域，OSVBench数据集为评估大型语言模型（LLMs）在生成完整规范代码方面的能力提供了标准化测试平台。该数据集基于真实操作系统内核Hyperkernel构建，包含245个复杂规范生成任务，每个任务涉及约20k-30k tokens的长上下文代码生成。研究人员通过该数据集能够系统地评估LLMs在理解验证假设、搜索语法和语义空间以及生成完整规范方面的表现，为操作系统验证领域的自动化工具开发提供了重要基准。

解决学术问题

OSVBench有效解决了操作系统验证领域的关键学术问题，包括长上下文代码生成的评估难题、规范自动生成的准确性度量以及不同LLMs在复杂系统任务中的性能比较。通过定义规范生成问题为受限语法和语义范围内的程序合成问题，该数据集为研究者提供了量化评估LLMs在操作系统验证任务中表现的科学方法，填补了该领域缺乏标准化评估工具的空白，推动了自动程序验证技术的发展。

衍生相关工作

基于OSVBench数据集，已衍生出多项重要研究工作。其中包括对12种主流LLMs在操作系统规范生成任务上的系统性评估，揭示了当前模型在长上下文代码生成方面的局限性。该数据集还启发了后续关于增强LLMs系统编程能力的研究，如结合形式化方法的混合验证系统开发。相关成果发表在操作系统和程序语言顶级会议上，推动了程序验证与AI技术的交叉研究发展。