論文の概要: $λ_A$: A Typed Lambda Calculus for LLM Agent Composition
- arxiv url: http://arxiv.org/abs/2604.11767v2
- Date: Tue, 14 Apr 2026 17:27:56 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-15 14:01:13.531486
- Title: $λ_A$: A Typed Lambda Calculus for LLM Agent Composition
- Title（参考訳）: λ_A$: LLMエージェント合成のための型付きラムダ計算
- Authors: Qin Liu,
- Abstract要約: エージェント合成のための計算である$_A$を提示し、単に型付けされた計算をオラクルコール、有界固定点、可変環境で拡張する。
動作意味論から構造的構成誤差を直接検出するlintツールを作成した。
LLMエージェント合成のための統一計算として、$_A$が$_A$のフラグメントを埋め込み、$_A$を確立する。
- 参考スコア（独自算出の注目度）: 2.1900658889606097
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Existing LLM agent frameworks lack formal semantics: there is no principled way to determine whether an agent configuration is well-formed or will terminate. We present $λ_A$, a typed lambda calculus for agent composition that extends the simply-typed lambda calculus with oracle calls, bounded fixpoints (the ReAct loop), probabilistic choice, and mutable environments. We prove type safety, termination of bounded fixpoints, and soundness of derived lint rules, with full Coq mechanization (1,519 lines, 42 theorems, 0 Admitted). As a practical application, we derive a lint tool that detects structural configuration errors directly from the operational semantics. An evaluation on 835 real-world GitHub agent configurations shows that 94.1% are structurally incomplete under $λ_A$, with YAML-only lint precision at 54%, rising to 96--100% under joint YAML+Python AST analysis on 175 samples. This gap quantifies, for the first time, the degree of semantic entanglement between declarative configuration and imperative code in the agent ecosystem. We further show that five mainstream paradigms (LangGraph, CrewAI, AutoGen, OpenAI SDK, Dify) embed as typed $λ_A$ fragments, establishing $λ_A$ as a unifying calculus for LLM agent composition.
- Abstract（参考訳）: 既存の LLM エージェントフレームワークには形式的な意味論が欠けている。
エージェント合成のための型付きラムダ計算である$λ_A$を提示し、単に型付けされたラムダ計算をオラクル呼び出し、境界固定点(ReActループ)、確率的選択、可変環境で拡張する。
タイプセーフ性、有界な固定点の終了、導出したリント規則の健全性を証明し、完全なCoq機械化(1,519行、42の定理、0の許容)を行う。
実用アプリケーションとして,動作意味論から直接構造的構成誤差を検出するlintツールを導出する。
835の現実世界のGitHubエージェント構成の評価によると、94.1%はλ_A$で構造的に不完全であり、YAMLのみのリント精度は54%で、175サンプルのYAML+Python AST分析で96-100%まで上昇している。
このギャップは、宣言的構成とエージェントエコシステムにおける命令的コードの間の意味的絡み合いの度合いを初めて定量化する。
さらに、LangGraph、CrewAI、AutoGen、OpenAI SDK、Difyの5つの主流パラダイムが、タイプされた$λ_A$フラグメントとして組み込み、LLMエージェント合成のための統一計算として$λ_A$を確立していることを示す。
関連論文リスト
- A Preliminary Agentic Framework for Matrix Deflation [2.6140509675507384]
本稿では,解法がランク1を更新し,いつ停止するかを決定する,行列デフレに対するエージェント的アプローチを提案する。
Digits (8times 8$), CIFAR-10 (32times32$ grayscale), 合成 (16times16$) の行列をガウス雑音と無雑音で評価した。
全ての設定において、エージェントは競合する結果を達成し、古典的な数値アルゴリズムの代替として、完全にエージェント的、しきい値のないデフレが実現可能であることを示唆している。
論文 参考訳（メタデータ） (2026-01-06T23:59:18Z) - LLM-Guided Probabilistic Fusion for Label-Efficient Document Layout Analysis [6.908972852063454]
半教師あり学習の進歩にもかかわらず、文書レイアウトの理解はデータ集約的なままである。
本稿では、視覚的予測を構造的事前に融合させることにより、半教師付き検出を強化するフレームワークを提案する。
提案手法はモデルスケール間で一貫した利得を示す。
論文 参考訳（メタデータ） (2025-11-12T02:25:58Z) - Co-Designing Quantum Codes with Transversal Diagonal Gates via Multi-Agent Systems [1.5948632947109136]
我々は、所定の対角ゲートを持つ量子符号を共設計するマルチエージェント・ヒューマン・イン・ザ・ループワークフローを提案する。
このワークフローはGPT-5を使っており、RA(https://texra.ai)-マルチエージェントリサーチアシスタントプラットフォームで実装されている。
論文 参考訳（メタデータ） (2025-10-23T16:45:39Z) - $\texttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
$texttSEM-CTRL$は、LLMデコーダに直接、リッチなコンテキスト依存制約とタスクおよびインスタンス固有のセマンティクスを強制する統一的なアプローチである。
texttSEM-CTRL$は、小さな訓練済みのLLMがより大きな変種や最先端の推論モデルよりも効率的に性能を向上することを可能にする。
論文 参考訳（メタデータ） (2025-03-03T18:33:46Z) - EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。
このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。
19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
論文 参考訳（メタデータ） (2025-02-18T02:54:25Z) - Semantic Operators: A Declarative Model for Rich, AI-based Data Processing [27.294714926492187]
我々は、宣言型および汎用AIベースの変換のための最初の定式化である意味演算子を紹介する。
セマンティックフィルタリング,ジョイン,グループバイ,トップk操作を最大1000ドルまで高速化する新しい最適化を提案する。
セマンティック・オペレーター・モデルは表現力があり、いくつかのオペレーター・コールで最先端のAIパイプラインをキャプチャする。
論文 参考訳（メタデータ） (2024-07-16T06:19:14Z) - Transfer Q Star: Principled Decoding for LLM Alignment [105.89114186982972]
Transfer $Q*$は、ベースラインモデルを通してターゲット報酬$r$の最適値関数を推定する。
提案手法は, 従来のSoTA法で観測された準最適差を著しく低減する。
論文 参考訳（メタデータ） (2024-05-30T21:36:12Z) - Refined Sample Complexity for Markov Games with Independent Linear Function Approximation [49.5660193419984]
マルコフゲーム(MG)はマルチエージェント強化学習(MARL)の重要なモデルである
本稿では、WangらによるAVLPRフレームワークを改良し(2023年)、最適部分ギャップの悲観的推定を設計する。
マルチエージェントの呪いに取り組み、最適な$O(T-1/2)収束率を達成し、同時に$textpoly(A_max)$依存性を避ける最初のアルゴリズムを与える。
論文 参考訳（メタデータ） (2024-02-11T01:51:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。