形式規格生成

深度分析

BODHI：以結構化領域知識提升 LLM 在 OSV-Bench 形式規格生成的準確度

作業系統核心形式驗證需精準規格，但手動撰寫昂貴。BODHI 以結構化 C→Python/Z3 翻譯指南擴充 few-shot prompt，分離前置檢查與後置狀態更新等關切點，並示範 15 類翻譯模式。實驗在 OSV-Bench 上顯著提升多款模型 Pass@1，顯示領域知識注入可實質改善規格生成。