OS 커널 공식 검증에 필요한 시스템 콜 명세를 LLM이 자동 생성하도록 돕는 도메인 지식 프롬프팅 기법 BODHI를 제안한다. C→Python 변환 지침(15개 카테고리)을 구조적 사고 체인(SCoT) 방식으로 사전 조건·사후 조건 추출로 분리해 표준 Few-shot 프롬프트에 추가한다. OSV-Bench(245개 명세 생성 태스크, 기존 최고 Pass@1 55.10%)에서 6개 사 9개 모델 전체 성능이 +11~+32% 향상됐으며, Claude Opus 4.6 + BODHI 조합이 96.73% Pass@1을 달성했다. 도메인 지식 주입이 구문·의미 오류를 모두 감소시키는 모델 무관 기법임을 입증했다.
- •C→Python 15범주 변환 지침을 SCoT 방식으로 구조화한 BODHI 프롱프팅이 OS 커널 명세 생성 정확도를 +11~+32% 향상.
- •OSV-Bench 6개 사 9개 모델 전체에서 성능 개선, 최고 성능 96.73% Pass@1(Claude Opus 4.6 + BODHI) 달성.
- •도메인 지식 주입이 구문·의미 오류를 모두 감소시키는 모델 무관(model-agnostic) 기법임을 실증.
BODHI: Precise OS Kernel Specification Inference
- 1.BODHI: C→Python 번역 15개 범주 도메인 지식 프롬프트로 LLM의 OS 커널 형식 명세 생성 성능을 모든 모델에서 향상
- 2.OSV-Bench 245개 태스크에서 Claude Opus 4.6 + BODHI 조합이 Pass@1 96.73% 달성 (기존 최고 55.10%)
- 3.6개 공급자 9개 모델(dense·MoE·추론 아키텍처) 평가, 개선폭 +11%~+32%로 모델 무관 기법임을 확인
왜 중요한가?
도메인 지식 주입 프롬프트만으로 범용 코드 생성 모델이 형식 명세 합성 수준에 도달할 수 있음을 입증, OS 커널 형식 검증 자동화의 현실적 가능성을 크게 높였다.
🏷️ 언급 프로젝트
본문 미리보기
arXiv:2605.23931v1 Announce Type: new Abstract: The formal verification of operating system kernels requires precise specifications that capture the intended behavior of system calls. Writing these specifications manually demands deep domain expertise, motivating the use of large language models (LLMs) to automate the process. However, in OSV-Bench, a benchmark of 245 specification generation tasks derived from the Hyperkernel OS kernel, the best reported Pass@1 is 55.10%. We propose a domain k
전체 내용이 궁금하다면?
원문을 직접 읽어보세요
