論文の概要: Extracting Formal Specifications from Documents Using LLMs for Automated Testing

• arxiv url: http://arxiv.org/abs/2504.01294v1
• Date: Wed, 02 Apr 2025 01:58:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-04-03 13:23:55.631180
• Title: Extracting Formal Specifications from Documents Using LLMs for Automated Testing
• Title（参考訳）: 自動テストのためのLCMを用いた文書からの形式仕様抽出
• Authors: Hui Li, Zhen Dong, Siao Wang, Hui Zhang, Liwei Shen, Xin Peng, Dongdong She,
• Abstract要約: 正式な仕様を定義する主なアプローチは、ソフトウェア文書のマニュアル分析である。 システム更新は、対応する正式な仕様を維持するための人件費をさらに高める。 大規模言語モデルの最近の進歩は、自然言語理解において有望な能力を示している。
• 参考スコア（独自算出の注目度）: 11.129512305353055
• License:
• Abstract: Automated testing plays a crucial role in ensuring software security. It heavily relies on formal specifications to validate the correctness of the system behavior. However, the main approach to defining these formal specifications is through manual analysis of software documents, which requires a significant amount of engineering effort from experienced researchers and engineers. Meanwhile, system update further increases the human labor cost to maintain a corresponding formal specification, making the manual analysis approach a time-consuming and error-prone task. Recent advances in Large Language Models (LLMs) have demonstrated promising capabilities in natural language understanding. Yet, the feasibility of using LLMs to automate the extraction of formal specifications from software documents remains unexplored. We conduct an empirical study by constructing a comprehensive dataset comprising 603 specifications from 37 documents across three representative open-source software. We then evaluate the most recent LLMs' capabilities in extracting formal specifications from documents in an end-to-end fashion, including GPT-4o, Claude, and Llama. Our study demonstrates the application of LLMs in formal specification extraction tasks while identifying two major limitations: specification oversimplification and specification fabrication. We attribute these deficiencies to the LLMs' inherent limitations in processing and expressive capabilities, as well as their tendency to fabricate fictional information. Inspired by human cognitive processes, we propose a two-stage method, annotation-then-conversion, to address these challenges. Our method demonstrates significant improvements over the end-to-end method, with a 29.2% increase in the number of correctly extracted specifications and a 14.0% improvement in average accuracy. In particular, our best-performing LLM achieves an accuracy of 71.6%.
• Abstract（参考訳）: 自動テストは、ソフトウェアのセキュリティを確保する上で重要な役割を担います。 システムの振舞いの正しさを検証するために、形式的な仕様に大きく依存しています。 しかし、これらの正式な仕様を定義する主なアプローチは、経験豊富な研究者やエンジニアによるかなりの量のエンジニアリング作業を必要とするソフトウェア文書のマニュアル分析である。 一方、システム更新により、対応する形式仕様を維持するための人件費がさらに増加し、手作業による分析アプローチは時間がかかり、エラーが発生しやすいタスクとなる。 大規模言語モデル(LLM)の最近の進歩は、自然言語理解において有望な能力を示している。 しかし、ソフトウェア文書からの正式な仕様の抽出を自動化するためにLLMを使うことの可能性については、未検討のままである。 3つの代表的なオープンソースソフトウェアにわたる37の文書から603の仕様からなる包括的データセットを構築することにより、実証的研究を行う。 次に、GPT-4o、Claude、Llamaを含む文書から文書から形式仕様を抽出する最新のLCMの能力を評価する。 本研究では,LLMを形式的仕様抽出タスクに適用し,仕様の単純化と仕様作成という2つの大きな制約を同定する。 これらの欠陥は、LLMの処理能力と表現能力の限界、および架空の情報を作成する傾向に起因している。 人間の認知プロセスに触発されて,これらの課題に対処するための2段階のアノテーション-then-conversion法を提案する。 提案手法は, エンド・ツー・エンド法に対して, 正確な仕様抽出回数が29.2%増加し, 平均精度が14.0%向上した。 特に、最高の性能のLCMは71.6%の精度を実現しています。

関連論文リスト

• Truth or Mirage? Towards End-to-End Factuality Evaluation with LLM-Oasis [78.07225438556203]
  LLM-Oasisは、エンド・ツー・エンドの事実性評価をトレーニングするための最大のリソースである。 ウィキペディアからクレームを抽出し、これらのクレームのサブセットを偽造し、事実と非事実のテキストのペアを生成することで構築される。 次に、データセットの品質を検証し、事実性評価システムのための金の標準テストセットを作成するために、人間のアノテータに依存します。
  論文  参考訳（メタデータ） (2024-11-29T12:21:15Z)
• Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting [0.0]
  高品質なシステムVerilog Assertions (SVA) を自動生成する大規模言語モデル(LLM)に基づくフローを提案する。 サブタスクに着目したファインチューニング手法を導入し,機能的に正しいアサーションの数を7.3倍に増やした。 実験では、このアプローチを使って構文エラーのないアサーション数が26%増加した。
  論文  参考訳（メタデータ） (2024-11-23T03:52:32Z)
• Exploring LLMs for Verifying Technical System Specifications Against Requirements [41.19948826527649]
  知識に基づく要求工学(KBRE)の分野は、システム要件の活用、検証、管理を支援する知識を提供することによって、技術者を支援することを目的としている。 大規模言語モデル(LLM)の出現はKBREの分野で新たな機会を開く。 本研究は, LLMの要件検証における可能性について実験的に検討する。
  論文  参考訳（メタデータ） (2024-11-18T13:59:29Z)
• Exploring Automatic Cryptographic API Misuse Detection in the Era of LLMs [60.32717556756674]
  本稿では,暗号誤用の検出において,大規模言語モデルを評価するための体系的評価フレームワークを提案する。 11,940個のLCM生成レポートを詳細に分析したところ、LSMに固有の不安定性は、報告の半数以上が偽陽性になる可能性があることがわかった。 最適化されたアプローチは、従来の手法を超え、確立されたベンチマークでこれまで知られていなかった誤用を明らかにすることで、90%近い顕著な検出率を達成する。
  論文  参考訳（メタデータ） (2024-07-23T15:31:26Z)
• SELF-GUIDE: Better Task-Specific Instruction Following via Self-Synthetic Finetuning [70.21358720599821]
  大規模言語モデル(LLM)は、適切な自然言語プロンプトを提供する際に、多様なタスクを解決するという約束を持っている。 学生LLMからタスク固有の入出力ペアを合成する多段階メカニズムであるSELF-GUIDEを提案する。 ベンチマークの指標から,分類タスクに約15%,生成タスクに18%の絶対的な改善を報告した。
  論文  参考訳（メタデータ） (2024-07-16T04:41:58Z)
• DOCBENCH: A Benchmark for Evaluating LLM-based Document Reading Systems [99.17123445211115]
  本稿では,大規模言語モデル(LLM)に基づく文書読解システムを評価するベンチマークであるDocBenchを紹介する。 我々のベンチマークには、人間のアノテーションの募集と、合成質問の生成が含まれる。 実際の文書は229件、質問は1,102件で、5つのドメインにまたがって4種類の質問がある。
  論文  参考訳（メタデータ） (2024-07-15T13:17:42Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• FOFO: A Benchmark to Evaluate LLMs' Format-Following Capability [70.84333325049123]
  FoFoは、大規模言語モデル(LLM)の複雑なドメイン固有のフォーマットに従う能力を評価するための先駆的なベンチマークである。 本稿では,大規模言語モデル(LLM)の複雑なドメイン固有フォーマットに従う能力を評価するための先駆的ベンチマークであるFoFoを提案する。
  論文  参考訳（メタデータ） (2024-02-28T19:23:27Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。 SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
  論文  参考訳（メタデータ） (2024-01-16T20:13:50Z)
• How Effective are Large Language Models in Generating Software Specifications? [14.170320751508502]
  大規模言語モデル(LLM)は多くのソフトウェア工学(SE)タスクにうまく適用されている。 ソフトウェアコメントやドキュメンテーションからソフトウェア仕様を生成するためのLCMの能力を評価するための、最初の実証的研究を行う。
  論文  参考訳（メタデータ） (2023-06-06T00:28:39Z)
• Estimating Large Language Model Capabilities without Labeled Test Data [51.428562302037534]
  大規模言語モデル(LLM)は、ほんの数例からICL(In-context Learning)を実行するという印象的な能力を持っている。 ICLの精度推定タスクを提案し、新しいタスクで文脈内学習を行う場合のLLMの精度を予測する。
  論文  参考訳（メタデータ） (2023-05-24T06:55:09Z)

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

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