論文の概要: Improving Dynamic Specification Inference with LLM-Generated Counterexamples

• arxiv url: http://arxiv.org/abs/2604.10761v1
• Date: Sun, 12 Apr 2026 18:09:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-14 20:13:16.20431
• Title: Improving Dynamic Specification Inference with LLM-Generated Counterexamples
• Title（参考訳）: LLM生成反例による動的仕様推論の改善
• Abstract要約: 本稿では,生成したアサーションを無効にしようとするテストを自動的に生成する大規模言語モデル(LLM)について検討する。 その結果,現在最先端のLCMは,SpecFuzzerが推定する無効なアサーションの最大11.68%を破棄する有効な反例を生成できることがわかった。
• 参考スコア（独自算出の注目度）: 3.555888578860533
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Contract assertions, such as preconditions, postconditions, and invariants, play a crucial role in software development, enabling applications such as program verification, test generation, and debugging. Despite their benefits, the adoption of contract assertions is limited, due to the difficulty of manually producing such assertions. Dynamic analysis-based approaches, such as Daikon, can aid in this task by inferring expressive assertions from execution traces. However, a fundamental weakness of these methods is their reliance on the thoroughness of the test suites used for dynamic analysis. When these test suites do not contain sufficiently diverse tests, the inferred assertions are often not generalizable, leading to a high rate of invalid candidates (false positives) that must be manually filtered out. In this paper, we explore the use of large language models (LLMs) to automatically generate tests that attempt to invalidate generated assertions. Our results show that state-of-the-art LLMs can generate effective counterexamples that help to discard up to 11.68\% of invalid assertions inferred by SpecFuzzer. Moreover, when incorporating these LLM-generated counterexamples into the dynamic analysis process, we observe an improvement of up to 7\% in precision of the inferred specifications, with respect to the ground-truths gathered from the evaluation benchmarks, without affecting recall.
• Abstract（参考訳）: 事前条件、後条件、不変性といった契約の主張は、プログラム検証、テスト生成、デバッグといったアプリケーションを可能にするソフトウェア開発において重要な役割を果たす。 これらのメリットにもかかわらず、契約のアサーションの採用は、手作業によるアサーションの生成が困難であるため、制限されている。 ダイコンのような動的解析ベースのアプローチは、実行トレースから表現力のあるアサーションを推測することで、このタスクを支援することができる。 しかし、これらの手法の根本的な弱点は、動的解析に使用されるテストスイートの徹底性に依存することである。 これらのテストスイートが十分に多様なテストを含んでいない場合、推論されたアサーションは一般化できないことが多く、手動でフィルタリングしなければならない不正な候補(偽陽性)の比率が高くなる。 本稿では,生成したアサーションを無効にしようとするテストを自動的に生成する大規模言語モデル(LLM)について検討する。 以上の結果から,現在最先端のLCMは,SpecFuzzerが推定する無効なアサーションの最大11.68 %を破棄する有効な反例を生成できることが示唆された。 さらに, これらのLCM生成反例を動的解析プロセスに組み込むことで, 評価ベンチマークから収集した基礎構造に対して, 評価仕様の精度を最大7倍に向上させることができた。

関連論文リスト

• Evaluating and Mitigating the Misguidance Effect of Buggy Code in LLM-Generated Unit Tests [6.228248513679207]
  本稿では,その誤動作を検証するテストを生成するために,バギーコードによるLSMを誘導する現象である「誤用効果」を測定するための新しい指標を提案する。 我々は,テスト中のコードをLCM生成した仕様文書に置き換える仕様ベースの単体テスト生成パラダイムを導入し,検証する。 本研究の結果から,このパラダイムは誤操作を効果的に低減し,有効なテストを大幅に増加させ,複数ラウンドのフィードバック駆動型テスト生成パイプラインを改善し,バグやバグのないコードにも適用可能であることが示唆された。
  論文  参考訳（メタデータ） (2026-07-24T19:47:41Z)
• Neuroforger: certified violation witnesses for smart contracts verification via LLMs [0.0]
  近年の大規模言語モデル(LLM)では、スマートコントラクトが特定のプロパティを尊重するかどうかを予測できる推論機能が組み込まれている。 抽象型でSolidityを拡張する新しい形式仕様言語を導入する。 LLMと型チェックと具体的な実行を組み合わせたワークフローを設計し、違反証人を生成し検証する。
  論文  参考訳（メタデータ） (2026-05-29T14:54:51Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• RESTestBench: A Benchmark for Evaluating the Effectiveness of LLM-Generated REST API Test Cases from NL Requirements [0.13681174239726607]
  RESTestBenchは、手動で検証されたNL要求と組み合わせた3つのRESTサービスからなるベンチマークである。 我々は,複数の最先端LCMに対して, (i)非リファインメントベース生成と (ii) 動作中のSUTとの相互作用によって誘導されるリファインメントベース生成の2つのアプローチを評価する。
  論文  参考訳（メタデータ） (2026-04-28T16:59:08Z)
• On the Soundness and Consistency of LLM Agents for Executing Test Cases Written in Natural Language [4.290931412096985]
  グラフィカルユーザインタフェース(GUI)アプリケーションを検証するための自然言語(NL)テストケースの利用は、将来性のある方向として現れつつある。 大規模言語モデル(LLM)の最近の進歩は、LLMエージェントによるNLテストケースの直接実行の可能性を広げている。 本稿では,NLテストケースの不協和性とテストケース実行の整合性に与える影響について検討する。
  論文  参考訳（メタデータ） (2025-09-23T15:20:40Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• Toward Automated Validation of Language Model Synthesized Test Cases using Semantic Entropy [0.5057850174013127]
  現代の大規模言語モデル(LLM)ベースのプログラミングエージェントは、しばしば、生成されたコードを洗練するためにテスト実行フィードバックに依存する。 本稿では,LLMが生成したテストケースの自動検証にセマンティックエントロピーを利用する新しいフレームワークVALTESTを紹介する。 VALTESTはテストの妥当性を最大29%向上し、パス@1スコアの大幅な増加によって証明されたコード生成のパフォーマンスが向上することを示している。
  論文  参考訳（メタデータ） (2024-11-13T00:07:32Z)
• AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
  本稿では,アサーション生成におけるLarge-Language Modelsの有効性を評価するための新しいベンチマークを提案する。 AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
  論文  参考訳（メタデータ） (2024-06-26T14:47:28Z)
• Prompt Optimization with EASE? Efficient Ordering-aware Automated Selection of Exemplars [66.823588073584]
  大規模言語モデル(LLM)は、現実世界のアプリケーションで印象的な機能を示している。 これらの卓越した作品の品質は、パフォーマンスに大きな影響を与えます。 既存の方法は、先行注文がパフォーマンスに与える影響を適切に説明できない。
  論文  参考訳（メタデータ） (2024-05-25T08:23:05Z)
• Self-Evaluation Improves Selective Generation in Large Language Models [54.003992911447696]
  オープンエンド生成タスクをトークンレベルの予測タスクに再構成する。 我々はLSMに答えを自己評価するように指示する。 自己評価に基づくスコアリング手法をベンチマークする。
  論文  参考訳（メタデータ） (2023-12-14T19:09:22Z)
• 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)
• LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyond [135.8013388183257]
  そこで我々は,SummEditsと呼ばれる10ドメインのベンチマークで不整合検出ベンチマークを作成し,実装する新しいプロトコルを提案する。 ほとんどのLLMはSummEditsで苦労しており、パフォーマンスはランダムに近い。 最も優れたモデルであるGPT-4は、推定された人間のパフォーマンスよりも8%低い。
  論文  参考訳（メタデータ） (2023-05-23T21:50:06Z)

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

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