BODHI: новый метод повышает точность генерации спецификаций ядра ОС до 96,73%
Формальная верификация ядер операционных систем требует точных спецификаций, описывающих ожидаемое поведение системных вызовов. Ручное написание таких спецификаций требует глубоких знаний предметной области, что стимулирует использование больших языковых моделей (LLM) для автоматизации процесса. Однако на бенчмарке OSV-Bench, содержащем 245 задач генерации спецификаций из ядра Hyperkernel, лучший показатель Pass@1 составлял лишь 55,10%.
Для решения этой проблемы исследователи разработали метод BODHI (domain knowledge prompting method). Он дополняет стандартный few-shot prompt структурированным руководством по переводу с C на Python, охватывающим 15 категорий предметно-ориентированных шаблонов. Вдохновленный техникой Structured Chain-of-Thought (SCoT), метод разделяет задачи на извлечение предусловий и генерацию постусловий.
BODHI протестировали на девяти моделях от шести провайдеров: Anthropic, Mistral, Amazon, DeepSeek, Meta и Alibaba. Среди них были плотные, смешанные экспертные и рассуждающие архитектуры. Улучшение составило от +11% до +32% для каждой модели. Лучший результат показала конфигурация Claude Opus 4.6 с BODHI — 96,73% Pass@1.
Метод снижает как синтаксические, так и семантические ошибки. Наибольший эффект наблюдался у моделей с достаточной способностью следования инструкциям для использования структурированного справочного материала. Результаты показывают, что инъекция предметных знаний является модельно-агностической техникой, значительно сокращающей разрыв между генерацией кода общего назначения и синтезом формальных спецификаций.
Статья опубликована на arXiv под идентификатором 2605.23931. Исследование демонстрирует практический подход к автоматизации сложной инженерной задачи, имеющей значение для верификации операционных систем.
