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不僅減少了語法錯誤，還顯著降低了語義錯誤。其效果在具備較強指令遵循能力、能夠充分利用結構化參考材料的模型上尤為突出。這一結果證明，領域知識注入是一種模型無關的通用技術，能夠有效彌合通用代碼生成與形式化規範合成之間的鴻溝，為操作系統內核的自動化驗證開闢了新的道路。