論文の概要: Can Formal Specifications Be Synthesized from Tests Alone?

• arxiv url: http://arxiv.org/abs/2608.13240v1
• Date: Thu, 13 Aug 2026 13:44:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-14 18:29:38.546945
• Title: Can Formal Specifications Be Synthesized from Tests Alone?
• Title（参考訳）: 形式的な仕様はテストから完全に合成できるのか?
• Abstract要約: 提案手法では,テストコードと動的実行トレースのみから候補仕様を推測するためにLLMを用いる。 候補仕様は有界モデルチェックを用いて局所的に検証され、フィードバックは反復的改善を導く。 SpecGenBenchベンチマークの最初の結果は、テストがLLMを意味のあるJavaモデリング言語仕様へと導くことができることを示唆している。
• 参考スコア（独自算出の注目度）: 6.705404088685053
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specifications offer strong guarantees, but remain costly to write manually. Recent LLM-based approaches automate this by inferring specifications from source code, yet their reliance on white-box access poses barriers to industrial adoption due to intellectual property risks and deployment costs. Our approach uses LLMs to infer candidate specifications solely from test code and dynamic execution traces: the LLM observes only the program interface, selected inputs, and corresponding outputs or state changes, while the implementation internals remain hidden. Candidate specifications are validated locally using bounded model checking, with feedback guiding iterative refinement. Initial results on the SpecGenBench benchmark suggest that tests can guide LLMs towards meaningful Java Modeling Language specifications, while also highlighting checker compatibility and diagnostic feedback as key challenges for reliable refinement.
• Abstract（参考訳）: 正式な仕様は強力な保証を提供するが、手作業で書くのにコストがかかる。 最近のLCMベースのアプローチでは、ソースコードから仕様を推測することでこれを自動化しているが、ホワイトボックスアクセスへの依存は、知的財産のリスクとデプロイメントコストによる産業採用の障壁となる。 LLMは、プログラムインターフェース、選択された入力、および対応する出力または状態変化のみを観察し、実装内部は隠蔽されている。 候補仕様は有界モデルチェックを用いて局所的に検証され、フィードバックは反復的改善を導く。 SpecGenBenchベンチマークの最初の結果は、テストがLLMを意味のあるJavaモデリング言語仕様へと導くことができることを示唆している。

関連論文リスト

• TAG: A Lightweight Framework for Test-Driven Agentic Artifact Generation [0.30786914102688595]
  基本原理に基づく軽量なフレームワーク:textit TAGM の生成を検証する。 第一に、textbftest駆動生成: テストがフェールすると、LCMは出力が失敗した理由を明らかにする指示的エラーメッセージを受け取る。 セキュリティドメインの3つのアーティファクトタイプ - KQL生成、TAGRE ATT&CKマッピング、エンティティマッピング – に関するフレームワークをデモして、Microsoft Sentinelで本番環境にデプロイします。
  論文  参考訳（メタデータ） (2026-07-01T17:28:56Z)
• An Empirical Study of LLM-Generated Specifications for VeriFast [7.58397933941565]
  静的検証ツールは、産業規模のソフトウェアを保証できますが、仕様を書くにはかなりの人的労力が必要です。 最近の研究は、検証対象の仕様を含むコード、テスト、証明を生成するために、大きな言語モデル(LLM)を適用している。 本稿では,SL検証器 VeriFast で 303 C 関数を検証するための仕様を生成するために LLM がいかにうまく機能するかを徹底的に評価する。
  論文  参考訳（メタデータ） (2026-06-25T00:50:43Z)
• LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report [3.5867640049033054]
  本稿では,この課題に対処するための2段階のLLMベースのワークフローを,インテリジェント車両サイバーセキュリティケーススタディで紹介する。 第一段階では、AIベースのルールマイナーが自然言語要求から検証可能なルールを抽出する。 第2段階では、AIベースのコード監査者が、抽出されたルールに対する実装証拠をチェックする。
  論文  参考訳（メタデータ） (2026-05-18T06:34:03Z)
• Talk is Cheap, Logic is Hard: Benchmarking LLMs on Post-Condition Formalization [0.32665457005470505]
  本稿では,プログラムの FULL プレコンディションとポストコンディションの生成における LLM の有効性について述べる。 新たな40タスクのデータセットを用いて24種類の最先端LCMを評価した。
  論文  参考訳（メタデータ） (2026-03-17T22:46:42Z)
• Are LLMs Reliable Code Reviewers? Systematic Overcorrection in Requirement Conformance Judgement [8.059802912761919]
  我々は,大規模言語モデル(LLM)が自然言語要求にマッチするコードの体系的失敗を明らかにする。 より詳細なプロンプト設計、特に説明や修正提案を必要とするものは、より高い誤判定率をもたらす。 そこで本稿では,提案した修正を実効的証拠として扱う固定誘導検証フィルタを提案する。
  論文  参考訳（メタデータ） (2026-02-28T08:35:25Z)
• Visualizing token importance for black-box language models [48.747801442240565]
  我々は,ブラックボックスの大規模言語モデル(LLM)を監査して,本運用環境にデプロイした場合に確実に動作させるという課題を考察する。 本稿では,各入力トークンに対する言語モデルの出力の感度を評価するために,分布ベース感性分析(DBSA)を提案する。
  論文  参考訳（メタデータ） (2025-12-12T14:01:43Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。 ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。 我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。 我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• Beyond Next Token Probabilities: Learnable, Fast Detection of Hallucinations and Data Contamination on LLM Output Distributions [60.43398881149664]
  LLM出力シグナチャの効率的な符号化を訓練した軽量アテンションベースアーキテクチャであるLOS-Netを紹介する。 非常に低い検出レイテンシを維持しながら、さまざまなベンチマークやLLMで優れたパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2025-03-18T09:04:37Z)
• Migrating Existing Container Workload to Kubernetes -- LLM Based Approach and Evaluation [0.0]
  あるアプローチでは、開発者がマニフェストを生成するのを支援するために、大きな言語モデル(LLM)を採用している。 現在、出力が与えられた仕様を満たし、理解可能であるかどうかを決定することは不可能である。
  論文  参考訳（メタデータ） (2024-08-21T08:37:10Z)
• DALD: Improving Logits-based Detector without Logits from Black-box LLMs [56.234109491884126]
  大規模言語モデル(LLM)はテキスト生成に革命をもたらし、人間の文章を忠実に模倣する出力を生成する。 我々は、ブラックボックステキスト検出における最先端性能を再定義する革新的なフレームワークであるDLD(Dis Distribution-Aligned LLMs Detection)を提案する。 DALDは、サロゲートモデルの分布を未知の目標LLMの分布と整合させ、高速モデルの反復に対する検出能力とレジリエンスを向上するように設計されている。
  論文  参考訳（メタデータ） (2024-06-07T19:38:05Z)
• ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation [10.503097140635374]
  ChIRAAGはOpenAI GPT4をベースとして、設計の自然言語仕様からSystem Verilog Assertion (SVA)を生成する。 実験では、LSM生成した生のアサーションの27%に誤りがあり、数回の反復で修正された。 以上の結果から,LLMはアサーション生成プロセスにおいて技術者を合理化し,支援し,検証を再構築できることが示唆された。
  論文  参考訳（メタデータ） (2024-01-31T12:41:27Z)
• Self-Evaluation Improves Selective Generation in Large Language Models [54.003992911447696]
  オープンエンド生成タスクをトークンレベルの予測タスクに再構成する。 我々はLSMに答えを自己評価するように指示する。 自己評価に基づくスコアリング手法をベンチマークする。
  論文  参考訳（メタデータ） (2023-12-14T19:09:22Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Configuration Validation with Large Language Models [22.018488540410548]
  大きな言語モデル(LLM)は、MLベースの構成検証の長期的制限に対処する上で、有望であることを示している。 汎用的なLCMベースの構成検証フレームワークCiriを開発した。 Ciriは有効なプロンプトエンジニアリングを採用し、有効な設定データと設定ミスデータの両方に基づいて数ショットの学習を行う。
  論文  参考訳（メタデータ） (2023-10-15T00:50:27Z)

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

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