論文の概要: KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base

• arxiv url: http://arxiv.org/abs/2606.21339v1
• Date: Fri, 19 Jun 2026 11:37:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-25 14:17:25.6865
• Title: KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base
• Title（参考訳）: KBSpec: ドメイン知識ベースを進化させるLLM駆動形式仕様生成
• Authors: Wenhan Wang, Zeyu Sun,
• Abstract要約: 本稿では,多言語モデル(LLM)を形式仕様言語コーパスのデュアルソース知識で拡張するKBSpecを提案する。 その結果,KBSpec は最新の LLM ベースのアプローチよりも10-25% の検証パス率向上を実現していることがわかった。
• 参考スコア（独自算出の注目度）: 9.796586560498026
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated formal specification generation is a key step towards program understanding and formal verification. Recently, due to the success of large language models (LLMs) in code generation, researchers have made early attempts to adopt LLMs for generating formal specifications. However, the lack of formal specification language corpora in the wild often makes LLMs fail to generate syntactically correct and semantically verifiable specifications. To mitigate this gap, we propose KBSpec, which augments LLMs with dual-source knowledge of formal specification language: external knowledge from official documentation, and internal knowledge distilled from verifier feedback on LLM-generated specifications. KBSpec maintains a self-evolving knowledge base that is continuously updated from successful generation and repair trajectories, without any LLM parameter tuning or labeled training data. We evaluate KBSpec on Java Modeling Language (JML) specification generation with three LLM backends, and results show that KBSpec improves verification pass rates by 10-25% over state-of-the-art LLM-based approaches, while producing the largest number of high-completeness specifications.
• Abstract（参考訳）: 自動形式仕様生成は、プログラム理解と形式検証のための重要なステップである。 近年、コード生成における大言語モデル(LLM)の成功により、研究者は正式な仕様作成にLLMを採用しようと試みている。 しかし、形式的な仕様言語コーパスが欠如しているため、LLMは構文的に正しく、意味的に検証可能な仕様を生成することができないことが多い。 このギャップを軽減するためにKBSpecを提案する。このKBSpecは、公式文書からの外部知識とLLM生成仕様の検証者フィードバックから抽出された内部知識という、形式仕様言語のデュアルソース知識をLLMに拡張する。 KBSpecは自己進化的な知識ベースを維持しており、LLMパラメータチューニングやラベル付きトレーニングデータなしで、生成と修復の軌道を継続的に更新している。 KBSpec on Java Modeling Language (JML) 仕様生成を3つの LLM バックエンドで評価した結果,KBSpec は最新の LLM ベースのアプローチよりも 10-25% の検証パス率向上を実現し,高完全性仕様の最大数を実現していることがわかった。

関連論文リスト

• Are LLMs Reliable Code Reviewers? Systematic Overcorrection in Requirement Conformance Judgement [8.059802912761919]
  我々は,大規模言語モデル(LLM)が自然言語要求にマッチするコードの体系的失敗を明らかにする。 より詳細なプロンプト設計、特に説明や修正提案を必要とするものは、より高い誤判定率をもたらす。 そこで本稿では,提案した修正を実効的証拠として扱う固定誘導検証フィルタを提案する。
  論文  参考訳（メタデータ） (2026-02-28T08:35:25Z)
• Aligning Requirement for Large Language Model's Code Generation [9.205909320363247]
  Specineは、大規模言語モデル(LLM)コード生成のための新しい仕様アライメント技術である。 その鍵となる考え方は、不整合入力仕様を特定し、LLMが認識した仕様を引き上げ、LLMのコード生成性能を高めるためにそれらを整合させることである。 例えば、Specineは最も効果的なベースラインを上回り、Pass@1ですべての被験者の平均29.60%の改善を達成した。
  論文  参考訳（メタデータ） (2025-09-01T09:56:13Z)
• How Reliable are LLMs as Knowledge Bases? Re-thinking Facutality and Consistency [60.25969380388974]
  大規模言語モデル (LLM) は知識ベース (KB) として研究されている。 現在の評価手法は、信頼性の高い性能の他の決定的な基準を見越して、知識の保持に過度に焦点を絞っている。 我々は,事実と一貫性を定量化するための新しい基準と指標を提案し,最終的な信頼性スコアを導いた。
  論文  参考訳（メタデータ） (2024-07-18T15:20:18Z)
• FOFO: A Benchmark to Evaluate LLMs' Format-Following Capability [70.84333325049123]
  FoFoは、大規模言語モデル(LLM)の複雑なドメイン固有のフォーマットに従う能力を評価するための先駆的なベンチマークである。 本稿では,大規模言語モデル(LLM)の複雑なドメイン固有フォーマットに従う能力を評価するための先駆的ベンチマークであるFoFoを提案する。
  論文  参考訳（メタデータ） (2024-02-28T19:23:27Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  大型言語モデル(LLM)は、自然言語と形式言語(コード)の組み合わせに基づいて訓練される コードは、標準構文、論理一貫性、抽象化、モジュール性を備えた高レベルの目標を実行可能なステップに変換する。
  論文  参考訳（メタデータ） (2024-01-01T16:51:20Z)
• Configuration Validation with Large Language Models [22.018488540410548]
  大きな言語モデル(LLM)は、MLベースの構成検証の長期的制限に対処する上で、有望であることを示している。 汎用的なLCMベースの構成検証フレームワークCiriを開発した。 Ciriは有効なプロンプトエンジニアリングを採用し、有効な設定データと設定ミスデータの両方に基づいて数ショットの学習を行う。
  論文  参考訳（メタデータ） (2023-10-15T00:50:27Z)
• How Effective are Large Language Models in Generating Software Specifications? [14.170320751508502]
  大規模言語モデル(LLM)は多くのソフトウェア工学(SE)タスクにうまく適用されている。 ソフトウェアコメントやドキュメンテーションからソフトウェア仕様を生成するためのLCMの能力を評価するための、最初の実証的研究を行う。
  論文  参考訳（メタデータ） (2023-06-06T00:28:39Z)
• Augmented Large Language Models with Parametric Knowledge Guiding [72.71468058502228]
  大規模言語モデル(LLM)は、言語理解と生成能力に優れた自然言語処理(NLP)を備えています。 それらのパフォーマンスは、関連するデータへの限られた露出のために専門的な知識を必要とするドメイン固有のタスクに最適であるかもしれない。 本稿では,LLMに関連知識にアクセスするための知識誘導モジュールを組み込んだ新しいPKGフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-05-08T15:05:16Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。