論文の概要: Validating Formal Specifications with LLM-generated Test Cases

• arxiv url: http://arxiv.org/abs/2510.23350v1
• Date: Mon, 27 Oct 2025 14:02:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-28 15:28:15.567113
• Title: Validating Formal Specifications with LLM-generated Test Cases
• Title（参考訳）: LLMテストケースによる形式仕様の検証
• Authors: Alcino Cunha, Nuno Macedo,
• Abstract要約: 本稿では,事前学習された大規模言語モデル(LLM)を用いて,自然言語要求からテストケースを生成する実験結果について報告する。 評価は最先端の GPT-5 モデルに焦点をあてるが,他のクローズドおよびオープンソース LLM の結果も報告する。
• 参考スコア（独自算出の注目度）: 1.2031796234206136
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Validation is a central activity when developing formal specifications. Similarly to coding, a possible validation technique is to define upfront test cases or scenarios that a future specification should satisfy or not. Unfortunately, specifying such test cases is burdensome and error prone, which could cause users to skip this validation task. This paper reports the results of an empirical evaluation of using pre-trained large language models (LLMs) to automate the generation of test cases from natural language requirements. In particular, we focus on test cases for structural requirements of simple domain models formalized in the Alloy specification language. Our evaluation focuses on the state-of-art GPT-5 model, but results from other closed- and open-source LLMs are also reported. The results show that, in this context, GPT-5 is already quite effective at generating positive (and negative) test cases that are syntactically correct and that satisfy (or not) the given requirement, and that can detect many wrong specifications written by humans.
• Abstract（参考訳）: 検証は、正式な仕様を開発する際の中心的な活動である。 コーディングと同様に、検証可能なテクニックは、将来の仕様が満たすべきかどうかを事前にテストケースやシナリオを定義することである。 残念なことに、このようなテストケースを指定するのは負担がかかり、エラーが発生しやすいため、ユーザはこのバリデーションタスクをスキップする可能性がある。 本稿では,事前学習された大規模言語モデル(LLM)を用いて,自然言語要求からテストケースを生成する実験結果について報告する。 特に、アロイ仕様言語で形式化された単純なドメインモデルの構造的要求に対するテストケースに焦点を当てる。 評価は最先端の GPT-5 モデルに焦点をあてるが,他のクローズドおよびオープンソース LLM の結果も報告する。 この文脈では、GPT-5は、構文的に正しい、与えられた要求を満たす(あるいは満たさない)正の(負の)テストケースを生成するのにすでに有効であり、人間によって書かれた多くの間違った仕様を検出できることを示している。

関連論文リスト

• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• AsserT5: Test Assertion Generation Using a Fine-Tuned Code Language Model [8.995812770349602]
  トレーニング済みのCodeT5モデルに基づく新しいモデルであるAsserT5を提案する。 焦点推定手法の抽象化と包含は、微調整された事前学習モデルにも有用であることがわかった。
  論文  参考訳（メタデータ） (2025-02-04T20:42:22Z)
• System Test Case Design from Requirements Specifications: Insights and Challenges of Using ChatGPT [1.9282110216621835]
  本稿では,Large Language Models (LLMs) を用いてソフトウェア要件仕様 (SRS) 文書からテストケース設計を作成することの有効性について検討する。 生成したテストケースの約87%が有効で、残りの13%は適用不可能か冗長かのどちらかでした。
  論文  参考訳（メタデータ） (2024-12-04T20:12:27Z)
• 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)
• Context-Aware Testing: A New Paradigm for Model Testing with Large Language Models [49.06068319380296]
  我々は,コンテキストを帰納バイアスとして用いて意味のあるモデル障害を探索するコンテキスト認識テスト(CAT)を導入する。 最初のCATシステムSMART Testingをインスタンス化し、大きな言語モデルを用いて、関連性があり、起こりうる失敗を仮説化します。
  論文  参考訳（メタデータ） (2024-10-31T15:06:16Z)
• GPT-HateCheck: Can LLMs Write Better Functional Tests for Hate Speech Detection? [50.53312866647302]
  HateCheckは、合成データに対してきめ細かいモデル機能をテストするスイートである。 GPT-HateCheckは,スクラッチからより多彩で現実的な機能テストを生成するフレームワークである。 クラウドソースのアノテーションは、生成されたテストケースが高品質であることを示しています。
  論文  参考訳（メタデータ） (2024-02-23T10:02:01Z)
• Self-Evaluation Improves Selective Generation in Large Language Models [54.003992911447696]
  オープンエンド生成タスクをトークンレベルの予測タスクに再構成する。 我々はLSMに答えを自己評価するように指示する。 自己評価に基づくスコアリング手法をベンチマークする。
  論文  参考訳（メタデータ） (2023-12-14T19:09:22Z)
• Automatic Generation of Test Cases based on Bug Reports: a Feasibility Study with Large Language Models [4.318319522015101]
  既存のアプローチは、単純なテスト(例えば単体テスト)や正確な仕様を必要とするテストケースを生成する。 ほとんどのテスト手順は、テストスイートを形成するために人間が書いたテストケースに依存しています。 大規模言語モデル(LLM)を活用し,バグレポートを入力として利用することにより,この生成の実現可能性を検討する。
  論文  参考訳（メタデータ） (2023-10-10T05:30:12Z)
• On the Limits of Evaluating Embodied Agent Model Generalization Using Validation Sets [101.28658250723804]
  本稿では,より広い視野を効果的に活用し,次のステップでナビゲーションや操作を行うかを選択するモジュールによるトランスフォーマーモデルの拡張実験を行う。 提案したモジュールは改良され,実際に,一般的なベンチマークデータセットであるALFREDの未確認検証セット上での最先端のパフォーマンスが向上した。 この結果は、機械学習タスクではより広い現象かもしれないが、主にテストスプリットの評価を制限するベンチマークでのみ顕著である、と我々は考えているので強調する。
  論文  参考訳（メタデータ） (2022-05-18T23:52:21Z)

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

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