【第 1 回】AI のハルシネーションとの戦い — 形式検証を入れたら、検証器に騙された

AIにコード生成させるとき、ハルシネーション——もっともらしいが違う出力——は故障ではなく、LLMが確率的に「尤もらしい続き」を出す仕様そのものから来る。問題は、コードの場合にはそのもっともらしさが高いことだ。型は合っている、コンパイルは通る、命名は自然で周囲のコードと調和している。こうした形だけ正しいバグはレビューで最も見つけにくい。人間レビュー、テスト、複数モデルの敵対的レビュー——いずれもコストが生成量に比例し、AIに量を書かせる価値と噛み合わない。

著者が選んだのは形式検証だ。Rustで中核ロジックを書き、事前条件と事後条件を式で定義し、機械に検証させる。この「制約駆動開発」のポイントは、AIに従うべきルールを先に決めることである。日本語は曖昧で、LLMは曖昧なところを質問せず勝手に補う。その補った内容は記録に残らない。仕様を厳密な言語で書こうとしたが、LLMの学習量不足で実用にならず、最終的には日本語のまま仕様を書き、守るべき性質だけをRustの式に落とすハイブリッド案に行き着いた。

製造業がシステム開発でAIを使うなら、このモデルが参考になる。曖昧な指示をAIに与えれば曖昧な結果しか出ない。守るべき性質——例えば「在庫は減らない」「日付は昇順」——をあらかじめ決め、AIはそれを満たす実装を書く、機械がそれを検証する。この構造なら、AIの出力に対する信頼度が格段に上がる。