論文の概要: Are LLM-Generated Formal Specifications Faithful to Their Requirements? A Study on Bimodal Formal Specification Generation

• arxiv url: http://arxiv.org/abs/2610.32053v1
• Date: Fri, 23 Oct 2026 01:48:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-27 01:38:06.321144
• Title: Are LLM-Generated Formal Specifications Faithful to Their Requirements? A Study on Bimodal Formal Specification Generation
• Title（参考訳）: LLM生成形式仕様は要求に忠実か? : バイモーダル形式仕様生成に関する研究
• Abstract要約: LLMベースの仕様生成アプローチは、入力プログラムが正しいと仮定し、形式的検証の真の目的から逸脱する。 我々は1,403のCプログラムのベンチマークを構築し、Frama-C検証を用いてACSL仕様生成を評価する。 非形式的なHoarePromptアプローチと比較すると、LCM生成の形式仕様は要求コード一貫性の予測にはあまり効果がない。
• 参考スコア（独自算出の注目度）: 12.176192611993093
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specification generation is a critical step towards formal verification and correctness assurance of software. Recently, large language models have been widely adopted in automatic generation of formal specifications. However, existing LLM-based specification generation approaches often assume that the input program is correct, which deviates from the real purpose of formal verification---to figure out whether the program meets its requirements when its correctness is unknown. Therefore, we conduct an empirical study of LLM-based specification generation under the bimodal setting: given both the natural language requirement and its corresponding code implementation, whose correctness is unknown. We construct a benchmark of 1,403 C programs and evaluate ACSL specification generation with Frama-C verification. Our study reaches several interesting findings: first, when the code implementation is correct, providing the natural language requirement does not further improve the pass rate of generated specifications. Second, when the code implementation is incorrect, LLM-based specification generation may erroneously pass verification by producing weak or implementation-misled specifications, and this cannot be fully alleviated by advanced prompting approaches. Compared with the non-formal HoarePrompt approach, LLM-generated formal specifications are less effective in predicting requirement-code consistency. Our study takes a first look at applying LLM-based formal specification generation to verifying program correctness against requirements, and points to requirement-faithful specification generation as a new direction for future LLM-based formal specification research.
• Abstract（参考訳）: 形式的仕様生成は、ソフトウェアの形式的検証と正当性を保証するための重要なステップである。 近年,形式仕様の自動生成において,大規模言語モデルが広く採用されている。 しかし、既存のLCMベースの仕様生成手法では、入力プログラムが正しいと仮定されることが多く、これは形式的検証の真の目的から逸脱し、そのプログラムがその正しさが不明な場合にその要件を満たすかどうかを判断する。 そこで本研究では,LLMに基づく仕様生成の実証的研究を行い,自然言語要件とそれに対応するコード実装の両方を考慮し,その正確性について述べる。 我々は1,403のCプログラムのベンチマークを構築し、Frama-C検証を用いてACSL仕様生成を評価する。 まず、コード実装が正しい場合、自然言語の要求が生成した仕様のパスレートをさらに改善しない。 第二に、コード実装が正しくない場合、LCMベースの仕様生成は、弱い仕様や実装ミスの仕様を生成することによって、誤って検証をパスし、高度なプロンプトアプローチによって完全に緩和することはできない。 非形式的なHoarePromptアプローチと比較すると、LCM生成の形式仕様は要求コード一貫性の予測にはあまり効果がない。 本研究は,LCMに基づく形式仕様生成を要件に対するプログラムの正当性検証に適用すること,および今後のLCMに基づく形式仕様研究の方向性として要求に忠実な仕様生成を指摘する。

関連論文リスト

• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  我々はClarifyCodeBenchを紹介した。ClarifyCodeBenchは、要求のあいまいさを解決するためのLarge Language Modelsの機能を評価するための、インタラクティブなベンチマークだ。 ClarifyCodeBenchを用いて、6つの最先端LCMの体系的評価を行う。 1) 能力の疎結合: 強いコード生成性能は本質的には効果的な要求の明確化に変換されない; 2) 推論パラドックス: 計算思考の増大はコードの正確性を高めるが、あいまいさの識別において限界的な利益をもたらす。
  論文  参考訳（メタデータ） (2026-07-01T09:58:59Z)
• KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base [9.796586560498026]
  本稿では,多言語モデル(LLM)を形式仕様言語コーパスのデュアルソース知識で拡張するKBSpecを提案する。 その結果,KBSpec は最新の LLM ベースのアプローチよりも10-25% の検証パス率向上を実現していることがわかった。
  論文  参考訳（メタデータ） (2026-06-19T11:37:00Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。 そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。 提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
  論文  参考訳（メタデータ） (2025-04-12T15:03:00Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。 SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
  論文  参考訳（メタデータ） (2024-01-16T20:13:50Z)

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

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