Semia：制約ガイド付き表現合成によるエージェントスキルの監査

要旨: エージェントのスキルとは、LLM駆動エージェントに、メールの読み取り、シェルコマンドの実行、ブロックチェーン取引への署名などの具体的な能力を備えさせるための設定パッケージである。各スキルはハイブリッドな成果物であり、構造化された前半は実行可能なインターフェースを宣言し、後半の散文はそれらのインターフェースがいつ、どのように発火するかを規定する。そしてこの散文は、呼び出しのたびに確率論的に再解釈される。従来の静的アナライザは構造化された前半を解析するが散文は無視する。一方でLLMベースのツールは散文を読み取れるものの、汚染された入力が高い影響を持つシンクに到達することを、再現可能に証明できない。
本稿では、エージェントスキルの静的監査器であるSemiaを提案する。Semiaは各スキルを、Skill Description Language（SDL）へ持ち上げる。SDLはDatalogの事実ベースであり、LLMが引き起こすアクション、散文で定義された条件、人間が介在するチェックポイントを捉える。構造的に健全で、かつ元の散文に対して意味論的に忠実な事実ベースを合成することが中核となる課題であり、収束するまでLLM候補を改良する提案-検証-評価のループであるConstraint-Guided Representation Synthesis（CGRS）によりこれに対処する。エージェントスキルに関するセキュリティ特性（例: 間接的なインジェクション、秘密情報の漏えい、コンフューズド・デプティ、不適切に防護されていないシンクなど）は、Datalog到達可能性クエリに還元できる。Semiaを、公的なマーケットプレイスから得た実世界のスキル13,728件で評価する。Semiaはそれらすべてを監査可能にし、半数を超えるスキルが少なくとも1つの重大な意味論的リスクを含むことを見出す。専門家がラベル付けした541件の階層化サンプルにおいて、Semiaは97.7%のリコールと90.6%のF1を達成し、署名ベースのスキャナおよびLLMのベースラインを大幅に上回る。