BODHI：面向操作系统内核规约的领域知识提示方法
这篇题为《BODHI: Precise OS Kernel Specification Inference》的论文于2026年4月22日提交至arXiv，作者为Zhiming Chang与另一位合作者，论文编号为arXiv:2605.23931，归类于cs.AI，并同时涉及cs.PL（编程语言）与cs.SE（软件工程）两个方向。该工作关注的是操作系统内核形式化验证中的一个核心难题：如何获得精确、可用的系统调用规约。
操作系统内核的形式化验证需要精确的规约来刻画系统调用的预期行为。手工编写这些规约要求研究者具备深厚的领域专业知识，这促使研究者尝试用大语言模型（LLM）来自动完成这一过程。然而在OSV-Bench这一基准测试上，现有方法的表现并不理想。OSV-Bench包含245个规格生成任务，全部源自Hyperkernel操作系统内核，此前报告的最佳Pass@1成绩仅为55.10%，说明通用代码生成能力与形式规约合成之间仍存在明显鸿沟。
针对这一问题，作者提出了名为BODHI的领域知识提示方法。该方法在标准的少样本（few-shot）提示基础上，额外加入一份结构化的C到Python翻译指南，这份指南系统性地覆盖了15类领域特定的翻译模式。受结构化思维链（Structured Chain-of-Thought，SCoT）提示思想的启发，该指南按照关注点分离的原则组织翻译过程，将前置条件提取与后置条件生成划分为不同的类别分别处理，从而让模型在生成规约时能够有条理地分步推理，而不是一次性给出缺乏依据的结果。
在实验评估方面，研究团队选取了来自六家提供商的九个模型，分别是Anthropic、Mistral、Amazon、DeepSeek、Meta和Alibaba，覆盖了稠密模型、混合专家（MoE）模型以及推理型架构等多种类型。结果显示，BODHI对每一个被测模型都有提升，增益范围在+11%到+32%之间。其中最佳配置为Claude Opus 4.6配合BODHI，达到了96.73%的Pass@1成绩，相比此前55.10%的最好水平有大幅跃升。
作者进一步分析指出，BODHI同时减少了语法错误和语义错误。值得注意的是，该方法的效果在不同模型上并不均匀：对于那些具备足够指令遵循能力、能够有效利用结构化参考材料的模型，提升最为显著。这也意味着，领域知识注入并非万能，其收益在一定程度上取决于模型本身能否正确理解并运用所提供的结构化指南。
论文的结论是，领域知识注入是一种与具体模型无关（model-agnostic）的技术，能够显著缩小通用代码生成能力与形式化规约合成之间的差距。这一发现对于操作系统内核验证、乃至更广泛的程序规约自动生成领域都具有参考价值。论文全文可通过arXiv获取PDF、实验性HTML版本以及TeX源码，DOI为10.48550/arXiv.2605.23931，提交记录显示该版本于2026年4月22日19:29:16 UTC提交，文件大小约31 KB。