論文の概要: LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents

• arxiv url: http://arxiv.org/abs/2611.02332v1
• Date: Mon, 02 Nov 2026 00:26:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-11-04 23:36:30.547098
• Title: LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents
• Title（参考訳）: LEANGUARD: ツール使用エージェントのためのリーン検証ガードレール
• Abstract要約: LeanGuardは、呼び出しが環境に到達する前にLean4で書かれたポリシーに対して提案されたすべてのツールコールをチェックする。 フィードバックにより、エージェントは違反したルールとヒントを受け取る。 証明誘導による修復により、リーンプログラミングはユーザの意図を守り、ポリシーがそれを認めることを証明する、近くの呼び出しを検索する。
• 参考スコア（独自算出の注目度）: 40.01021473111788
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Tool-using language-model agents often execute actions that their domain policies forbid. We present LeanGuard, a runtime that checks every proposed tool call against a policy written in Lean4 before the call reaches the environment. Policies combine state predicates with scoped past-time temporal operators over the execution history, evaluation is fail-closed, and the decision procedure is proved equivalent to a LeanLTL semantics. A denied call can be corrected in two ways. With feedback, the agent receives the violated rule and a hint; with proof-guided repair, Lean metaprogramming searches for a nearby call that preserves the user's intent and proves that the policy admits it, without the model. On Tau-Bench with five Qwen models (0.8B-27B), unguarded agents execute at least 33 calls that the Lean policy forbids, while LeanGuard executes none; with feedback, task success does not change significantly. On DTap, LeanGuard reduces direct prompt-injection success from 57.9% to 5.9%, and in telecom, where benign tasks need no writes, benign success is unchanged. Feedback reduces repeated blocked calls and raises task success for four of five models over a bare denial. On replayed denials, repair proves an admissible edit for 88 of 252 denials caused by argument values, in a median of 2,ms.
• Abstract（参考訳）: ツールを使用する言語モデルエージェントは、ドメインポリシーが禁止しているアクションを実行することが多い。 コールが環境に到達する前に、Lean4で書かれたポリシーに対して提案されたすべてのツールコールをチェックするランタイムであるLeanGuardを紹介します。 ポリシーは、状態述語と実行履歴のスコープ化された過去の時間演算子を組み合わせ、評価はフェールクロースされ、決定手順はLeanLTLセマンティクスと等価であることが証明される。 拒否された呼び出しは2つの方法で修正できる。 フィードバックにより、エージェントは違反したルールとヒントを受け取り、証明誘導された修復により、リーンはユーザの意図を守り、モデルなしでポリシーがそれを認めることを証明する近くの呼び出しをメタプログラミングする。 5つのQwenモデル(0.8B-27B)を持つTau-Benchでは、守られていないエージェントが少なくとも33の呼び出しを実行し、LeanGuardは一切実行しない。 DTapでは、LeanGuardは直接のインジェクション成功を57.9%から5.9%に削減する。 フィードバックは繰り返しブロックされた呼び出しを減らし、素の否定に対して5つのモデルのうち4つのタスクの成功を高める。 リプレイされた否定について、修復は、引数値による252の否定のうち88の許容可能な編集を、中央値2,msで証明する。

関連論文リスト

• Knowing When to Stop: The Evidence-Action Gap in Coding Agents [76.92446812179517]
  コーディングエージェントはタスクを完了させるために訓練され、環境が完了を不可能にしている場合でも試し続けます。 ImpasseBenchを導入し、12の環境ブロッカーを他の方法で解決可能な修理タスクに注入する。 外部に必要なほぼすべての実行が十分な証拠を集めているのに、3分の1は予算を使い果たしている。
  論文  参考訳（メタデータ） (2026-10-22T20:45:47Z)
• Behavior Beyond Text: Evaluating Refusal Transfer Failure in LLM Agents [0.0]
  テキスト転送における拒絶行動がツール利用に影響を及ぼすかどうかを検討する。 さまざまなサイズと家族の5つのモデルをテストします。 要求をテキストで拒否すると、安全でないツールコールが発生することがよくあります。
  論文  参考訳（メタデータ） (2026-10-20T23:14:30Z)
• From Approval to Abuse: Privilege Escalation Attacks on Harness-Protected Coding Agents [71.95900681890676]
  コーディングエージェントは、実行ハーネスを使用して、パーミッション境界を強制することによって、プロンプトインジェクションの結果を制限する。 承認疲労を軽減するために、ユーザはエージェントが提案する許可ルールを承認し、その後、ルールにマッチする将来のアクションをプロンプトなしで許可する。 信頼できないコンテキストは、承認のために提示された許可に影響を与える可能性がある。
  論文  参考訳（メタデータ） (2026-10-16T06:13:06Z)
• ReDraft, Don't Just Distill: Reference-Driven Revision for Continual VLLM Post-Training [66.72708893922605]
  大規模なマルチモーダルモデルのポストトレーニングは、事前トレーニングから保護しながら、新しい機能を追加する必要がある。 SFTは、タスクをほぼゼロの精度から学習する明確なターゲット監視を提供するが、そのオフポリティックターゲットはモデルを十分に移動させ、忘れる原因となる。 モデル自身の失敗から両方を得るReDraftを紹介します。
  論文  参考訳（メタデータ） (2026-09-15T04:59:03Z)
• If Agents Were Angels, No Governance Would Be Necessary: Out-of-Band Policy Enforcement at a Trusted Tool Boundary [0.07499722271664146]
  Out-of-Band Policy Enforcement (OBPE)は、エージェント推論以外の信頼できる境界である。 OBPEは型付き操作とリソースを許可し、バックエンド呼び出しの前にクエリを絞り込み、それからレコードとフィールドをフィルタリングし、レスポンスの値にマスクを付ける。
  論文  参考訳（メタデータ） (2026-08-27T19:35:48Z)
• ROPE: Routed Origin Policy Enforcement against Indirect Prompt Injection [61.4148196085256]
  本稿では,信頼という構造概念に根ざしたROPE(Routed Origin Policy Enforcement)について述べる。 提案手法では,(1)軌道の各段階において,攻撃可能コンテンツのみを起点とする値が,原点保護パラメータに到達しない,(2)注入のリワードがない,という2つの保証が認められている。
  論文  参考訳（メタデータ） (2026-08-27T01:22:14Z)
• ClawSentry: A Progressive Multi-Tier Security Monitor for Safeguarding Autonomous LLM Agents [24.540638169054812]
  悪意のあるサードパーティのスキルにハイジャックされた単一のエージェントは、データの流出、特権のエスカレーション、カスケード妥協を引き起こす可能性がある。 我々は、エージェントランタイムのためのオープンソースのフレームワークに依存しないセキュリティ監視ゲートウェイであるClawSentryを紹介する。
  論文  参考訳（メタデータ） (2026-08-21T13:47:51Z)
• Reason Less, Verify More: Deterministic Gates Recover a Silent Policy-Violation Failure Mode in Tool-Using LLM Agents [1.6567880228735357]
  ポリシーを許容する環境では、対応する状態遷移がドメインポリシーによって禁じられている場合であっても、ツールはよくできた呼び出しを実行できる。 我々は、この障害モードを2ドルの航空会社ドメインで研究する。 我々は、決定論的かつリードオンリーの事前実行ゲートという、軽量な介入を評価する。
  論文  参考訳（メタデータ） (2026-07-08T13:38:54Z)

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

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