論文の概要: Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis

• arxiv url: http://arxiv.org/abs/2504.21061v1
• Date: Tue, 29 Apr 2025 10:02:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-09 23:56:56.522119
• Title: Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis
• Title（参考訳）: スペックを探る:ニューロシンボリックな仕様合成の事例
• Authors: George Granberry, Wolfgang Ahrendt, Moa Johansson,
• Abstract要約: この研究は、Large Language Models (LLM) とシンボリックメソッドを組み合わせて、コードから正式な仕様を生成することに関係している。 まず、コード中のバグの有無が生成された仕様にどのように影響するかを調査する。 第2に,LLMが生成した仕様に対する記号解析の結果の影響について検討する。
• 参考スコア（独自算出の注目度）: 1.2152813244704233
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This work is concerned with the generation of formal specifications from code, using Large Language Models (LLMs) in combination with symbolic methods. Concretely, in our study, the programming language is C, the specification language is ACSL, and the LLM is Deepseek-R1. In this context, we address two research directions, namely the specification of intent vs. implementation on the one hand, and the combination of symbolic analyses with LLMs on the other hand. For the first, we investigate how the absence or presence of bugs in the code impacts the generated specifications, as well as whether and how a user can direct the LLM to specify intent or implementation, respectively. For the second, we investigate the impact of results from symbolic analyses on the specifications generated by the LLM. The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA. We demonstrate how the addition of symbolic analysis to the workflow impacts the quality of annotations.
• Abstract（参考訳）: この研究は、Large Language Models (LLM) とシンボリックメソッドを組み合わせて、コードから正式な仕様を生成することに関係している。 具体的には,プログラミング言語はC,仕様言語はACSL,LLMはDeepseek-R1である。 この文脈では、目的対実装の仕様と、LLMと記号解析の組み合わせの2つの研究方向について述べる。 まず、コード中のバグの有無が生成された仕様にどのように影響するか、また、ユーザがLLMにインテントや実装を指定できるかどうかを調査する。 第2に,LLMが生成した仕様に対する記号解析の結果の影響について検討する。 LLMプロンプトは、Frama-Cエコシステムの2つの形式的なメソッドツール、PathcrawlerとEVAの出力で拡張されている。 ワークフローにシンボリック分析を追加することが、アノテーションの品質にどのように影響するかを実証する。

関連論文リスト

• Aligning Large Language Models to Follow Instructions and Hallucinate Less via Effective Data Filtering [66.5524727179286]
  NOVAは、幻覚を減らすための学習知識とよく一致した高品質なデータを特定するために設計されたフレームワークである。 内部整合性探索(ICP)とセマンティック等価同定(SEI)が含まれており、LLMが命令データとどれだけ親しみやすいかを測定する。 選択したサンプルの品質を確保するため,親しみ以上の特性を考慮した専門家による報酬モデルを導入する。
  論文  参考訳（メタデータ） (2025-02-11T08:05:56Z)
• SpecTool: A Benchmark for Characterizing Errors in Tool-Use LLMs [77.79172008184415]
  SpecToolは、ツール使用タスクのLLM出力のエラーパターンを特定するための新しいベンチマークである。 もっとも顕著なLCMでも,これらの誤りパターンが出力に現れることを示す。 SPECTOOLの分析と洞察を使って、エラー軽減戦略をガイドすることができる。
  論文  参考訳（メタデータ） (2024-11-20T18:56:22Z)
• Large Language Models are Interpretable Learners [53.56735770834617]
  本稿では,Large Language Models(LLM)とシンボルプログラムの組み合わせによって,表現性と解釈可能性のギャップを埋めることができることを示す。 自然言語プロンプトを持つ事前訓練されたLLMは、生の入力を自然言語の概念に変換することができる解釈可能な膨大なモジュールセットを提供する。 LSPが学んだ知識は自然言語の記述と記号規則の組み合わせであり、人間(解釈可能)や他のLLMに容易に転送できる。
  論文  参考訳（メタデータ） (2024-06-25T02:18:15Z)
• Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods [1.2152813244704233]
  我々は,Cプログラムの仕様を合成するために,大規模言語モデルと記号解析の組み合わせをどのように利用できるかを検討する。 この方法は、バグギープログラムの仕様を生成し、バグに対する結果の堅牢性を観察することで、プログラムの振る舞いよりもむしろプログラムの意図を推測する。
  論文  参考訳（メタデータ） (2024-06-21T17:39:57Z)
• Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control [0.7580487359358722]
  時間論理は、反応系の合成と検証に広く使われている強力なツールである。 大規模言語モデルに関する最近の進歩は、そのような仕様を書くプロセスをよりアクセスしやすいものにする可能性がある。
  論文  参考訳（メタデータ） (2024-06-11T16:07:24Z)
• CodecLM: Aligning Language Models with Tailored Synthetic Data [51.59223474427153]
  命令追従能力のための高品質な合成データを適応的に生成するフレームワークであるCodecLMを紹介する。 まず、ターゲットの指示分布をキャプチャするために、オンザフライで生成された簡潔なキーワードであるメタデータにシード命令をエンコードする。 また、デコード中に自己論理とコントラストフィルタを導入し、データ効率の良いサンプルを調整する。
  論文  参考訳（メタデータ） (2024-04-08T21:15:36Z)
• Hint-enhanced In-Context Learning wakes Large Language Models up for knowledge-intensive tasks [54.153914606302486]
  大規模言語モデル(LLM)の規模拡大に伴い、インコンテキスト学習(ICL)能力が出現した。 我々は、オープンドメイン質問応答におけるICLのパワーを探るため、Hint-enhanced In-Context Learning(HICL)と呼ばれる新しいパラダイムを提案する。
  論文  参考訳（メタデータ） (2023-11-03T14:39:20Z)
• ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
  本稿では,LLMベースのフレームワークであるReEvalについて述べる。 本稿では、ChatGPTを用いてReEvalを実装し、2つの人気のあるオープンドメインQAデータセットのバリエーションを評価する。 我々の生成したデータは人間可読であり、大きな言語モデルで幻覚を引き起こすのに役立ちます。
  論文  参考訳（メタデータ） (2023-10-19T06:37:32Z)
• Harnessing the Zero-Shot Power of Instruction-Tuned Large Language Model in End-to-End Speech Recognition [23.172469312225694]
  自動音声認識(ASR)におけるテキスト生成プロセスの指導に,命令調整付き大言語モデル(LLM)を用いることを提案する。 提案手法はCTCとアテンションアーキテクチャを併用し,LLMはデコーダのフロントエンド特徴抽出器として機能する。 実験結果から,LLM誘導モデルによる単語誤り率の相対的な増加率は,主要なベンチマークで約13%であった。
  論文  参考訳（メタデータ） (2023-09-19T11:10:50Z)
• Label Words are Anchors: An Information Flow Perspective for Understanding In-Context Learning [77.7070536959126]
  大規模言語モデル(LLM)の有望な能力としてインコンテキスト学習(ICL)が出現する 本稿では,情報フローレンズを用いたICLの動作機構について検討する。 本稿では,ICL性能向上のためのアンカー再重み付け手法,推論の高速化のための実演圧縮手法,GPT2-XLにおけるICLエラーの診断のための解析フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-05-23T15:26:20Z)
• LMs: Understanding Code Syntax and Semantics for Code Analysis [25.508254718438636]
  我々は,大規模言語モデル(LLM)の機能と,ソフトウェア工学におけるコード解析の限界を評価する。 GPT4, GPT3.5, StarCoder, CodeLlama-13b-インストラクトという,最先端の4つの基礎モデルを採用している。
  論文  参考訳（メタデータ） (2023-05-20T08:43:49Z)

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

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