技術的概要：TLA+ 反例を用いたエージェント協調プロトコルの修復、TraceFix

1. 問題定義

独立した大規模言語モデル（LLM）エージェントは、共有外部状態を変更する並行かつ非同期の環境でますます運用されるようになっている。このような設定において、システム障害は個々のエージェントの能力不足に起因するのではなく、複雑なインターリーブ、競合、デッドロック、見送られたハンドシェイクに起因する協調エラーから生じることが多い。これらの危険性は潜在しており、プロトコルは観測された実行では成功しても、未検証のスケジューリング下では失敗する可能性がある。

従来のアプローチは、明示的なグラフによるオーケストレーションフレームワーク、単一アーティファクトの正しさを目的としたソルバー・イン・ザ・ループ生成、またはランタイムガードを通じて LLM 協調に対処してきた。しかし、これらは特に並行プロトコルの正しさを標的にすることに失敗することが多い。正しい並行プロトコルを作成することは困難であり、エッジケースは特定の、列挙されていないインターリーブの下でのみ出現する。人間または LLM によって生成されたワンショット仕様は、説得力があるが不十分であり、これらのエッジケースを体系的に発見するメカニズムを欠いている。

2. 手法：TraceFix パイプライン

TraceFix は、プロトコル設計を合成、モデル検査、修復の反復ループとして扱う検証ファーストのパイプラインを導入する。このシステムは、設計時合成とランタイム強制の 2 つのフェーズで動作する。

2.1 設計時ループ

パイプラインは、オーケストレーションエージェントによって駆動される 4 つの段階から構成される：

1. トポロジー合成：エージェントは自然言語のタスク記述から**プロトコルトポロジー中間表現（IR）**を合成する。この IR は、エージェント、共有リソース（ロック、カウンター）、および方向付きラベル付きメッセージチャネル（FIFO キュー）を宣言的に定義する。進行する前に JSON スキーマを通じて構造的に検証される。
2. ロジック生成：トポロジーはPlusCal（TLA+ のためのアルゴリズム表記）にコンパイルされる。エージェントは、明示的な制御フロー（送信、受信、ロック取得）および非決定的な選択（either/or）を含む、エージェントごとのプロセス本体を生成する。
3. モデル検査：PlusCal コードは TLA+ に変換され、TLC モデルチェッカーを用いて検証される。TLC は、安全性プロパティをチェックするために、有界な仮定（例えば、有界キューの深さ）の下で到達可能なすべての状態を網羅的に探索する：
   • デッドロックの不在：どのエージェントも進行できない状態がないこと。
   • 相互排除：2 つ以上のエージェントが同じロックを保持していないこと。
   • 孤児ロック：終了時に保持されているロックがないこと。
   • チャネルの排水：エージェントが終了するときにすべてのチャネルが空であること。
4. 反例駆動修復：TLC が違反を発見した場合、具体的な反例トレースを返す。修復エージェントはこのトレースを使用して PlusCal ソースコードを編集し（例えば、ロック順序の強制、ハンドシェイクの追加、ループの再構成）、特定の失敗証人を排除する。TLC が違反を見つけなくなるまでループが繰り返される。

2.2 ランタイム強制

プロトコルが検証に合格すると、検証済みのプロセス本体はエージェント向けのシステムプロンプトにコンパイルされる。トポロジーモニターがランタイムにおいてエージェントと共に実行される。このモニターは、トポロジーで定義された協調インターフェースを強制する：

• すべての協調操作（送信、受信、取得、解放）が、有効なラベルを持つ宣言されたチャネルまたはリソースをターゲットにしていることを検証する。
• トポロジーに違反する操作（トポロジー外操作）を拒否する。
• ステップの順序付けや公平性を強制しない；検証済みの構造的契約内でのみエージェントが留まることを保証する。エージェントはこれらの制約内でドメインツールや意思決定に関する自律性を保持する。

3. 主要な貢献

1. TraceFix システム：トポロジー IR を合成し、PlusCal 協調ロジックを生成し、検証が成功するまで TLC 反例を用いてプロトコルを反復的に修復するプロトコル設計エージェント。
2. 協調ベンチマーク：ソフトウェア開発、研究、製造、CI/CD にまたがる16 のシナリオファミリーの48 タスクからなる新しいベンチマーク。3 つの難易度レベルで定義される。真の正解は、ドメイン意味論ではなく、協調の正しさ（デッドロックの不在、相互排除）によって定義される。
3. ランタイムトポロジー強制：エージェントの自律性を維持しつつ、検証済みのプロトコルトポロジーから逸脱する協調操作を拒否する監視レイヤー。
4. 対照的アブレーション研究：同一のランタイム条件下で検証済みプロトコルと未検証プロトコルを比較することによる、反例駆動修復の寄与の実験的隔離。

4. 実証結果

評価は、プロトコル設計に Claude Opus 4.6 を、ランタイム実行に gpt-5-mini/gpt-5-nano を使用した 48 タスクベンチマーク上で実施された（合計 3,456 回の実行）。

4.1 検証収束

• 100% の最終通過率：すべての 48 タスクが TLC 検証を完全に通過した。
• 効率性：62.5% のタスクが最初の試行で通過した。どのタスクも4 回の修復反復を超えなかった。
• スケーラビリティ：状態空間は 6 つの桁（30 から 770 万の異なる状態）にわたった。それにもかかわらず、検証はすべてのタスクで60 秒未満で完了した（中央値 <1 秒）。
• 失敗分類：必要な 29 回の修復試行のうち、69% はデッドロックであった。支配的な失敗パターンは、根本的な設計欠陥ではなく、構造的な協調危険（例えば、チャネルチェック前の非決定的な受信、衛星エージェントがリトライループを完了する前にハブエージェントが終了すること）であった。ロックのみのタスクは 100% が最初の試行で通過し、チャネル意味論が複雑性の主要な源であることを示している。

4.2 ランタイムパフォーマンス

4 つのランタイムアーキテクチャ（トポロジー監視型、仲介者強制型、プロンプトのみ、チャットのみ）の比較は、以下のことを明らかにした：

• 最高完了率：トポロジー監視型実行が最高のタスク完了率（平均 89.4%、完全完了 81.5%）を達成した。
• 安全性：ベースラインと比較してデッドロック/ライブロック（DL/LL）率が大幅に減少した。
• モデルの劣化：モデル能力が低下した場合（gpt-5-mini から gpt-5-nano へ）、検証済みプロトコルを使用したランタイムは、プロンプトのみまたはチャットみのベースラインの約半分の速度で劣化した。検証済みプロトコルは「能力バッファ」として機能する。
• フォールトトレランス：注入されたフォールト下でも、検証済みプロトコルは高い完了率を維持したが、ベースラインは深刻なパフォーマンス低下を被った。

4.3 アブレーション研究

固定されたトポロジー監視型ランタイム下で、検証済みプロトコルと未検証プロトコルを比較したところ、反例駆動修復は DL/LL 率を**31.1% から 14.1%**に減少させた。改善はフォールト注入下で最も顕著であり、修復プロセスが不利な条件下で増幅される具体的な協調危険を除去することを確認した。

5. 意義と主張

本論文は、TraceFix が LLM 多エージェント協調のための生成/検証/修復パラダイムの実用性を示していることを主張する。

• 修復の必要性：ループは必要である。なぜなら、初期試行の 3 分の 1 以上が失敗するためであり、また十分である。なぜなら、すべてが少数の反復予算内で収束するためである。
• 取扱い可能性：有界モデル検査は、大きな状態空間であっても取扱い可能であり、検証時間を状態空間の大きさから切り離す。
• ランタイムの利益：検証済みプロトコルは、タスク完了とモデル劣化およびフォールトに対する堅牢性の面で測定可能かつ具体的な改善を提供する。
• 範囲の制限：システムは、有界な仮定の下での協調の安全性（デッドロック、相互排除）を検証する。タスク意味論、出力の質、または生存性プロパティ（例えば、保証された終了）は検証しない。なぜなら、LLM プロトコルには厳密な生存性チェックによって拒否される有効な非決定的ループが含まれることが多いためである。

この研究は、形式手法を LLM システムに統合する具体的な実装として位置づけられ、特に多エージェントシステムにおける支配的な失敗モードとして特定された「仕様とオーケストレーションのギャップ」を標的にする。それは、エージェントが何を生成するかではなく、どのように協調するかを検証することで、既存の最適化フレームワーク（DSPy など）を補完する。