あなたは、魔法の自己修復機能を持つレンガのセットを使って家を建てているところだと想像してください。これらのレンガは「Rust」と呼ばれ、非常に有名です。なぜなら、不安定なものを建てようとすると「ダメだ！」と叫んで阻止する、内蔵された安全検査官がいるからです。もし壁があるべき場所に窓を置こうとすれば、検査官は最初の石を置く前に「ノー！」と叫んであなたを止めます。このため、Rustはソフトウェアを構築する上で非常に安全であり、問題が発生する前にクラッシュやセキュリティホールを防いでくれます。しかし、熟練の建築家が、重い梁を素早く動かすために特別な危険な道具を使いたいとき、時としてそのような事態が起こります。Rustの世界では、これは「unsafe code（アンセーフ・コード）」と呼ばれます。これは、検査官を回避して通り抜けるための秘密のパスのようなものですが、非常に高い代償を伴います。たった一つのミスをしただけで、家全体が崩壊してしまう可能性があるからです。家を建てる状態に保つためには、これらの危険な道具をどのように安全に使用するかを正確に証明する、非常に厳格な数学的「ルールブック（仕様書）」を書く必要があります。しかし、これらのルールブックを手書きすることは非常に困難で、時間がかかり、ヒューマンエラーが起きやすいのです。

ここで、KaPilotの物語が始まります。このプロジェクトの研究者たちは、次のような単純な問いを立てました。「超スマートなコンピュータの脳（AI）に、私たちの代わりにこれらの安全ルールブックを書かせることはできるだろうか？」という問いです。課題は、これらのAIはコードを書くことには長けているものの、コードの背後にある「意図」を理解するのではなく、目にするコードのミスをそのままコピーしてしまうことが多いという点です。彼らは完璧に見えるルールブックを書くかもしれませんが、実は致命的な細部を見落としているかもしれません。この論文では、このパズルを解決するために協力して働くAIエージェントのチーム、KaPilotを紹介しています。単にAIに「ルールを書いて」と頼むのではなく、KaPilotは探偵、作家、そして厳格な編集者の役割をすべて兼ね備えたシステムとして機能します。それは、建築家のメモ（ドキュメント）を読み、真の安全要件を抽出し、ドラフトを作成し、穴がないかチェックし、そしてそれが実際に機能するかどうかを確認するための厳格なテストを実行します。その結果、このシステムは危険なコードに対する高品質な安全ルールを自動生成することができ、人間の専門家がすべてのルールを手書きする必要なく、より安全なソフトウェアを構築することを容易にします。

探偵、作家、そして編集者

アンセーフなRustコードの検証プロセスを、ブレーキのない高速レースカーのための完璧な取扱説明書を書くことだと考えてみてください。もしマニュアルが間違っていれば、車は衝突します。もしマニュアルが曖昧すぎれば、ドライバーは運転できません。もしマニュアルが厳しすぎれば、ドライバーは全く動けなくなります。

KaPilotはマルチエージェント・フレームワークであり、それは単に、特化したAIキャラクターのチームが協力して働いていることを意味します。彼らがどのように役割を果たすのかを見てみましょう。

1. 探偵 (SafetyReq): 何かを書き始める前に、チームは何がルールであるべきかを知る必要があります。通常、これらのルールは、コードと共に提供される乱雑な人間によるメモ（ドキュメント）の中に隠されています。「SafetyReq」エージェントは探偵のように振る舞います。彼はこれらのメモを読み、余計な情報を無視し、クリーンで簡潔な安全要件のリストを抽出します。これは、例えば「赤いボタンに触るな」というとりとめもない物語を、「1. 赤いボタンを押さないこと。2. 赤いボタンから5フィート以内に立たないこと」という明確な番号付きリストに変えるような作業です。このステップが極めて重要なのは、AIがコードのミスを単にコピーしてしまうのを防ぐためです。
2. 作家 (SpecGenerate): 探偵がリストを作成したら、「SpecGenerate」エージェントが登場します。彼は、そのリストをコンピュータが理解できる形式（具体的にはKaniと呼ばれる言語）に変換する作家です。彼は単に推測するのではなく、探偵のリストを厳格なガイドとして使用します。
3. 編集者 (SpecPrecheck): 作家のドラフトが最終ボスに送られる前に、「SpecPrecheck」エージェントがレビューを行います。彼は厳格な編集者であり、「探偵が見つけたすべてのポイントをカバーしているか？ 文言が弱すぎないか？ 強すぎないか？」と問いかけます。もしドラフトが雑であれば、編集者は修正方法についての具体的な指示を添えて、作家にドラフトを差し戻します。ドラフトが堅実になるまで、このループは繰り返されます。
4. テストドライバー (SpecVerify): 最後に、「SpecVerify」エージェントがドラフトを受け取り、現実世界のテストにかけます。彼はKaniというツールを使用して、何百万もの異なる走行シナリオをシミュレートし、車が衝突するかどうかを確認します。もし車が衝突した場合（検証が失敗した場合）、テストドライバーは作家に対して、なぜ衝突したのかという理由を正確に伝え、ループが再び始まります。

「シャッフル＆ミックス」戦略

ここからが、このチームの非常に賢いところです。時として、AIはいくつかの異なるバージョンのルールブックを生成することがあります。あるバージョンは完璧な「開始条件（事前条件）」を持っているかもしれませんが、「終了条件（事後条件）」が弱いかもしれません。別のバージョンは、開始条件は弱いが終了条件は完璧かもしれません。もし一つだけを選んでしまうと、最良の組み合わせを見逃す可能性があります。

KaPilotは**「シャッフル・アンド・インプリケーション（混ぜ合わせと含意）」**と呼ばれる戦略を使用しています。ルールブックの各パーツが異なるカードであると想像してください。チームはこれらのカードをシャッフルし、あるバージョンの最高の「開始」部分と、別のバージョンの最高の「終了」部分を混ぜ合わせます。そして、これらの新しい組み合わせをテストし、元のドラフトよりも優れたものになるかどうかを確認します。これは、ある車から最高のエンジンを取り出し、別の車から最高のタイヤを取り出して、究極のレーシングカーを組み立てるようなものです。これにより、彼らは単に「そこそこ良い」ルールブックで妥協するのではなく、最高のルールブックを見つけ出すことができるのです。

得られた成果

研究者たちは、124個の異なるアンセーフなRustコードを用いてKaPilotのテストを行いました。これらは2つのグループに分けられました。

• ゴールド・セット (54個の関数): これらには人間の専門家によって書かれた「正解（グラウンドトゥルース）」となるルールブックが存在するため、チームはKaPilotの成果が正しいかどうかを確認できました。
• ウルトラ・セット (70個の関数): これらには人間のルールブックが存在しないため、チームはKaPilotが「動作するルールブック」を生成できるかどうかのみを確認しました。

結果は目覚ましいものでした。ゴールド・セットにおいて、KaPilotは**88.9%**の関数に対して動作するルールブックの生成に成功しました。さらに重要なことに、**57.4%**の確率で、作成されたルールブックは人間の専門家が書いたものと同等、あるいはそれ以上に優れていました。ウルトラ・セットについては、**71.4%**の関数に対して動作するルールブックを作成できました。

KaPilotを、別のAIツールであるAutoSpec（この新しいシステムに合わせて適応させたもの）と比較したところ、KaPilotが圧倒的な勝利を収めました。KaPilotは、テストを通過するルールブックを**14.8%多く生成し、人間の書いたものと同等またはそれ以上に優れた意味論的なルールブックを25.9%**多く生成しました。

なぜこれが重要なのか

この論文は、単にAIに「このコードに基づいて安全ルールを書いて」と頼むだけでは、うまくいかないことを主張しています。AIはコードの欠陥をコピーしたり、複雑さに混乱したりする傾向があるからです。タスクを専門家チーム（読み手、書き手、編集者、テスター）に分割することで、KaPilotはこれらの落とし穴を回避しています。

また、研究者たちは、人間によるメモ（ドキュメント）の質が非常に重要であることも発見しました。メモが曖昧であれば、AIは苦戦します。しかし、メモが明確であれば、KaPilotは真価を発揮します。彼らはまた、「シャッフル」戦略が鍵となる要素であることも明らかにしました。これがなければ、システムは完璧な組み合わせを見つける代わりに、平凡な解決策に落ち着いてしまうことが多かったのです。

要するに、KaPilotは、人間の専門知識とAIのスピードのどちらか一方を選ぶ必要はないことを示唆しています。厳格かつ論理的なプロセスに従う専門のアシスタントチームとしてAIを活用することで、ソフトウェアの最も危険な部分に対する安全ルール作成を自動化し、デジタル世界をより安全な場所にすることができるのです。この論文は、これがすべての問題を解決すると主張しているわけではありません（複雑なループなどは依然として人間の助けが必要です）。しかし、このマルチエージェント・アプローチが、ソフトウェア検証を自動化し、信頼できるものにするための大きな一歩であることを証明しています。