Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers

AIエージェントのデジタル健忘症

あなたは、旅行の計画を立てたり物語を書いたりといった複雑なタスクを実行できるロボットを作っていると想像してください。時として、このロボットはあなたに「フライトを予約すべきですか？」や「このストーリー展開はどうですか？」といった質問をするために、動作を一時停止する必要があります。これは「中断（interrupt）」と呼ばれます。もしロボットがクラッシュしたり、電源が切れたり、あるいは中断されたりした場合、ロボットは中断した場所から正確に再開できるように、どこまで進んだかを記憶しておく方法が必要です。これは「永続性（persistence）」と呼ばれます。

コンピュータサイエンスの世界、特に人工知能（AI）ワークフローの分野では、ある問題が深刻化しています。中断と再開ができる多くの異なる「ロボットの脳（フレームワーク）」を私たちは構築してきました。しかし、これらのロボットは、自分が「すでに何をしたか」を覚えていることが非常に苦手です。もしロボットがタスクを完了し、進捗を保存し、その後再起動した場合、行儀の良いロボットであれば「それはすでに完了しました。次に進みましょう」と言うべきです。しかし、混乱したロボットは「それをやった記憶がありません！」と言い、同じタスクを何度も繰り返してしまうかもしれません。もしそのタスクがメールの送信やクレジットカードの決済であった場合、二重に行うことは災難を招きます。本論文は、現在のAIロボットが本当に混乱しているのか、それとも単に賢いふりをしているだけなのかを調査するものです。

---

偉大なる「レジューム（再開）」の混乱

この論文は、探偵小説のようなものです。ただし、著者のサッジャド・カーン（Sajjad Khan）が解決しようとしているのは殺人事件ではなく、「デジタルの健忘症」というミステリーです。謎はこうです：AIエージェントが一時停止し、その後再開するとき、そのエージェントは既に行ったことを覚えているのか、それとも誤って同じことを繰り返してしまうのか？

著者は、現在普及している5つの主要なAIフレームワークが、すべて異なる、あるいは矛盾するルールブックに従って動いていることを発見しました。それはまるで、5つの異なるビデオゲームがあり、あるゲームでは「続行」を押すとクリアしたレベルをスキップできるのに、別のゲームでは再びボス戦を強制されるようなものです。さらに悪いことに、これらのゲームの中には、自分がどのルールを使用しているのかさえ教えてくれないものもあります。

優れたレジュームのための6つのルール

誰が公平にプレイしているかを判断するために、著者は「レジューム契約（Resume Contract）」を考案しました。これは、ロボットが昼寝から目覚めたときにどのように振る舞うべきかを示すルールブックだと考えてください。この契約には、主に6つのルールがあります。

1. 接頭辞による継続（Prefix Continuation）: 目覚めたとき、映画の最初からではなく、中断した場所から正確に開始しなければならない。
2. 効果の一回のみ（Effect Exactly-Once）: すでにメールを送信したりカード決済を行ったりした場合、二度と行ってはならない。必ず一度きりにすること。
3. 分岐の決定論（Fork Determinism）: もし進む道が分かれた場合（例：「左に行く」対「右に行く」）、ロボットは自分がどの道を選んだかを覚えていなければならない。もしあなたが二度目に「左」と言ったとしても、二度目の選択が「右」のように扱われてはならない。
4. チェックポイントの妥当性（Checkpoint Validity）: ロボットのメモリログはクリーンでなければならない。後でクラッシュする原因となるような「ゴミ」や壊れたデータを保存してはならない。
5. 一度限りの消費（Consume-Once）: 人間が回答を与えた場合（例：「はい、フライトを予約してください」）、ロボットはその回答を一度だけ使用しなければならない。一つの「はい」を使って二つのフライトを予約してしまうようなことがあってはならない。
6. 復旧の決定論（Recovery Determinism）: 二つのロボットが全く同じメモリログを持って目覚めた場合、彼らは全く同じ決定を下さなければならない。

調査：誰が失敗したのか？

著者は、5つの人気のあるAIフレームワークをテストするために、極めて精密な、ロボットを使用しないテスト用装置（ハーネス）を構築しました。テストには人間の脳もAIモデルも関与しておらず、純粋なコードのみが使用されました。結果は衝撃的でした：どの2つのフレームワークも同じようには振る舞いませんでした。

• LangGraph: このフレームワークは、自分の宿題を忘れるロボットのようなものです。クラッシュして再起動すると、すでに完了した作業をやり直してしまいます（「効果の一回のみ」に違反）。また、考えを変えようとした場合（「分岐」）、新しい選択を無視して古い選択を繰り返すというグリッチ（不具合）もあります。
• CrewAI: これはさらに混沌としています。完了した作業をスキップすると主張していますが、再起動すると結局すべてをやり直します。それはまるで、「玉ねぎはもう刻みました」と言いながら、再び玉ねぎを刻んで時間と材料を無駄にするシェフのようです。
• LlamaIndex Workflows: このフレームワークは、自身の混乱に対して正直です。「注意：一時停止すると、停止前の作業をやり直す可能性があります」と認めています。これはバグではなく、文書化された仕様（フィーチャー）ですが、決済などの用途では依然としてリスクがあります。
• pydantic-graph: このロボットは非常に脆弱で、タスクの途中でクラッシュすると、二度と目覚めることができません。それは、ギアが入ったままエンジンを切ると始動しなくなる車のようなものです。
• AutoGen: これは、「おい、壊れたセーブファイルをロードしようとしたぞ！」と大声で警告し、実行を拒否する唯一の存在です。バリデーション・チェックを回避させない厳格な教師のような存在です。

「ダブルブッキング」の惨劇

最も危険な発見の一つは、**一度限りの消費（Consume-Once）**に関するものでした。人間が回答を与えるための「パーキングスペース（待機場所）」があると想像してください。もし二人の人間が同時に回答を試みた場合、現在のシステムでは両方の人が「駐車」できてしまいます。するとロボットは、二つの回答を受け取ったと判断し、タスクを二度実行してしまいます。
著者は、同時に回答しようとする16人の「レーサー」を用いてこれをテストしました。40回のテストのうち36回において、システムは完全に失敗し、16人全員がアクションをトリガーさせてしまいました。それは、16人が同じチケットを購入しようとしたとき、システムが全員を通してしまうチケット売り場のようなものです。

証明と修正

著者は単に推測したのではなく、TLA+と呼ばれる数学的ツールを使用して、何百万ものシナリオをシミュレートし、これらの失敗が単なる不運ではなく現実であることを証明しました。また、完璧なロボットエンジンであるREMITを構築するために、形式検証ツールであるVerusを使用しました。

REMITは、ルールを完璧に遵守するリファレンス・エンジンです。これは、どの道を選んだかを正確に記憶することで「分岐」の問題を解決し、回答をロックすることで「ダブルブッキング」の問題を解決します。著者は、REMITを使用した場合、64個のスレッドが同時に話しかけてきても、ロボットが正しく動作することを示しました。

まとめ

ここでの大きな教訓は、AIフレームワークが「チェックポインティング（保存と再開の能力）」を持っていると言っていても、それがお金やメッセージ送信のような重要な事柄に対して安全であるとは限らないということです。現在、多くのAIツールの「レジューム（再開）」ボタンは、二重課金やデータの紛失を引き起こす可能性のある形で壊れています。

本論文は、開発者が自分のAIが目覚めたときに何をすべきかを正確に理解するために、標準的なルールブック（レジューム契約）が必要であることを証明しています。それまでは、もしあなたが現実世界のタスクを実行するAIを構築しているなら、フレームワークが記憶してくれることをただ信じるのではなく、独自のセーフティネットを構築しなければなりません。著者は、開発者がシステムを修正し、安全にするために使用できる無料のツール（REMIT）を公開しており、現在の一般的なツールがまだ実現できていないとしても、完璧でルールを遵守するレジュームが可能であることを証明しています。