論文の概要: MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs

• arxiv url: http://arxiv.org/abs/2609.19391v1
• Date: Wed, 16 Sep 2026 20:15:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-20 08:55:53.996899
• Title: MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs
• Title（参考訳）: MAGS:マルチエージェントのオートフォーマル化は、エージェントアウトプットの安全性を保証
• Abstract要約: ファズテスト、静的解析、LSM-as-a-Verifierといった一般的なアプローチは、多くの障害を検出するが、可能なすべてのエッジケースをカバーするのに苦労する。 我々は,Dafnyを検証対応中間表現として使用して,形式的な安全性保証を備えたプログラムを生成する,統一型マルチエージェントフレームワークMAGSを導入する。 220のすべての例において、フリーズ仕様に対して非自明な安全性を保証するプログラムを制作する上で、100%の成功率を達成する。
• 参考スコア（独自算出の注目度）: 20.71357320455618
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: LLM coding agents now generate complex programs at a scale that makes thorough human review increasingly difficult, raising the risk of safety and security failures. Common approaches, including fuzz testing, static analysis, and LLM-as-a-Verifier, can detect many failures but struggle to cover all possible edge cases. Formal verification addresses this by providing machine-checkable guarantees over specified properties, but traditionally demands substantial manual specification and proof engineering. We introduce a unified multi-agent framework, MAGS, that generates executable programs with formal safety guarantees, using Dafny as a verification-aware intermediate representation where safety properties can be mechanically checked. MAGS formalizes and freezes human-audited APIs and safety requirements, translates generated code into Dafny, repairs violations using verifier feedback, and compiles verified programs back into executable code. We evaluate MAGS on 100 CUDA kernels, 100 terminal scripts, and 20 robotic-arm tasks. Across all 220 examples, it achieves a 100% success rate in producing programs with non-trivial safety guarantees against frozen specifications. Independent safety and functional evaluations further show strong performance across all three domains, while revealing failures when the auto-formalized semantics do not fully capture the target behavior.
• Abstract（参考訳）: LLMコーディングエージェントは、人間の徹底的なレビューをますます困難にし、安全性とセキュリティの失敗のリスクを増大させるような、複雑なプログラムをスケールで生成する。 ファズテスト、静的解析、LSM-as-a-Verifierといった一般的なアプローチは、多くの障害を検出するが、可能なすべてのエッジケースをカバーするのに苦労する。 形式的検証は、指定されたプロパティに対してマシンチェック可能な保証を提供することによってこの問題に対処するが、伝統的に手動の仕様と証明工学を必要とする。 本稿では,安全性を機械的に確認可能な検証対応中間表現としてDafnyを用いて,形式的安全性保証を備えた実行可能プログラムを生成する,統一型マルチエージェントフレームワークMAGSを提案する。 MAGSは、人間監査されたAPIと安全要件を形式化し凍結し、生成されたコードをDafnyに翻訳し、検証者フィードバックを使用して違反を修正し、検証済みプログラムを実行可能なコードにコンパイルする。 我々は,100個のCUDAカーネル,100個の端末スクリプト,20個のロボットアームタスク上でMAGSを評価した。 220のすべての例において、フリーズ仕様に対して非自明な安全性を保証するプログラムを制作する上で、100%の成功率を達成する。 独立した安全性と機能評価は、3つのドメインすべてに対して強いパフォーマンスを示す一方で、自動形式化されたセマンティクスがターゲットの動作を完全にキャプチャしていない場合の障害を明らかにする。

関連論文リスト

• AgentLens: Interpretable Safety Steering via Mechanistic Subspaces for Multi-Turn Coding Agent [53.82005364479556]
  大規模言語モデル(LLM)に基づく符号化エージェントは、驚くべき自律性を示す。 既存の安全機構は主に外部ガードレールに依存している。 我々は,ランタイムの安全性検出と表現レベルの緩和を行う,ホワイトボックスの防御フレームワークであるAgentLensを提案する。
  論文  参考訳（メタデータ） (2026-06-21T21:13:55Z)
• Detecting and Understanding Vulnerabilities in Fully Homomorphic Encryption Frameworks [14.240598788040051]
  ホモモルフィック暗号化(英語版) (FHE) は、復号化せずに直接暗号化されたデータ上で計算を行うことを可能にする。 ハイレベルなFHEプログラムを複雑なFHE操作に変換するために、新しい世代の特殊フレームワークが登場した。 HERTAは、FHEフレームワーク用に調整された最初の自動テストツールである。
  論文  参考訳（メタデータ） (2026-06-21T14:18:49Z)
• SeClaw: Spec-Driven Security Task Synthesis for Evaluating Autonomous Agents [87.26967184869198]
  SeClawは、仕様駆動のセキュリティタスク合成と、自律エージェントの実行ベースのセキュリティ評価を組み合わせたフレームワークである。 ベンチマークは、リソース、ユーザタスク、環境、本質的なエージェントの振る舞いから生じるリスクをカバーしている。
  論文  参考訳（メタデータ） (2026-06-01T14:23:42Z)
• On-Policy Self-Evolution via Failure Trajectories for Agentic Safety Alignment [54.30690671490447]
  既存の安全アライメント信号は、主に応答レベルまたは政治外である。 FATEは、検証済みの失敗を専門家のデモンストレーションなしで修復管理に変換する。 FATEは攻撃成功率を33.5%、有害なコンプライアンスを82.6%削減し、外的軌道安全診断を6.5%改善する。
  論文  参考訳（メタデータ） (2026-05-12T09:56:28Z)
• AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification [10.258883626292265]
  メモリセーフティエラーは、低レベルソフトウェアにおけるゼロデイ脆弱性の永続的な原因である。 現在の検証はほとんど手作業で行われており、専門的な専門知識が必要である。 本稿では,コンポーネントレベルのメモリ安全性検証を自動化するシステムであるAutoSOUPを提案する。
  論文  参考訳（メタデータ） (2026-05-11T15:23:26Z)
• SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
  RLM(Reasoning Language Model)は、プログラミングにおいてますます使われている言語モデルである。 しかし、最先端のRLMでさえ、生成されたコードに重大なセキュリティ脆弱性を頻繁に導入する。 我々は、構造化されたセキュリティ推論を内部化するためのRTMを教える微調整パイプラインであるSecPIを提案する。
  論文  参考訳（メタデータ） (2026-04-04T04:29:11Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。 我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
  論文  参考訳（メタデータ） (2026-01-30T08:29:01Z)
• Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
  大規模言語モデル(LLM)ベースのAIエージェントは、データソース、API、検索エンジン、コードサンドボックス、さらにはその他のエージェントなどのツールへのアクセスを可能にすることで、機能を拡張する。 LLMは意図しないツールインタラクションを起動し、機密データを漏洩したり、クリティカルレコードを上書きしたりするリスクを発生させる。 モデルベースセーフガードのようなリスクを軽減するための現在のアプローチは、エージェントの信頼性を高めるが、システムの安全性を保証することはできない。
  論文  参考訳（メタデータ） (2026-01-12T21:31:38Z)
• AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents [8.290987399121343]
  LLMエージェントのランタイム制約を指定・強制するための軽量言語であるAgentSpecを提案する。 AgentSpecでは、トリガー、述語、執行機構を含む構造化ルールを定義する。 コード実行、エンボディエージェント、自律運転など、複数のドメインにまたがるAgentSpecを実装しています。
  論文  参考訳（メタデータ） (2025-03-24T13:31:48Z)

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

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