BODHI: 精确的操作系统内核规范推断
研究人员提出BODHI方法，通过领域知识提示技术大幅提升大型语言模型生成操作系统内核形式化规范的能力。在OSV-Bench基准上，结合Claude Opus 4.6的BODHI方法达到了96.73%的Pass@1，相较于此前最佳结果提升显著。
文章情报
要点
- BODHI是一种领域知识提示方法，通过结构化C到Python转换指南辅助LLM生成内核规范。
- 在OSV-Bench的245个规范生成任务上，BODHI将最佳Pass@1从55.10%提升至96.73%。
- 该方法在来自6家提供商的9个模型上均有效，性能提升11%至32%。
为什么重要
这条新闻值得关注，因为BODHI是一种领域知识提示方法，通过结构化C到Python转换指南辅助LLM生成内核规范。
技术影响
可能影响模型选型、推理成本、产品能力和评测基准。
操作系统的形式化验证是确保其安全性与可靠性的关键手段，而这一过程高度依赖于精确的系统调用规范。传统上，编写这些规范需要专家手动完成，不仅成本高昂，而且极易出错。为了克服这一瓶颈，研究人员开始探索利用大型语言模型（LLM）来自动生成形式化规范。然而，在基于Hyperkernel操作系统的OSV-Bench基准测试中——该基准包含245个规范生成任务——此前最好的Pass@1指标仅为55.10%，远未达到实用水平。
针对这一挑战，来自多家机构的研究团队提出了BODHI（领域知识提示方法）。该方法在标准少样本提示的基础上，引入了一个结构化的C到Python转换指南，该指南系统性地覆盖了15类领域特定的转换模式。受结构化思维链（SCoT）提示的启发，该指南按照关注点分离的原则组织，将前置条件提取和后置条件生成区分为不同的处理类别，从而有效提升了模型对复杂语义的理解能力。
研究团队在来自Anthropic、Mistral、Amazon、DeepSeek、Meta和阿里巴巴等六家提供商的九个模型上展开了全面评估，这些模型涵盖了密集型、混合专家型和推理型等多种架构。实验结果显示，BODHI方法在所有测试模型上均带来了显著的性能提升，提升幅度从11%到32%不等。其中，最佳配置——即Claude Opus 4.6与BODHI的结合——在OSV-Bench上实现了96.73%的Pass@1，几乎是此前最优结果的两倍。
进一步的分析表明，BODHI不仅减少了语法错误，还显著降低了语义错误。其效果在具备较强指令遵循能力、能够充分利用结构化参考材料的模型上尤为突出。这一结果证明，领域知识注入是一种模型无关的通用技术，能够有效弥合通用代码生成与形式化规范合成之间的鸿沟，为操作系统内核的自动化验证开辟了新的道路。