OSVBench

OSVBench是一个用于评估大型语言模型（LLMs）在生成操作系统内核验证任务相关完整规范代码方面的基准。该基准将规范生成问题定义为在语法和语义的限定范围内进行程序合成问题，并为LLMs提供编程模型。LLMs需要理解提供的验证假设和潜在的语法和语义空间，然后在操作系统的高级功能描述的指导下，为可能存在错误的操作系统代码实现生成完整的规范。该基准建立在真实的操作系统内核Hyperkernel之上，总共包含245个复杂的规范生成任务，每个任务大约包含20k到30k个token。我们对12个LLMs的综合评估表明，当前LLMs在操作系统验证的规范生成任务上的性能有限。它们在基准测试上的性能差异显著，突出了它们处理长上下文代码生成任务的能力差异。评估工具包和基准测试可在https://github.com/lishangyuhkust/OSVBench获得。OSVBench is a benchmark for evaluating large language models (LLMs) on the task of generating complete formal specification code related to operating system kernel verification. This benchmark defines the specification generation problem as a program synthesis task within the bounds of syntax and semantics, and provides programming models for LLMs. LLMs are required to understand the provided verification hypotheses and the underlying syntactic and semantic spaces, then generate complete specifications for bug-prone operating system code implementations under the guidance of high-level functional descriptions of the operating system. This benchmark is built on the real operating system kernel Hyperkernel, and contains a total of 245 complex specification generation tasks, each containing approximately 20k to 30k tokens. Our comprehensive evaluation of 12 LLMs shows that the current performance of LLMs on operating system verification specification generation tasks is limited. Their performance on this benchmark varies significantly, highlighting the differences in their ability to handle long-context code generation tasks. The evaluation toolkit and benchmark are available at https://github.com/lishangyuhkust/OSVBench.

搜集汇总

数据集介绍

构建方式

OSVBench数据集的构建基于真实的操作系统内核Hyperkernel，通过定义规范生成问题为一个在限定语法和语义范围内的程序合成问题，为大型语言模型（LLMs）提供编程模型。该数据集包含245个复杂的规范生成任务，每个任务涉及约20k至30k个标记的长上下文任务。构建过程中，首先从Hyperkernel的49个系统调用出发，手动编写多个版本的功能描述，并基于清晰度和技术准确性选择最佳版本。随后，通过向正确的内核实现中随机引入五种真实世界的错误类型，生成包含不同数量错误的代码实现，以模拟现实世界中的操作系统内核验证场景。

使用方法

使用OSVBench数据集时，首先需为LLMs提供任务提示，包括验证假设、编程模型、少量示例和任务问题。LLMs需基于功能描述和潜在错误的代码实现生成对应的状态机规范。生成阶段完成后，通过评估阶段验证生成规范的正确性。评估阶段使用内核验证器对生成规范和基准规范进行对比，确保生成规范在所有内核实现中均能正确识别不一致性。数据集支持多种评估指标，如Pass@N、语法错误率和语义错误率，全面衡量LLMs在规范生成任务中的表现。

背景与挑战

背景概述

OSVBench是由香港科技大学和佐治亚理工学院的研究团队于2025年提出的一个创新性基准测试，专注于评估大语言模型在操作系统内核验证任务中的规范生成能力。该数据集基于真实的Hyperkernel操作系统内核构建，包含245个复杂的规范生成任务，每个任务涉及约20k-30k标记的长上下文处理。其核心研究问题在于探索如何利用大语言模型自动化生成精确的操作系统内核规范，以解决传统人工验证方法耗时耗力且依赖专业知识的瓶颈。OSVBench通过将规范生成问题转化为限定语法和语义范围内的程序合成问题，为操作系统验证领域提供了首个系统化的评估框架，显著推动了形式化方法与人工智能技术的交叉研究。

当前挑战

OSVBench面临的主要挑战体现在两个维度：在领域问题层面，操作系统内核验证需要处理复杂的并发逻辑、硬件交互和状态转换，其规范生成要求模型具备精确的语义映射能力和长程依赖建模能力；在构建过程层面，数据集创建者需要解决真实内核代码的抽象建模、多样化漏洞注入、以及验证假设的形式化表达等难题。具体而言，挑战包括：1)如何确保生成规范与内核实现的语义等价性；2)处理状态机规范与声明式规范之间的复杂约束关系；3)在无限搜索空间中实现有效的程序合成；4)保持长上下文建模的连贯性；5)平衡漏洞类型的代表性与现实性。这些挑战使得OSVBench成为测试大语言模型复杂推理能力的严格基准。

常用场景

经典使用场景

OSVBench作为评估大型语言模型在操作系统内核验证任务中生成规范代码能力的基准，其经典使用场景主要集中在自动化操作系统内核的形式化验证领域。该数据集通过提供编程模型和验证假设，要求模型在受限的语法和语义范围内生成完整的规范代码，以验证可能存在缺陷的内核实现。这种场景下，模型需要充分理解操作系统的高级功能描述，同时掌握形式化验证所需的专业知识和技能。

解决学术问题

OSVBench有效解决了操作系统验证领域中的关键学术问题：自动化规范生成的挑战。传统操作系统验证需要大量人工编写形式化规范，耗费专家数月甚至数年时间。该数据集通过245个复杂规范生成任务，系统评估了LLMs在长上下文代码生成、领域知识理解和形式化语义转换等方面的能力。其创新性在于将规范生成问题重新定义为受限范围内的程序合成问题，为研究LLMs在形式化方法中的应用提供了标准化评估框架。

实际应用

在实际应用中，OSVBench可直接支持操作系统开发中的验证流程自动化。安全关键系统如航空航天、医疗设备和核能控制系统中的操作系统内核，需要严格的形式化验证来确保可靠性。该数据集评估的规范生成能力可大幅降低验证门槛，使更多开发团队能够采用形式化方法。此外，其基于Hyperkernel真实内核的构建方式，确保了评估结果对实际操作系统开发具有直接指导价值。

数据集最近研究

最新研究方向

OSVBench作为首个专注于操作系统内核验证的基准测试工具，其最新研究聚焦于探索大语言模型在长上下文代码生成任务中的边界。随着形式化验证在安全关键领域的重要性日益凸显，该数据集通过245个复杂任务（每个任务约2-3万token）系统评估了12个前沿大模型在规范生成任务上的表现。研究发现，即使是当前最先进的Doubao-1.5-pro模型，其规范生成准确率也仅达55.1%，暴露出大模型在理解操作系统语义空间和验证假设方面的显著局限。该工作为操作系统验证自动化提供了重要基准，同时揭示了模型在硬件交互、并发控制等核心系统编程概念上的认知鸿沟，为后续研究指明了提升模型系统级推理能力的关键方向。

相关研究论文

• OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification

  香港科技大学 · 2025年