BODHI：精确的操作系统内核规范推断

arXiv:2605.23931v1 公告类型：新 摘要：操作系统内核的形式验证需要精确的规范来捕获系统调用的预期行为。手动编写这些规范需要深厚的领域专业知识，因此需要使用大型语言模型 (LLM) 来自动化该过程。然而，在 OSV-Bench（源自 Hyperkernel OS 内核的 245 个规范生成任务的基准）中，最佳报告的 Pass@1 为 55.10%。我们提出了一种领域知识提示方法（BODHI），该方法通过涵盖 15 类特定领域翻译模式的结构化 C 到 Python 翻译指南来增强标准的小样本提示。受结构化思维链 (SCoT) 提示的启发，该指南通过关注点分离来组织翻译，将前置条件提取和后置条件生成作为不同的类别进行处理。 BODHI 对来自 6 个提供商（Anthropic、Mistral、Amazon、DeepSeek、Meta、Alibaba）的 9 个模型进行了评估，涵盖密集、专家混合和推理架构，BODHI 改进了每个测试的模型，增益范围从 +11% 到 +32%。最佳配置（Claude Opus 4.6 + BODHI）达到96.73% Pass@1。 BODHI 减少了语法和语义错误，对具有足够的指令跟踪能力以利用结构化参考材料的模型效果最强。这些结果表明，领域知识注入是一种与模型无关的技术，它基本上弥合了通用代码生成和形式规范综合之间的差距。