論文の概要: 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生成反例による動的仕様推論の改善
• Authors: Agustín Balestra, Agustín Nolasco, Facundo Molina, Diego Garbervetsky, Renzo Degiovanni, Nazareno Aguirre,
• 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倍に向上させることができた。

関連論文リスト

• 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)

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

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