論文の概要: LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation

• arxiv url: http://arxiv.org/abs/2605.01394v1
• Date: Sat, 02 May 2026 11:31:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-05 20:33:49.748201
• Title: LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation
• Title（参考訳）: LiveFMBench: 仕様生成におけるエージェントワークフローのパワーと限界を明らかにする
• Authors: Dong Xu, Jialun Cao, Guozhao Mo, Junjie Hu, Cheng Wen, Hongyu Lin, Xianpei Han, Shengchao Qin, Cong Tian, Shing-Chi Cheung, Le Sun, Yaojie Lu,
• Abstract要約: 大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
• 参考スコア（独自算出の注目度）: 75.05397479715576
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specification is essential for rigorous program verification, yet writing correct specifications remains costly and difficult to automate. Although large language models (LLMs) and agents have shown promising progress, their true capabilities and failure modes remain unclear. We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs. We introduce LiveFMBench, a continuously evolving benchmark of 630 ACSL (ANSI/ISO C Specification Language)-annotated C programs, including 360 newly collected cases designed to mitigate data leakage. Using this benchmark, we evaluate direct prompting with different sampling sizes, reasoning-enabled (thinking mode) inference, the agentic pipeline, and perform a fine-grained failure analysis. Experimental results reveal that naive evaluation substantially overestimates performance because models under direct prompting may exhibit unfaithful behaviors, such as deceiving automated provers or ignoring code-context constraints; after excluding such cases, the true specification generation accuracy drops by approximately 20\%. We further find that both increased sampling and thinking mode significantly improve success rates, with smaller models benefiting more from thinking mode. Agentic pipelines are particularly effective under low sampling budgets and on harder datasets. Failure analysis further shows that incorrect loop invariants are the dominant error type, while agentic pipelines notably reduce assertion errors. These results expose fundamental limitations in current LLM-based approaches and suggest they remain far from replacing human-authored formal specifications. We release LiveFMBench at https://huggingface.co/datasets/fm-universe/Live-FM-Bench and all evaluation artifacts to support future research.
• Abstract（参考訳）: 形式仕様は厳密なプログラム検証には不可欠だが、正確な仕様を書くことはコストがかかり、自動化が難しい。 大きな言語モデル(LLM)とエージェントは将来的な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。 630 ACSL (ANSI/ISO C Specification Language) アノテーション付き C プログラムの継続的なベンチマークである LiveFMBench を紹介する。 このベンチマークを用いて、異なるサンプリングサイズ、推論可能な推論可能な(思考モード)推論、エージェントパイプラインを用いて直接プロンプトを評価し、きめ細かい故障解析を行う。 実験結果から,直接的プロンプト下でのモデルでは,自動プロバーの誤認やコードコンテキスト制約の無視といった不誠実な動作が生じる可能性があるため,本手法を除外すると,真の仕様生成精度が約20倍低下する可能性が示唆された。 さらに、サンプリングモードと思考モードの増加が成功率を著しく向上させ、より小さなモデルの方が思考モードの恩恵を受けることが判明した。 エージェントパイプラインは、低サンプリング予算とより厳しいデータセットで特に有効である。 フェール解析により、誤ループ不変が主流のエラータイプであり、エージェントパイプラインは特にアサーションエラーを減少させる。 これらの結果は、現在のLLMベースのアプローチにおける基本的な制限を明らかにしており、人間による正式な仕様の置き換えには程遠いことを示唆している。 私たちはLiveFMBenchをhttps://huggingface.co/datasets/fm-universe/Live-FM-Benchでリリースします。

関連論文リスト

• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。 テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。 Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
  論文  参考訳（メタデータ） (2026-03-23T14:48:54Z)
• AgentProcessBench: Diagnosing Step-Level Process Quality in Tool-Using Agents [50.481033105867205]
  我々はAgentProcessBenchを紹介した。AgentProcessBenchは、現実的なツール拡張トラジェクトリにおけるステップレベルの有効性を評価するための最初のベンチマークである。 ベンチマークは、1,000の多様な軌跡と8,509の人間ラベル付きステップアノテーションと89.1%のアノテーション間合意で構成されている。 探索をキャプチャする3つのラベリングスキームと、ラベルのあいまいさを減らすためのエラー伝搬ルールを備えている。
  論文  参考訳（メタデータ） (2026-03-15T16:13:58Z)
• MARS: Unleashing the Power of Speculative Decoding via Margin-Aware Verification [7.935725883885573]
  Speculative Decoding (SD)は、自動回帰型大言語モデル(LLM)推論をデカップリングして高速化する。 対象モデルの局所的決定性に適応する訓練不要でドメインに依存しない検証戦略であるMargin-Aware Speculative Verificationを提案する。 本手法は,目標ロジットから直接測定した決定安定性の検証を行い,厳密な検証が最小限の利益をもたらす場合にのみ拒否を緩和する。
  論文  参考訳（メタデータ） (2026-01-21T22:03:06Z)
• Stress-Testing ML Pipelines with Adversarial Data Corruption [11.91482648083998]
  規制当局は現在、ハイテイクシステムは現実的で相互依存的なエラーに耐えられるという証拠を要求している。 SAVAGEは依存性グラフとフレキシブルな汚いテンプレートを通じて、データ品質の問題を正式にモデル化するフレームワークです。 Savanageは、脆弱性のあるデータサブポピュレーションと微調整による汚職の深刻度を効率的に識別するために、双方向の最適化アプローチを採用している。
  論文  参考訳（メタデータ） (2025-06-02T00:41:24Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  より大規模なモデルではなく、推論時間の増加を活用する統合されたテスト時間計算スケーリングフレームワークを提案する。 当社のフレームワークには,内部TTCと外部TTCの2つの補完戦略が組み込まれている。 当社の textbf32B モデルは,DeepSeek R1 671B や OpenAI o1 など,はるかに大きなモデルを上回る 46% の課題解決率を実現している。
  論文  参考訳（メタデータ） (2025-03-31T07:31:32Z)

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

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