【第 4 回】AI のハルシネーションとの戦い — 自分で書いた変異は、自分が思いつく壊し方しか試せない

形式検証とテストで安心しきるのは危険だ、という話である。データベースに列を追加する操作が既存データを壊さないか判定する述語を書いた時のこと。実装の欠陥を探す「ミューテーション」（実装を意図的に壊す）を3つ用意して、証明（proof）が全て落ちることを確認した。安心した。ところが後から、機械的にミューテーションを走査した監査役が「何も返さない実装」を試したら、証明が全部通ってしまった。単体テストは引っかかったのに、形式検証だけが通った。

理由は、証明が片方向の含意しか言っていなかったからだ。「Some（結果）を返したなら、その中身は正しい」と書いたが、「そもそも Some を返すべき時に返しているか」は誰も述べていない。だから何も返さない実装は全て通る。そして最初に用意した3つのミューテーションは、いずれも「間違った答えを返す」パターンだった。「答えを返さない」パターンが試されていない。つまり実装役が想像できた「壊れ方」の型が1種類しかなかったということだ。

この盲点は同じ形で複数回繰り返された。全称（すべて）と存在（どれか一つ）の区別が1要素のテストでは消えるために、.all() と .any() の入れ違いを見逃した。2度踏んだ。認可ロールが単一の変数に置かれていたために、複数の役割源がある実装では最後の代入が勝つバグが、単一源のテストでは見えなかった。「自分で書いた変異は、自分が思いつく壊し方しか試せない」—これが本質である。安全方向だけを守る検証は、安全方向だけを壊す欠陥と相性がよく、両方揃うと何も検出しない組み合わせになる。

AI の鬼の視点はここだ。検証層を重ねるなら、欠陥の「型」を複数用意せねばならない。反対方向の検証も必要だ。要素をまたいで共有される可変状態があるか、正当な入力は必ず受理される側の proof を対にする、「答えを返さない」パターンも試す。こうした「自分が思いつかない壊し方」を組織的に試せる構造を作らないかぎり、検証は安心の錯覚に過ぎない。中小企業では形式検証までやることは稀だが、同じ原理は単体テストや統合テストにも当てはまる。自社ツール開発で「テストは全部通った」と言う時、その通った内容がどの型の欠陥を試しているのか、試していないのかを言語化する癖をつけると、バグ摘発の精度が急に上がる。