あなたは、新しい、謎めいたレシピ本を使って、非常に複雑なケーキを焼く方法をロボットに教えようとしているところだと想像してください。その本（ディープラーニング・ライブラリ）は膨大ですが、指示は曖昧です。「小麦粉を加える」とは書いてありますが、小麦粉と砂糖の比率をどうすべきか、あるいは巨大なボウルいっぱいの生地を小さなスプーンで混ぜようとしたらどうなるか、といったことは教えてくれません。もし予想を外せば、ロボットはキッチンを破壊してしまうかもしれませんし、もっと悪いことに、見た目は立派なのに味はひどいケーキを焼き上げてしまうかもしれません。

これは、現代のAIを支える「レシピ本」であるディープラーニング・ライブラリ（PyTorchやTensorFlowなど）に対して、研究者が直面した問題そのものです。これらのライブラリは強力ですが、隠れた罠（バグ）に満ちています。問題は、これらのライブラリのマニュアルが不完全であったり、散逸していたり、あるいは分かりにくい言葉で書かれていたりすることです。

そこで登場するのが、これらのライブラリをテストするために研究者によって開発された新しいツール、「Centaur（ケンタウロス）」です。Centaurを、人間の創造的な直感とコンピュータの厳格な論理という、2つの異なる思考方法を組み合わせた「超スマートな探偵」だと考えてください。

Centaurの2つの脳

Centaurは「ニューロシンボリック」です。これは、2つの脳が連携して動いているという、少し専門的な言い方です。

1. 「ニューラル」な脳（クリエイティブな探偵）： この部分は**大規模言語モデル（LLM）**を使用します。これは、何百万もの料理ブログやレシピ本を読んできた、非常に博識なシェフのようなものです。Centaurがある特定の関数（例えば「2つの数字を足す」など）を見たとき、LLMはその知識を用いてルールを推測します。「おい」とLLMは言うかもしれません。「通常、2つのリストを足すときは、サイズが同じであるか、あるいは片方がコピー可能な単一の数値である必要があるはずだ」。

   • 注意点： LLMは創造的ですが、間違いを犯すこともあります。もっともらしく聞こえるものの、実際には正しくないルールを推測してしまう可能性があるのです。

2. 「シンボリック」な脳（厳格な数学教授）： この部分はSMTソルバー（一種の論理エンジン）を使用します。これは、シェフが行ったすべての推測をチェックする、厳格な数学教師のようなものです。もしシェフが「小麦粉5カップに砂糖2カップを混ぜることができる」と言った場合、数学教授はそれが物理法則（あるいはこの場合はソフトウェアの法則）に反せずに実際に機能するかどうかを計算して確認します。

   • その力： 数学教授は単に「はい」か「いいえ」と言うだけではありません。ルールが機能することを証明するために、何千もの具体的な有効な例（例：「小麦粉3カップ、砂糖1カップ」）を生成することができます。

Centaurの仕組み（レシピ）

以下は、Centaurが使用するステップ・バイ・ステップのプロセスを簡単に説明したものです。

ステップ1：推測ゲーム（ルール生成）
Centaurは「シェフ」（LLM）に対し、特定の関数がどのように機能すべきかというルールを書き出すよう求めます。シェフが暴走しないように、Centaurは特別なテンプレート（文法）を与え、ルールが特定の論理的な形式で書かれるように強制します。シェフは、「2つのテンソルは同じ形状でなければならない」といったルールを推測するかもしれません。

ステップ2：事実確認（制約学習）
次に、Centaurはこれらの推測を、既知の「正しい」入力（有効なデータ）のセットと照らし合わせてテストします。

• もしルールがすべての「正しい」入力に対して成立する場合、Centaurはそのルールを保持します。
• もしルールが失敗する場合、Cent היא はそれを捨てます。
• 洗練： 時として、シェフが全く同じ意味を持つ2つのルールを推測することがあります。Centaurには、これらの重複を特定して取り除く特別なトリックがあり、混乱を防ぎます。

ステップ3：大量生産（ファジング）
検証されたルールのリストを手に入れたら、今度は「数学教授」（SMTソルバー）を使用して、数百万個の新しいテストケースを生成します。ルールが数学的に証明されているため、Centaurが作成する入力のほとんどすべてが有効であることを知っています。それは、決して焦げたり生焼けだったりすることのない、完璧なケーキの生地だけを作り出す機械を持っているようなものです。

ステップ4：クラッシュテスト
Centaurは、これら数百万の完璧な入力をディープラーニング・ライブラリに投入します。もしライブラリがクラッシュしたり、フリーズしたり、奇妙な回答を出したりすれば、Centaurはそれをバグとしてフラグを立てます。

なぜこれが重要なのか？

従来のツールは、主に2つの方法でバグを探そうとしてきました。

• 「ランダム投げ」： ライブラリにランダムなデータを投げつける方法です。これは目隠しをしてダーツを投げるようなものです。ほとんどのダーツは的（有効な入力）を外してしまい、時間を無駄にします。
• 「コード読み」： ライブラリのソースコードを読んでルールを理解しようとする方法です。これは、家が建設されている最中にその設計図を読もうとするようなものです。時間がかかる上に、設計図が乱雑であれば迷子になってしまいます。

Centaurは違います。 ライブラリがどのように振る舞うかを観察することによって（LLMを使用）、ルールを学習し、その後に数学を用いて完璧なテストケースを生成します。

結果（論文の主張）

研究チームは、最も人気のあるAIライブラリであるPyTorchとTensorFlowを用いてCentaurをテストしました。その結果は以下の通りです。

• 正確性： Centaurのルールは94%の精度を誇りました。推測を誤ることは滅多になく、実際に存在するルールを見逃すこともほとんどありませんでした。
• 効率性： 他のツールは主に無効な入力を生成していましたが（それは役に立ちません）、Centaurは98%有効な入力を生成しました。つまり、不可能なシナリオに時間を浪費することなく、ほぼすべての時間を実際のテストに費やせたのです。
• カバレッジ（網羅率）： Centaurは、従来の最高水準のツールよりも多くのコード部分を探索しました。それは、表面的なエラーではなく、ソフトウェアのコア・ロジックにある「深い」バグを見つけ出しました。
• バグハンティング： Centaurを使用することで、チームはこれらのライブラリから26個の新しいバグを発見しました。そのうち18個は開発者によって確認されました。そのうちの1つは、論文の発表前に修正さえされました！

「深いバグ」に関する簡単な比喩

架け橋を想像してみてください。

• 浅いバグは、道路脇にあるポットホール（穴）のようなものです。簡単に見つかり、簡単に直せます。
• 深いバグは、主要な支持梁にある亀裂のようなものです。外側からは見えませんが、重いトラックが通ると、橋全体が崩落する可能性があります。

従来のツールは主にポットホールを見つけるものでした。しかし、橋がどのように建設されているかという複雑なルールを理解することで、Centaurは支持梁の亀裂を見つけることができたのです。

まとめ

Centaurは、クリエイティブなAIを使ってディープラーニング・ライブラリのルールを推測し、論理的な数学エンジンを使ってそれらのルールを検証し、数百万の完璧なテストケースを生成する、新しいテストツールです。この組み合わせにより、他のツールが見逃してしまうような、隠れた危険なバグを見つけ出し、私たちが頼りにしているAIシステムをより安全で信頼できるものにします。