論文の概要: LM2Alloy: Investigating LLM-Generated Formal Specifications for Automated Test Derivation in Production Software
- arxiv url: http://arxiv.org/abs/2607.18555v1
- Date: Mon, 20 Jul 2026 22:41:55 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-22 19:05:05.261316
- Title: LM2Alloy: Investigating LLM-Generated Formal Specifications for Automated Test Derivation in Production Software
- Title（参考訳）: LM2Alloy:生産ソフトウェアにおける自動テスト導出のためのLCM生成形式仕様の検討
- Abstract要約: 本稿では,Large Language Models (LLMs) を用いた合金仕様作成のための探索的研究について述べる。
Flipperは機能フラグ管理システムであり、Cerberusはデータ検証ライブラリである。
- 参考スコア（独自算出の注目度）: 0.9023847175654603
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present an exploratory study on using Large Language Models (LLMs) to generate Alloy formal specifications from both requirements documentation and production source code, and to derive executable test cases from those specifications. We evaluate on two real open-source Python libraries: Flipper, a feature flag management system, and Cerberus, a data validation library. In both cases, the LLM produced workable Alloy specifications and executable tests without any manual correction. For Flipper, our pipeline uncovered a genuine bug that the existing test suite had missed: the library silently accepts duplicate flag names, directly contradicting its documented uniqueness requirement. A direct LLM baseline--generating tests from the same README but skipping the Alloy step--achieved 68% branch coverage yet failed to catch this bug across all three independent runs. This suggests that introducing a formal intermediate representation can surface constraint-level defects that coverage-oriented generation may miss. For Cerberus, the code-derived specification captured an implicit abstraction over sized types that the documentation-derived spec omitted, producing two additional tests. Across both libraries, code-based specifications showed lower variance in test generation (mean SD = 2.15) than documentation-based ones (mean SD = 5.0), though whether this generalises remains an open question. Index Terms--formal specifications, Alloy, large language models, automated testing, specification drift, software validation.
- Abstract（参考訳）: 本稿では,Large Language Models (LLMs) を用いて,要件文書と実運用ソースコードの両方からアロイ形式仕様を生成し,それらの仕様から実行可能なテストケースを導出する探索的研究を行う。
Flipperは機能フラグ管理システムであり、Cerberusはデータ検証ライブラリである。
どちらの場合も、LLMは手動で修正することなく実用可能な合金仕様と実行可能な試験を作成した。
Flipper氏にとって、私たちのパイプラインは、既存のテストスイートが見逃していた真のバグを発見しました。
同じREADMEから直接LCMのベースライン生成テストが行われたが、アロイのステップをスキップして68%のブランチカバレッジを達成したが、3つの独立したランでこのバグをキャッチできなかった。
このことは、形式的な中間表現を導入することは、カバレッジ指向生成が見逃す可能性のある制約レベルの欠陥を表面化する可能性があることを示唆している。
Cerberus氏にとって、コード由来の仕様は、ドキュメント由来の仕様が省略したサイズの型に対する暗黙の抽象化をキャプチャし、2つの追加テストを生成した。
どちらのライブラリでも、コードベースの仕様は、ドキュメントベースの仕様よりもテスト生成のばらつき(平均SD = 2.15)が低い(平均SD = 5.0)。
インデックス用語--形式仕様、アロイ、大きな言語モデル、自動テスト、仕様のドリフト、ソフトウェア検証。
関連論文リスト
- IntentTester: Intent-Driven Multi-agent Framework for Cross-Library Test Migration [14.0813614333238]
IntentTesterは意図駆動テストの再利用のためのフレームワークです。
IntentTesterは3つのドメイン(JSON、HTML、Time)と2つの言語(JavaとPython)にわたる9つのオープンソースプロジェクトで評価します。
論文 参考訳（メタデータ） (2026-06-24T08:59:01Z) - AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications [7.797719198801956]
本稿では,ハードウェア検証における現実的なアサーション生成のためのオープンソースのベンチマークであるAssertLLM2を紹介する。
AssertLLM2には13の機能カテゴリにわたる83の現実世界の設計が含まれている。
それぞれの設計について、このベンチマークは構造化された設計仕様、検証済みの依存性完全ゴールデンRTL、系統的に変更されたバグギーRTLの亜種を提供する。
論文 参考訳（メタデータ） (2026-05-26T10:49:25Z) - CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
本稿では,実行ベース評価プロトコルの下で実行可能な動作仕様生成のためのベンチマークであるCodeSpecBenchを紹介する。
CodeSpecBenchは関数レベルとリポジトリレベルのタスクの両方をサポートし、仕様を実行可能なPython関数としてエンコードする。
リポジトリレベルのタスクでは、最高のモデルが20.2%のパス率しか達成できないため、パフォーマンスが大幅に低下するのを観察します。
論文 参考訳（メタデータ） (2026-04-14T04:31:45Z) - GPT-4.1 Sets the Standard in Automated Experiment Design Using Novel Python Libraries [0.649540541957527]
大規模言語モデル(LLM)は、科学研究におけるコード生成を自動化するツールとして急速に進歩してきた。
本研究では,関数型Pythonコードを生成する上で,最先端のLLMの選択を体系的にベンチマークする。
結果は、モデルの小さなサブセットだけが一貫して正しい実行可能なコードを生成することを示している。
論文 参考訳（メタデータ） (2025-07-30T13:11:29Z) - IFEvalCode: Controlled Code Generation [69.28317223249358]
本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。
IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
論文 参考訳（メタデータ） (2025-07-30T08:08:48Z) - CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
$rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。
それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
論文 参考訳（メタデータ） (2025-05-20T05:15:47Z) - METAMON: Finding Inconsistencies between Program Documentation and Behavior using Metamorphic LLM Queries [10.9334354663311]
本稿では,既存の検索ベーステスト生成技術を用いて,現在のプログラム動作をテストケース形式でキャプチャするMETAMONを提案する。
MeTAMONはこのタスクでメタモルフィックテストと自己整合性によってサポートされている。
Defects4J v2.0.1の5つのオープンソースプロジェクトを使って生成された9,482対のコードドキュメンテーションとコードスニペットに対する実証的な評価は、METAMONがコードとドキュメントの不整合を精度0.72、リコール0.48で分類できることを示している。
論文 参考訳（メタデータ） (2025-02-05T00:42:50Z) - DiffSpec: Differential Testing with LLMs using Natural Language Specifications and Code Artifacts [7.019166148885954]
本稿では,プロンプト連鎖を用いた差分テストを生成するフレームワークであるDiffSpecを紹介する。
DiffSpecの2つの異なる(大規模にテストされた)システム、eBPFランタイム、Wasmバリデータに対する有効性を示す。
論文 参考訳（メタデータ） (2024-10-05T18:11:14Z) - GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [64.95492752484171]
GenAudit - 文書基底タスクの事実チェック LLM 応答を支援するためのツール。
GenAuditは、レファレンス文書でサポートされていないクレームを修正したり削除したりすることでLCMレスポンスを編集することを提案し、また、サポートしているように見える事実の参照から証拠を提示する。
GenAuditは、さまざまなドメインから文書を要約する際に、8つの異なるLCM出力でエラーを検出することができる。
論文 参考訳（メタデータ） (2024-02-19T21:45:55Z) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳（メタデータ） (2023-11-15T14:41:57Z) - Knowledge-Augmented Language Model Verification [68.6099592486075]
最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。
本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。
その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
論文 参考訳（メタデータ） (2023-10-19T15:40:00Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。