論文の概要: FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

• arxiv url: http://arxiv.org/abs/2604.11556v1
• Date: Mon, 13 Apr 2026 14:42:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-14 20:13:16.61983
• Title: FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning
• Title（参考訳）: FM-Agent:LLMベースのホアスタイル推論による大規模システムへの形式的手法のスケーリング
• Authors: Haoran Ding, Zhaoguo Wang, Haibo Chen,
• Abstract要約: 本稿では,大規模システムにおける自動構成推論を実現する最初のフレームワークであるFM-Agentについて述べる。 FM-Agentは関数の仕様を呼び出し側が関数の振る舞いを期待する方法から導いたものである。 バグの存在を確認し、バグの原因を説明するために、FM-Agentは、潜在的なバグを引き起こすテストケースを自動的に生成する。
• 参考スコア（独自算出の注目度）: 4.380970786738328
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: LLM-assisted software development has become increasingly prevalent, and can generate large-scale systems, such as compilers. It becomes crucial to strengthen the correctness of the generated code. However, automated reasoning for large-scale systems remains challenging due to code complexity. Hoare logic offers an approach to decomposing a large system into smaller components and reasoning about them separately (i.e., compositional reasoning). However, existing works still struggle to scale, because Hoare logic requires writing formal specifications for each function, imposing a heavy human burden. The problem is exacerbated when code is generated by LLMs, as developers lack a deep understanding of each function's expected behavior. This paper presents FM-Agent, the first framework that realizes automated compositional reasoning for large-scale systems. Leveraging LLMs, FM-Agent introduces a top-down paradigm to automatically generate function-level specifications. Specifically, FM-Agent derives the specification of a function from how its callers expect the function to behave, so the generated specifications can reflect the developer's intent of a function even if the implementation is buggy. Developers' intent is usually expressed in natural language, while existing verifiers only support formulas. Therefore, FM-Agent generalizes Hoare-style inference to reason about functions against natural-language specifications. Finally, to confirm bug existence and explain bug causes, FM-Agent automatically generates test cases to trigger potential bugs. In our evaluation, FM-Agent successfully reasons about large-scale systems within 2 days, each of which has up to 143k LoC. These systems have already been tested by their developers, but FM-Agent still finds 522 newly discovered bugs. These bugs can cause serious consequences, including system crashes and incorrect execution results.
• Abstract（参考訳）: LLM支援ソフトウェア開発はますます普及し、コンパイラのような大規模システムを生成することができる。 生成されたコードの正確性を強化することが重要になります。 しかし、コードの複雑さのため、大規模システムの自動推論は依然として困難である。 Hoareロジックは、大規模システムを小さなコンポーネントに分解し、それらを別々に推論するアプローチを提供する(つまり、構成的推論)。 しかし、Hoareロジックは機能ごとに正式な仕様を書く必要があり、人的負担が重いため、既存の作業はスケールに苦慮している。 開発者は各関数の期待する振る舞いを深く理解していないため、コードがLLMによって生成されると、問題は悪化する。 本稿では,大規模システムにおける自動構成推論を実現する最初のフレームワークであるFM-Agentについて述べる。 LLMを活用して、FM-Agentは関数レベルの仕様を自動的に生成するトップダウンパラダイムを導入している。 具体的には、FM-Agentは呼び出し側が関数の振る舞いを期待する方法から関数の仕様を導出する。 開発者の意図は通常自然言語で表現されるが、既存の検証は公式のみをサポートする。 したがって、FM-Agent は、自然言語仕様に対する関数を推論するために Hoare スタイルの推論を一般化する。 最後に、バグの存在を確認し、バグの原因を説明するために、FM-Agentは潜在的なバグを引き起こすテストケースを自動的に生成する。 評価において,FM-Agentは2日以内の大規模システムについて,それぞれ最大143kLOCの理由付けに成功した。 これらのシステムはすでに開発者によってテストされていますが、FM-Agentは新たに発見された522のバグを発見しています。 これらのバグは、システムのクラッシュや誤った実行結果など、深刻な結果をもたらす可能性がある。

関連論文リスト

• DoVer: Intervention-Driven Auto Debugging for LLM Multi-Agent Systems [48.971606069204825]
  DoVerは、大規模言語モデル(LLM)ベースのマルチエージェントシステムのための介入駆動デバッグフレームワークである。 ターゲットの介入を通じて、アクティブな検証によって仮説生成を増強する。 DoVerは失敗試験の18～28%を成功させ、最大16%のマイルストーンを達成し、失敗仮説の30～60%を検証または否定する。
  論文  参考訳（メタデータ） (2025-12-07T09:23:48Z)
• Where LLM Agents Fail and How They can Learn From Failures [62.196870049524364]
  大規模言語モデル(LLM)エージェントは、複雑なマルチステップタスクの解決において有望であることを示す。 単一ルート原因エラーがその後の決定を通じて伝播する、障害のカスケードに対する脆弱性を増幅する。 現在のシステムは、モジュール的で体系的な方法でエージェントエラーを包括的に理解できるフレームワークを欠いている。 AgentErrorTaxonomyは、メモリ、リフレクション、計画、アクション、システムレベルの操作にまたがる障害モードのモジュール分類である。
  論文  参考訳（メタデータ） (2025-09-29T18:20:27Z)
• Which Agent Causes Task Failures and When? On Automated Failure Attribution of LLM Multi-Agent Systems [50.29939179830491]
  LLMマルチエージェントシステムにおける障害帰属は、まだ調査が過小評価されており、労働集約的である。 本稿では,3つの自動故障帰属手法の開発と評価を行い,その欠点と欠点を要約する。 最良の方法は、障害に応答するエージェントを特定する際に53.5%の精度を達成するが、故障の特定には14.2%しか役に立たない。
  論文  参考訳（メタデータ） (2025-04-30T23:09:44Z)
• AEGIS: An Agent-based Framework for General Bug Reproduction from Issue Descriptions [10.686849324750556]
  gEneral buG reproductIon Scripts 生成フレームワークは AEGIS という名称で、タスクのための最初のエージェントベースのフレームワークである。 AEGISは、Agentlessの相対的な解決率を12.5%向上させることができる。
  論文  参考訳（メタデータ） (2024-11-27T03:16:47Z)
• A Unified Debugging Approach via LLM-Based Multi-Agent Synergy [39.11825182386288]
  FixAgentはマルチエージェントのシナジーによる統合デバッグのためのエンドツーエンドフレームワークである。 1.25$times$ 2.56$times$レポレベルのベンチマークであるDefects4Jのバグを修正した。
  論文  参考訳（メタデータ） (2024-04-26T04:55:35Z)
• AgentFL: Scaling LLM-based Fault Localization to Project-Level Context [11.147750199280813]
  本稿では,ChatGPTに基づくマルチエージェントシステムであるAgentFLについて述べる。 人間の開発者の振る舞いをシミュレートすることで、AgentFLはFLタスクを3段階のプロセスとしてモデル化する。 広く使用されているDefects4J-V1.2.0ベンチマークの評価は、AgentFLがTop-1内の395のバグのうち157をローカライズできることを示している。
  論文  参考訳（メタデータ） (2024-03-25T01:58:19Z)
• ML-Bench: Evaluating Large Language Models and Agents for Machine Learning Tasks on Repository-Level Code [76.84199699772903]
  ML-Benchは、既存のコードリポジトリを利用してタスクを実行する現実世界のプログラミングアプリケーションに根ざしたベンチマークである。 LLM(Large Language Model)とAIエージェントの両方を評価するために、事前に定義されたデプロイメント環境でLLMのテキスト-コード変換を評価するML-LLM-Benchと、Linuxサンドボックス環境でエンドツーエンドのタスク実行で自律エージェントをテストするML-Agent-Benchの2つの設定が採用されている。
  論文  参考訳（メタデータ） (2023-11-16T12:03:21Z)

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

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