OpenShellでのAIエージェント制御への形式手法適用から学んだこと

2026年9月10日 AIエージェント制御への形式手法適用から学んだこと 長期間稼働するAIエージェントにおける権限変更を推論するために形式手法を使用することの紹介。 Alex Watson、OpenShellチーム（NVIDIA） この記事では、エージェントの規模で権限レビューがどのように破綻するか、そしてエージェントが提案するポリシー変更が承認された範囲内に収まることを証明するためにZ3オープンソースライブラリを使用して形式証明を記述する方法について掘り下げます。 エージェント規模で権限レビューが破綻する理由 AIエージェントはより賢くなり、私たちが彼らに依頼する仕事はますます自律的になっています。今日、私たちの多くは、ClaudeやCodexを使用して、一度に1つのPRをコードで反復処理するために、少数のエージェントグループを使用しています。ますます、私たちはエージェントに、数百または数千時間にわたって動作する数百のエージェントが必要な、長期間でオープンエンドの研究タスクを任せ始めており、これはセクターの次のブレークスルーを解き放つ可能性があります。これらのユースケースが拡大するにつれて、いくつかのことが起こり始めます。 エージェントのニーズは進化します。タスクを進めるにつれて、エージェントはデータストア、コーディングリポジトリ、インターネット検索能力、詳細なシミュレーションとテストを実行する能力を必要とするようになります。人間の監督はスケーリングしなくなります。これらの実行が必要な規模では、すべてのエージェントに対する人間の監督自体が不可能になります。これは難しい質問を提起します。一緒に作業しているエージェントのグループ（それぞれ独自のスコープ付きポリシーを持つ）が、システム全体に付与された権限を超えないことをどのように保証できるでしょうか？インターネットへの書き込みアクセスを持つ1つのエージェント、セキュリティツールへのアクセスを持つ別のエージェント、または「競合調査を行う」のような広範にスコープされたチャーターの下で作業するグループを想像してください。システムを人間のオペレーターの意図内にどのように留めることができるでしょうか？これは、サンドボックス権限のリストを細かく見るのをやめ、より高レベルで宣言的な方法で考えることを可能にする、新しいセットの制御とメカニズムを必要とします。この記事では、OpenShellチームでこの分野で行っている研究の一部、特に形式手法の使用を中心に、単一のエージェントだけでなく、エージェントシステム全体の機能の「証明」を構築することについて掘り下げます。 私たちの考えを変えたデモ Jensenのために行ったOpenShellの最初のデモの1つで、OpenShellのREST検査エンドポイントを使用して、広範にスコープされたAPIキーへのアクセスがあるにもかかわらず、OpenClawエージェントがGitHubリポジトリへの書き込みを選択的に許可できることを実証しました。デモは予想通りに始まりました。OpenShellのサンドボックスは、禁止されたリポジトリへの書き込み試行を検出し、それをブロックしました。次に表示されたメッセージは「ファイルが[禁止されたリポジトリ]に正常に書き込まれました」でした。何が起こったのでしょうか？エージェントは自分がサンドボックスで実行されていることを認識し、次にgit-remote-httpsという別の低レベルのGitHubバイナリでGitHub認証情報を使用しました。これは、レイヤー7のHTTP/REST/MCP検査を、当時、Gitリポジトリをクローンするためにポリシーで承認していましたが、それらに書き込む能力があるとは知らなかったバイナリを使用してバイパスしました。賢い。そして、それは1つの点を提起しました。ネットワーク、ファイル、ツール、AIモデル、および認証情報アクセスに関するサンドボックス/ランタイムポリシーの間には、AIエージェントが人間のオペレーターが明確に望まないことを実行できる可能性のある、指数関数的な数の意図しない組み合わせが存在するということです。 以前の作業 - AWSでのEC2、IAM、S3ポリシーの証明 2016年頃、私たちのチームのメンバーはAWSで働いており、同様の課題に直面していました。AWS IAMポリシー、AWS S3ストレージポリシー、履歴バージョンサポートのすべての素晴らしい複雑さを考えると、S3内のオブジェクトがパブリックインターネットからアクセス可能かどうかを断定的に言うことはできますか？今日、これは少しおかしく聞こえますし、2016年にもそうでしたが、システムを制御するために書くポリシー間の複雑さとレイヤー化された相互作用を考えるとそうではありません。Byron Cookと同僚はAWSでZelkovaを開発しました。これはAWSアクセスポリシーをSMT（Satisfiability Modulo Theories）の公式として形式化し、2018年に彼らが研究を発表したときにはすでに毎日数百万回呼び出されていました。その取り組みはAWS全体に広がり、後の研究では1日あたり10億のSMTクエリにスケーリングしたことが説明されています。アイデアは、形式手法、特に定理証明器を使用して、IAM、S3、およびEC2ポリシーを形式的にモデル化することでした。これらのポリシーとその相互作用を形式論理でモデル化したら、不変条件（真であると期待されるもの）が保持されるという証明を構築できました。これは非常に成功し、複雑なポリシーを形式論理でモデル化するという集中的なタスクの後、それらを横断する実際のクエリは非常に高速になり、コンピューティング全体で水平にスケーリングできるという追加の利点がありました。 同じ問題、今度はエージェントで 今日、私たちの課題は非常に似ています。エージェント、またはエージェントシステムはそれぞれ、ファイルシステム、ネットワーク、認証情報、ツール、およびMCPポリシーを持っており、それぞれ異なる機能を持っており、エージェントが異なるエージェントと通信できるため、組み合わされる可能性があります。Frontier Labsは、専門モデルからのエージェントアクションの信頼できるAIエージェントレビューを提唱しており、最も重要なイベントを人間の承認のためにエスカレートし、承認の疲労を軽減しています。しかし、AIモデルは、人間と同様に、確率的であり、重要な詳細を見落とす可能性があります。さらに、すべてのエージェントアクションを同等の知能を持つレビューアモデルでレビューすると、コンピューティングコストが2倍になり、総トークンスループットが実質的に半分になります。 OpenShellで実験および検証しているのは、形式手法を使用して、コードリポジトリへの書き込みや本番データベースへの削除をブロックするルールをバイパスする意図しない方法など、ポリシー内の特定の不変条件をモデル化し、柔軟に「証明」することです。私たちが発見したのは、これらのポリシーのモデリングは複雑であり、最新の状態に保つ必要があるということですが、いくつかの非常に強力な利点があります。 いつでも形式的に監査または証明できる能力 私たちのポリシーの理解に対する決定論的な「証明」 これらのチェックはミリ秒単位で実行され、トークンは不要です。 これらの論理チェックは、一時的な使い捨てリポジトリの削除アクセスを要求する場合と、本番リポジトリの削除アクセスを要求する場合のようなコンテキストを理解しません。しかし、人間または信頼できるAIレビューアと組み合わせることで、これらの証明は、機密性の高い物理的（現実世界）または規制管理された環境で実行するために必要な形式的な監査証跡を提供し、かつ、欺かれたり誤解されたりすることのない出力を持つ確率的AIレビューアに信じられないほどの価値を提供できます。 あなたのポリシー定義に対する証明はあなたに何をもたらしますか？ 私たちは、エージェント制御に関する研究の非常に有望な分野として形式手法を考えています。これらの証明の例は、敵対的な研究実験でこちらで見ることができます：https://nvidia.github.io/OpenShell-Research/dev-notes/posts/2026-08-27-adversarial-policy-review-long-horizon-agents/ 形式手法はポリシー検証だけでなく、クリティカルシステムで長い歴史を持っています。航空管制システム、コアインターネットスイッチングとルーティング、さらには私たちのシステムで毎日使用しているパッケージマネージャーまで、ソフトウェア間の複雑な依存関係が正しく一致することを保証するために使用されています。多くのAI研究者にとって、私たちの中には大学で形式検証のクラスを取ったことがあるかもしれませんが、実際に形式検証を使用したことがある人は比較的少数です。この記事の残りの部分では、アルゴリズム検証の紹介を探求し、人気のあるオープンソースソルバーを使用して、OpenShellでエージェント制御のための最小限の例をゼロから構築します。 SAT、SMT、およびZ3を5分で コンピュータサイエンスと形式手法では、SAT（Satisfiability）ソルバーはブール式が充足可能かどうかを回答します。変数（例えばxとy）に真となる値が存在する場合、SATソルバーはtrueを返します。そうでない場合はfalseを返します。変数aとbのような変数を与えると、この式を真にする割り当てを見つけることができます：a AND (NOT b) 対照的に、SMT（Satisfiability Modulo Theories）ソルバーは、そのスタイルの推論を拡張します。