論文の概要: Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
- arxiv url: http://arxiv.org/abs/2606.06523v1
- Date: Tue, 02 Jun 2026 18:46:50 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-08 14:33:29.340041
- Title: Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
- Title（参考訳）: Lean4Agent: エージェントワークフローと軌道の形式的モデリングと検証
- Abstract要約: 信頼性の高いマルチステップを実行するためのLLM(Large Language Models)の取得は、人工知能における中心的な課題となっている。
この課題は、自然言語の曖昧さ(NL)が形式言語(FL)の発展を動機付けている数学における長年の問題を反映している。
エージェントの振る舞いをモデル化し検証するための依存型FLであるLean4を使用した最初のフレームワークである**Lean4Agent*を提案する。
- 参考スコア（独自算出の注目度）: 17.95201244576703
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Equipping Large Language Models (LLMs) to execute reliable multi-step workflows has become a central challenge in artificial intelligence. Despite recent advances in LLMs' agentic capabilities, most agent systems still lack formal methods for specifying, verifying, and debugging their workflow and execution trajectories. This challenge mirrors a long-standing problem in mathematics, where the ambiguity of natural languages (NLs) motivates the development of formal languages (FLs). Inspired by this paradigm, we propose **Lean4Agent**, to the best of our knowledge, the first framework that uses Lean4, a dependent-type FL to model and verify agent behavior. **Lean4Agent** launches **FormalAgentLib**, an extensible Lean4 library for formally modeling and verifying agent workflows' semantic consistency under explicit assumptions, and enabling localization of execution-time failures revealed by trajectories. Building on **FormalAgentLib**, we further develop **LeanEvolve**, which applies results in **FormalAgentLib** to revise workflows to enhance its capability. Extensive experiments on a hard problem subset of SWE-Bench-Verified and a subset of ELAIP-Bench across 5 leading LLMs indicate that the verification-passing workflows outperform the failing ones by an average of **11.94%**, and **LeanEvolve** further improves SWE performance by **7.47%** on average. Furthermore, **Lean4Agent** establishes a foundation for a new field of using expressive dependent-type FL to formally model and verify agent behavior.
- Abstract（参考訳）: 信頼性の高い多段階ワークフローを実行するためのLLM(Large Language Models)の取得は、人工知能における中心的な課題となっている。
LLMのエージェント能力の最近の進歩にもかかわらず、ほとんどのエージェントシステムは、ワークフローと実行軌跡を指定、検証、デバッグするための正式なメソッドを欠いている。
この課題は、自然言語の曖昧さ(NL)が形式言語(FL)の発展を動機付けている数学における長年の問題を反映している。
エージェントの振る舞いをモデル化し検証するための依存型FLであるLean4を使用した最初のフレームワークである。
これは、明示的な仮定の下でエージェントワークフローのセマンティックな一貫性を正式にモデル化し、検証し、トラジェクトリによって明らかにされる実行時障害のローカライズを可能にする拡張可能なLean4ライブラリである。
ここでは、**FormalAgentLib* に基づいて、**LeanEvolve** をさらに開発し、**FormalAgentLib* で結果を適用して、ワークフローを改訂し、その機能を強化します。
SWE-Bench-Verified のハード問題部分集合と5つの主要な LLM にまたがる ELAIP-Bench の部分集合に関する広範な実験により、検証パスワークフローは、平均**11.94%** と***LeanEvolve** は、平均***7.47%* でSWE性能をさらに向上することを示している。
さらに、**Lean4Agent**は、表現依存型FLを使用してエージェントの振る舞いを正式にモデル化し検証する新しい分野の基礎を確立する。
関連論文リスト
- A Phased Workflow for Operating LLM-Based Coding Agents [0.7874708385247353]
InfobipのAI研究チームが開発したコーディングエージェントを操作するための段階的ワークフローについて報告する。
コンテキスト管理は、既知の障害モードに対応するために各フェーズで適用される4つの戦略を通じて対処される、中心的な関心事である。
ワークフローの有効性のためのメトリクスの欠如と、形式化されたコンテキスト管理コンポーネントと実践者が必要とするワークフローレベルのパターンのギャップです。
論文 参考訳（メタデータ） (2026-08-31T12:39:26Z) - AgentArk: Distilling Multi-Agent Intelligence into a Single LLM Agent [57.10083973844841]
AgentArkは、マルチエージェントダイナミクスを単一のモデルの重みに蒸留する新しいフレームワークである。
各種モデル,タスク,スケーリング,シナリオの3つの階層的蒸留戦略について検討する。
シミュレーションからトレーニングへ計算の負担をシフトさせることで、蒸留されたモデルは、複数のエージェントの強い推論と自己補正性能を示しながら、一つのエージェントの効率を保ちます。
論文 参考訳（メタデータ） (2026-02-03T19:18:28Z) - R&D-Agent: An LLM-Agent Framework Towards Autonomous Data Science [70.1638335489284]
高レベルの機械学習エンジニアリングタスクは、労働集約的で反復的である。
機械学習プロセスを形式化する包括的で分離されたフレームワークであるR&D-Agentを紹介します。
R&D-AgentはMLEを2つのフェーズと6つのコンポーネントに定義し、MLEのエージェント設計を原則としてテスト可能なプロセスに変える。
論文 参考訳（メタデータ） (2025-05-20T06:07:00Z) - FlowAgent: Achieving Compliance and Flexibility for Workflow Agents [31.088578094151178]
FlowAgentは、コンプライアンスと柔軟性の両方を維持するように設計された新しいエージェントフレームワークである。
PDL を基盤として,OOW クエリを効果的に管理する LLM を支援する包括的フレームワークを開発した。
本稿では,LLMエージェントのOOWシナリオ処理能力を評価するための新しい評価手法を提案する。
論文 参考訳（メタデータ） (2025-02-20T07:59:31Z) - Large Language Model Agent for Fake News Detection [33.06422916067896]
FactAgentは、偽ニュースの検出に大規模な言語モデルを利用するためのエージェント的アプローチである。
モデルトレーニングなしでニュースクレームを検証する際に、人間の専門家の振る舞いをエミュレートする。
エンドユーザーに偽ニュース検出の推論プロセスに関する洞察を提供する。
論文 参考訳（メタデータ） (2024-04-30T06:55:27Z) - Enhancing the General Agent Capabilities of Low-Parameter LLMs through Tuning and Multi-Branch Reasoning [56.82041895921434]
オープンソースの事前訓練された大規模言語モデル(LLM)は、強力な言語理解と生成能力を示す。
現実世界の複雑な問題に対処するエージェントとして使用される場合、ChatGPTやGPT-4のような大型の商用モデルに比べてパフォーマンスははるかに劣る。
論文 参考訳（メタデータ） (2024-03-29T03:48:12Z) - Agent-FLAN: Designing Data and Methods of Effective Agent Tuning for Large Language Models [56.00992369295851]
オープンソースのLarge Language Models(LLM)は、さまざまなNLPタスクで大きな成功を収めていますが、エージェントとして振る舞う場合、それでもAPIベースのモデルよりもはるかに劣っています。
本稿では,(1) エージェント学習コーパスを,(1) エージェント学習データの分布から大きくシフトするエージェント推論と,(2) エージェントタスクが必要とする能力に異なる学習速度を示すエージェント学習コーパスと,(3) 幻覚を導入することでエージェント能力を改善する際の副作用について述べる。
本稿では,エージェントのためのFLANモデルを効果的に構築するためのエージェントFLANを提案する。
論文 参考訳（メタデータ） (2024-03-19T16:26:10Z) - DS-Agent: Automated Data Science by Empowering Large Language Models with Case-Based Reasoning [56.887047551101574]
大規模言語モデル(LLM)エージェントとケースベース推論(CBR)を利用した新しいフレームワークであるDS-Agentを提案する。
開発段階では、DS-AgentはCBRフレームワークに従い、自動イテレーションパイプラインを構築する。
デプロイメントの段階では、DS-Agentは、シンプルなCBRパラダイムで低リソースのデプロイメントステージを実装し、LCMの基本能力に対する需要を大幅に削減する。
論文 参考訳（メタデータ） (2024-02-27T12:26:07Z) - AgentBench: Evaluating LLMs as Agents [99.12825098528212]
エージェントとしてのLarge Language Model (LLM)は近年広く認知されている。
我々は,LLM-as-Agentの推論と意思決定能力を評価するために,8つの異なる環境からなるベンチマークであるAgentBenchを提案する。
論文 参考訳（メタデータ） (2023-08-07T16:08:11Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。