論文の概要: BODHI: Precise OS Kernel Specification Inference
- arxiv url: http://arxiv.org/abs/2605.23931v1
- Date: Wed, 22 Apr 2026 19:29:16 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-15 07:09:36.479536
- Title: BODHI: Precise OS Kernel Specification Inference
- Title（参考訳）: BODHI: OSカーネルの正確な仕様推論
- Authors: Zhiming Chang, Ziyang Li,
- Abstract要約: 245の仕様生成タスクのベンチマークであるOSV-Benchでは、最もよく報告されているPass@1は55.10%である。
構造化されたC-to-Python翻訳ガイドを用いて,標準的な数ショットプロンプトを増強するドメイン知識プロンプト手法(BODHI)を提案する。
- 参考スコア（独自算出の注目度）: 11.243181562664802
- License: http://creativecommons.org/licenses/by/4.0/
- 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 knowledge prompting method (BODHI), which augments the standard few-shot prompt with a structured C-to-Python translation guide covering 15 categories of domain-specific translation patterns. Inspired by Structured Chain-of-Thought (SCoT) prompting, the guide organizes translation by separation of concerns, addressing pre-condition extraction and post-condition generation as distinct categories. Evaluated on nine models from six providers (Anthropic, Mistral, Amazon, DeepSeek, Meta, Alibaba), covering dense, mixture-of-experts and reasoning architectures, BODHI improves every model tested, with gains ranging from +11% to +32%. The best configuration (Claude Opus 4.6 + BODHI) reaches 96.73% Pass@1. BODHI reduces both syntax and semantic errors, with the strongest effect on models that have sufficient instruction-following capability to utilize structured reference material. These results demonstrate that domain knowledge injection is a model-agnostic technique that substantially bridges the gap between general-purpose code generation and formal specification synthesis.
- Abstract（参考訳）: オペレーティングシステムカーネルの正式な検証には、システムコールの意図した振る舞いをキャプチャする正確な仕様が必要である。
これらの仕様を手作業で記述するには、プロセスを自動化するために大きな言語モデル(LLM)を使用する動機となる、深いドメインの専門知識が必要です。
しかし、Hyperkernel OSカーネルから派生した245の仕様生成タスクのベンチマークであるOSV-Benchでは、最も報告されているPass@1は55.10%である。
ドメイン固有の翻訳パターンの15のカテゴリをカバーする構造付きC-to-Python翻訳ガイドを用いて、標準的な数ショットプロンプトを増強するドメイン知識プロンプト手法(BODHI)を提案する。
構造化連鎖(Structured Chain-of-Thought, SCoT)にインスパイアされたガイドは、関心事の分離によって翻訳を整理し、事前条件抽出と後条件生成を異なるカテゴリとして扱う。
6つのプロバイダ(Anthropic、Mistral、Amazon、DeepSeek、Meta、Alibaba)の9つのモデルから評価され、密集したエキスパートと推論アーキテクチャをカバーする。
最高の設定(Claude Opus 4.6 + BODHI)は96.73%のPass@1に達する。
BODHIは構文と意味的誤りを減らし、構造化された参照材料を利用するのに十分な命令追従能力を持つモデルに最も強い影響を与える。
これらの結果から,ドメイン知識注入は汎用コード生成と形式仕様合成のギャップを著しく埋めるモデルに依存しない手法であることが示唆された。
関連論文リスト
- A Hybrid Vision-Language Architecture for Automated Defect Reasoning and Report Generation in Industrial Inspection [0.42970700836450487]
本稿では,風力タービン羽根試験用分離・エッジ展開可能なパイプラインについて述べる。
The EyesはY26-x-obb指向のバウンディングボックスで、データセットネイティブの解像度で欠陥をローカライズする。
ブリッジは決定論的でパラメータフリーな符号化モジュールであり、検出された各バウンディングボックスをグリッド参照トークンにマップする。
論文 参考訳（メタデータ） (2026-05-26T04:27:38Z) - Context-Instrumental Data Distillation for Kubernetes Manifest Generation: Method and Experimental Evaluation [36.94429692322632]
本稿では,ドメイン固有言語(AML)におけるアーティファクトを生成するために,最大40億のパラメータを持つ小言語モデルの特殊化について検討する。
本稿では, 実Yファイルからの逆命令生成により, ソースコーパスを合成生成し, 拡張スキームで生成する, 文脈構造データ蒸留法を提案する。
論文 参考訳（メタデータ） (2026-05-25T13:30:38Z) - DocAtlas: Multilingual Document Understanding Across 80+ Languages [58.715440331861295]
本稿では,82言語を対象とした高忠実度OCRデータセットとベンチマークを構築するフレームワークDocAtlasを紹介する。
我々のデュアルパイプライン、ネイティブDOCX文書の微分レンダリング、左右スクリプトの合成ベース生成は正確な構造アノテーションを生成する。
論文 参考訳（メタデータ） (2026-05-12T18:09:38Z) - SecGoal: A Benchmark for Security Goal Extraction and Formalization from Protocol Documents [3.363429643522915]
SecGoalは15の広くデプロイされたプロトコルドキュメントをカバーする最初のエキスパートアノテーション付きベンチマークである。
我々は、タスクをコンテキスト対応のゴール抽出に分解するAI支援フレームワークであるSecGoalとAIFGを紹介する。
論文 参考訳（メタデータ） (2026-04-30T08:50:03Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Infinity Instruct: Scaling Instruction Selection and Synthesis to Enhance Language Models [14.927052028174744]
Infinity-Instructは、大規模言語モデルの基本機能とチャット機能の両方を強化するために設計された高品質な命令データセットである。
我々は、Mistral、LLaMA、Qwen、Yiなどのオープンソースモデルを微調整して、Infinity-Instructを実証的に評価し、基礎的および命令的ベンチマークの両方でかなりの性能向上を観察する。
論文 参考訳（メタデータ） (2025-06-09T06:37:15Z) - How Far Can Camels Go? Exploring the State of Instruction Tuning on Open
Resources [117.6496550359768]
この研究は、オープンな命令追従データセットにおける命令チューニング言語モデルの最近の進歩を探求する。
我々は、12の命令データセットに基づいて訓練された6.7Bから65Bのパラメータを含む、命令調整されたモデルの大規模なセットを提供する。
それらの事実的知識、推論、多言語性、コーディング、そしてその後に続くオープン・エンド・インストラクションに基づいて評価する。
論文 参考訳（メタデータ） (2023-06-07T19:59:23Z) - Scaling Instruction-Finetuned Language Models [126.4789306516927]
命令として表現されたデータセットの集合上での言語モデルの微調整は、モデル性能を改善することが示されている。
命令の微調整により,様々なモデルクラスの性能が劇的に向上することがわかった。
論文 参考訳（メタデータ） (2022-10-20T16:58:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。