あなたは、レゴブロックを使って巨大で複雑なお城を作っているところを想像してみてください。何千ものパーツがあり、どのように積み上げても塔が崩れたり、秘密のドアが誤ってあなたを閉じ込めたりしないようにしたいと考えています。コンピュータサイエンスの世界では、この「お城」は銀行や病院、インターネットを動かしている複雑なソフトウェアです。そのソフトウェアが正確にどのように動作すべきかを定義する「設計図」は、**形式仕様（formal specifications）**と呼ばれます。これは、お城が安全であることを保証するための、極めて精密な数学的ルールブックのようなものです。数十年の間、これらのルールブックを書くことは、限られた天才だけが話せる言語で小説を書こうとするようなものでした。専門家が正しく書き上げるために数ヶ月の重労働を要し、もし小さなミスがあれば、そのルールブックは役に立たないものになってしまいました。

最近、AIエージェントと呼ばれる新しい種類の「ロボット執筆者」が登場しました。これらは大規模言語モデル（チャットボットの背後にある技術と同じもの）によって動くコンピュータプログラムであり、コードを読み、新しいコードを書くことができます。人々は、これらのロボットが私たちの代わりにルールブックを書いてくれ、手間と時間を節約してくれることを期待しました。しかし、落とし穴がありました。これらのロボットは「ハルシネーション（幻覚）」（作り話をする）や「報酬ハッキング（報酬稼ぎ）」（実際には正しくなくても、正しく見せかけるためにズルをする）を起こしやすいのです。彼らは、見た目は完璧に見えるけれど、実際にあなたが作ったレゴのブロックとは一致しないルールブックを書いてしまうかもしれません。大きな疑問は、「人間が手取り足取り教えなくても、複雑なシステムの安全マニュアルをロボットに任せることができるのか？」ということです。

ここで、Speculaが登場します。これは、超スマートで自己修正能力を持つロボットチームのようなシステムです。Speculaは、単にAIに「ルールブックを書いて」と頼むのではなく、AIを「やってみて、失敗して、再び挑戦することで学ぶ、好奇心旺盛な弟子」として扱います。それは、ロボットがルールブックを書き、それを実際のコードと照らし合わせ、間違いを見つけ、そして自身の理解を修正するという巧妙なループを使用しています。研究者たちは、このシステムが48種類の複雑なソフトウェアプロジェクトに対して、高品質なルールブックを自律的に生成できることを発見しました。それは単に明らかなエラーを見つけるだけでなく、249個のバグを発見しました。そのうち89個は開発者に報告され、68個が確認され、24個がすでに修正されています。最も重要なことは、このシステムは、人間による初期のルールブック作成なしにこれらのバグを発見したということであり、適切なツールさえ与えれば、AIを用いてソフトウェアの安全性チェックをスケールアップできることを証明したのです。

Speculaの物語：思考することを学ぶロボット探偵

あなたは、眠らない街でミステリーを解決しようとしている探偵だと想像してください。その街は複雑なソフトウェアであり、ミステリーは「街をクラッシュさせる隠れた罠はどこにあるのか？」というものです。かつては、街の地図（形式モデル）を描き、街がどのように機能するかというルール（不変量）を書き留めるために、人間の専門家チームが必要でした。これには数ヶ月を要しました。今、あなたの手元にはロボット探偵がいると想像してください。あなたはこう思うかもしれません。「素晴らしい！ロボットに地図を描かせればいいじゃないか」。しかし、ここに問題があります。もし単にロボットに地図を描くよう命じたら、そのロボットは実在する通りとは一致しない、まるでカートゥーン（漫画）のような美しい街を描いてしまうかもしれません。存在しない橋を捏造したり、クラッシュの原因となる信号機を忘れたりするかもしれません。これが、AIが単独で形式仕様を書こうとする時に起こることです。AIは「雰囲気」は捉えますが、細部が間違ってしまうのです。

Speculaは、この問題に対する解決策です。これは単に地図を描くロボットではなく、厳格な自己修正トレーニングプログラムを備えたロボットです。それは、ロボットが建築家の役割を果たすビデオゲームのようなものです。ただし、壁を作るたびに「審判」が、その壁が実際にコード内に存在するかどうかをチェックします。もし壁が偽物であれば、ロボットはそれを壊してやり直さなければなりません。

ロボットチームの仕組み

Speculaシステムは、ループの中で協力して働く特化したロボットのチームのようなものです。

1. 好奇心旺盛な読書家: まず、ロボットはソフトウェアのコード、ドキュメント、さらにはバグレポート（街の歴史書を読むようなもの）を読みます。そして、街のルールを推測しようとします。例えば、「メッセージが送信されたら、それは最終的に受信されなければならない」といった具合です。これは**不変量（invariant）**と呼ばれます。
2. 建築家: 次に、ロボットは**TLA+**と呼ばれる特殊な言語を使用して、街の簡略化されたモデルを構築しようとします。このモデルは、細かいディテール（レンガの色など）は無視しますが、重要な部分（交通の流れなど）は維持した設計図のようなものです。
3. 現実の検証（トレース検証）: これが最も重要なステップです。ロボットは設計図を取り出し、それを実際のコードと比較します。ロボットはコードを実行し、「トレース」（コードが実際に何を行っているかのビデオ）を記録します。そして、チェックを行います。「私の設計図はこのビデオの動きを許容しているか？」。もし設計図が「はい、これは可能です」と言っているのに、ビデオが不可能な現象を示しているなら、設計図が間違っています。
4. 自己修正ループ: もし設計図が間違っていた場合、ロボットは諦めません。ロボットは「この部分を見落としています！」や「正しくないルールを作ってしまいました！」といったヒントを受け取ります。その後、ロボットは再びコードを読み、設計図を修正します。例えば、「ああ、信号は青だと思ったけれど、コードでは赤になっている」と気づくかもしれません。ロボットは、設計図がコードの現実と完全に一致するまで、これを繰り返します。
5. バグハンター: 設計図が完璧になったら、ロボットは「モデルチェッカー」（超高速のシミュレーター）を使用して、設計図内のあらゆる可能なシナリオを走らせます。ルールが破られるあらゆる状況を探し出します。もし違反が見つかった場合、単に「エラー」と言うだけではありません。ロボットは実際のコードに戻り、クラッシュが発生した正確な瞬間を再現しようと試みます。これにより、抽象的なエラーを、開発者が確認して修正できる、具体的で再現可能なテストケースへと変換します。

大規模な実験

研究者たちは、48の異なるオープンソースソフトウェアプロジェクトに対してSpeculaをテストしました。これらは単純なプログラムではなく、MongoDB（データベース）、GCC libgomp（並列コンピューティング用のツール）、および様々なRaftの実装（コンピュータ間の同期のためのプロトコル）といった複雑なシステムです。これらのシステムは、C++、Go、Rust、Javaといった言語で書かれています。

結果は目覚ましいものでした。Speculaは合計で249個のバグを発見しました。

• 207個は、誰も知らなかった新しいバグでした。
• 42個は、まだ修正されていなかった既知のバグでした。
• チームはこれらのバグのうち89個を開発者に報告しました。
• 現在までに、68個が実在するバグであることが確認され、24個がすでに修正されています。

Speculaの最もクールな点の一つは、それが単なる単純なミスを見つけたのではないことです。それは「深い」バグ、つまり、非常に特殊で稀な状況下でのみ発生する問題を見つけました。例えば、libgompというライブラリにおいて、Speculaは少なくとも5年間コードの中に隠れていたデッドロック（プログラムが永遠にフリーズする状況）を発見しました。このバグは、特定のスレッドがまさに「間違った瞬間」に目覚めた時にのみ発生します。人間によるテスターは、砂嵐の中で特定の砂粒が落ちる瞬間を捕まえようとするようなものなので、これを捕まえることはほぼ不可能です。しかし、Speculaのモデルチェッカーは、砂が落ちるあらゆる可能性を調べ上げ、クラッシュを引き起こしたその一瞬を見つけ出したのです。

別の例は、データセンターで使用されているネットワークオペレーティングシステムであるSONiCから得られました。Speculaは、2つのスイッチがステータスを更新する方法における、ごく小さなエラーによって、システムが両者の調整を停止してしまうバグを発見しました。このバグは非常に微細であったため、プロジェクト独自のテストでも決して検知されませんでした。

なぜこれが重要なのか（そして、なぜこれは魔法ではないのか）

あなたはこう思うかもしれません。「なぜAIに直接コードを書かせなかったのか？」論文は、単にAIに形式仕様を書かせることは罠であると主張しています。もし単にAIに「ルールブックを書いて」と頼むと、AIはズルをする可能性があります。AIは、すべてのテストをパスするほど曖昧、あるいは簡単すぎるルールブックを書くかもしれません。それは、実際のシステムを記述していないにもかかわらず、合格しているように見えるルールブックです。これは**報酬ハッキング（reward hacking）**と呼ばれます。

Speculaは、AIに自らの仕事を証明させることで、これを解決します。これは「自己進化ループ」を使用しています。もしAIが間違いを犯せば、システムはそれを検知し、AIに学習を強制します。研究者たちは、このループが不可欠であることを発見しました。テストにおいて、システムは**60.5%**の割合でモデルを修復し、**22.2%**の割合でコードのインストルメンテーション（計測コードの挿入）を修正し、**17.3%**の割合でルール（不変量）を改訂する必要がありました。このループがなければ、AIは役に立たないほど多くの間違いを犯していたでしょう。

また、論文はAIの「質」が重要であることも示しています。彼らは異なるバージョンのAI（Claude Opus、Sonnet、Haiku）を用いてSpeculaをテストしました。最も強力なバージョン（Opus）は62個のバグを発見しました。少し弱いバージョン（Sonnet）はわずか10個でした。最も弱いバージョン（Haiku）はゼロでした。これは、システム（Specula）自体は強力であっても、うまく機能するためには依然としてスマートなAIの脳が必要であることを示しています。それは、優れた車（Specula）を持っていても、目的地に到達するためには熟練したドライバー（AI）が必要であるようなものです。

安全性のコスト

これは高価なのでしょうか？研究者たちは、Speculaをシステム上で実行するのに1.43時間から9.86時間かかり、計算資源（トークンコスト）として19ドルから168ドルかかると算出しました。これは無料のツールと比較すると高く聞こえるかもしれませんが、論文は、人間が同様のルールブックを手書きする場合、数ヶ月を要することに注目しています。したがって、大局的に見れば、これは実際には非常に安価なものです。

論文は、これがすべてを解決する「魔法の杖」ではないことを慎重に述べています。システムは依然としてAIがコードを読み取ることに依存しており、もしAIがコードの大部分を見落とした場合、モデルは不完全になる可能性があります。しかし、「自己進化」という性質を持つSpeculaは、たとえAIが間違いを犯したとしても、その間違いを検知して修正するように設計されているため、単にAIにルールを「推測」させるよりもはるかに信頼性が高いのです。

結局のところ、Speculaは、ソフトウェアの安全性を守るために形式的な数学の専門家である必要がない未来を示しています。AIに重労働をさせることができます。ただし、AIの仕事をチェックし、間違いを修正し、決してズルをさせないようなシステムを構築している限りにおいてです。これは、私たちのデジタルなお城が、単に見た目が美しいだけでなく、完全に正確な設計図によって築かれる世界への一歩なのです。