本記事は Zenn にも同内容を公開している: https://zenn.dev/flip451/articles/sotohe-semantic-gate
プログラムの正しさには、シンタックス(構文)とセマンティクス(意味論)の両面がある。構文の検証は機械の得意分野で、コンパイラや lint が昔から黙って引き受けてきた。一方、意味論の検証——この仕様は設計の意図と矛盾していないか、このコードをレビューして指摘すべき所見はないか——は、長らく人間のレビューに頼るほかなかった。そして人間のレビューは、高価で、再現せず、属人的だ。
LLM の登場が、この分担を変えつつある。自然言語とコードをまたいで意味を読める判定器が、機械の側に現れたからだ。意味論の検証から属人性を排除しつつ、自動化できるようになったのだ。
ただし LLM の判定は非決定的で、同じ入力に同じ答えを返す保証がない。そのままゲートに置けば、信頼できない門番になる。本稿では、LLM の判定を規律で縛って CI ゲートに耐えるものにする方法を扱う。扱う規律は以下の 5 つである。
- 引用義務
- hash とキャッシュ
- 検出精度の検査
- 段階エスカレーション
- fail-closed な適用範囲
考え方自体は判定の対象を選ばない。
筆者の作成しているハーネス(SoTOHE)では、
- コード差分に対する「レビュー指摘ゼロ」のゲート(第 2 回で紹介)
- 引用・参照の意味論検証のレーン
- 書くべきテストが書かれているかを問うテスト義務ゲート(第 5 回で扱う)
と複数の LLM 判定ゲートがある。本稿では、規律が最も濃く現れる引用・参照の意味論検証を主例に取る。
これは SoTOHE 紹介シリーズの第 4 回である。
第 1 回で SoT Chain(「ADR ← 仕様書 ← 型契約 ← 実装」を一方向の参照で結ぶチェーン)の全体像を、第 2 回で track ワークフローを、第 3 回で型契約書 (TDDD) を扱った1。
シリーズ全体の地図は記事末尾に置いた。
参照や引用の整合性の 4 つの評価軸
文書やプログラムの断片から、より上流のドキュメントへの参照・引用(たとえばプログラム中の関数から設計書内の一文への参照)について考える。このとき、下流が上流を適切に参照できているかを評価する軸は、次の 4 つである。
- ① 参照が存在するか
- ② 参照先が実在するか
- ③ 参照先が主張を本当に裏付けているか
- ④ ①〜③ の検証結果が古くなっていないか
この 4 つに、それぞれ名前を与えておく。
- 存在信号(①):下流が上流への参照を引用しているか(例:仕様の各要件が設計判断への参照を持つか、型契約書の各型宣言が仕様への参照を持つか2)
- 構造(②):引用先が実在するか(例:引用に書かれた参照先が ADR 側に実在するか)
- 意味論(③):引用先が主張を実際に裏付けているか
- 鮮度(④):検証の結果が、いま見てもまだ有効か
ここで注意しておきたいことがある。層① と層② の検証は、機械的に行うことができる。しかし、① と ② の合格は「引用が存在し、参照先も実在する」を意味するだけで、参照先が主張を意味的に裏付けているかは何も言っていない。仕様書が設計判断の一つを引用し、しかしその決定を否定する内容を書いていても、① と ② は素通しになる。例えば設計判断が「設定ファイルの欠落は起動エラーにする」と決めているのに、仕様書がそれを引用しながら「欠落時は既定値で継続する」と書いてしまう、というような食い違いがありうる。
意味論検証を LLM に委ねる
このような意味論的な食い違いを防止する検証(層③)は、従来、人間のレビューに委ねられていた。だが人間のレビューは高価で、しかも再現しない。同じ差分を二度レビューしても同じ結論が出る保証はなく、忙しいフローの中では実質的に素通りになりがちだ。
そこで、ここに LLM の判定を持ち込むことを考えてみよう。何が課題になるだろうか。ざっと挙げるだけでも、次のようなものがある。
- LLM も人間と同じで非決定的(確率的)
- 実際に意味を検証せずに LGTM してくる可能性がある(とくに推論にかける労力を低く設定したモデルで顕著)
- 呼び出しは遅く、高価で、変更のたびにすべての参照を判定し直していてはスケールしない
- モデルの更新やプロンプトの変更で、判定の厳しさが気づかぬうちに緩む
- 何を読ませて判定させたかを固定しないと、判定を再現も監査もできない
これらはどれも、LLM を「信頼できない門番」にする方向に働く。放置したまま CI に置けば、緑になった理由を誰も説明できないゲートができあがる。だから、判定を規律で縛り、その規律を機構として強制する。以降では、筆者の実装がこれらの課題にどう答えているかを、冒頭に挙げた 5 つの規律に沿って見ていく。
判定の構図: 主張・証拠・判定結果
筆者の実装では、意味論の検証(③)を独立した意味論レーンとして持ち、その判定を小さな裁判の構図で行う。下流の記述が主張(claim)、上流の記述が証拠(evidence)で、両者を突き合わせて LLM が合否を判定する。合格には証拠の引用が義務づけられ、主張か証拠が変われば判定結果は失効する。
判定が問うのは「主張が証拠の意図や振る舞いと矛盾するか」であって、細部まで証拠に書かれていることではない。上流の文書が struct の全フィールドやメソッドシグネチャまで自然言語で書き切ることは不可能で、そこまで要求すれば設計判断の記録が実装仕様書に変質する。不合格になるのは、矛盾する主張、根拠にない新しい振る舞いの約束、根拠にない新しい設計制約、の 3 類型である。逆に、根拠に明示されていなくても、決定の自然な実装として導ける詳細は不合格にしない。
この判定結果を CI ゲートに耐えさせているのが、冒頭に挙げた 5 つの規律である。
規律 1: 合格に引用を義務づける
LLM に「この仕様は ADR と整合しているか」と聞いて、"LGTM" と返ってきたとしよう。それを何の疑いもなく信じることもできる。だがその返答は、実際には何も検証していないかもしれないし、我々が求めるより浅い意味で「整合している」と言っているだけかもしれない(課題の 2 つ目)。このように、検査対象が黙って検査から漏れて green になることを、サイレントパス (silent pass) と呼ぶ。ゲートの設計で一貫して排除すべき失敗モードである。
そこで、合格判定の際には、根拠のどの箇所 (文や段落) が主張を裏付けるかの引用を必須とする。引用を提示できない合格は「判定保留」として不合格方向に倒す。裸の合格は受け付けない。「何もチェックせず素通り」を構造的に排除するための仕掛けである。
これは人間のレビューでも本来やるべきことだが、人間には強制しづらい。機構として引用フィールドを必須にすることで、初めて一貫して守られる。
規律 2: hash とキャッシュの活用
意味論検証の判定結果は主張と証拠の対、すなわち (claim_hash, evidence_hash) のペアをキーとして凍結される。ここで claim_hash (主張側) は下流ノード、evidence_hash (証拠側) は上流ノードの内容 hash である。たとえば、仕様 → ADR のリンクなら (仕様要素の hash, ADR の hash)、型契約書 → 仕様のリンクなら (型契約書の型宣言の hash, 仕様要素の hash) となる。
主張側と証拠側のどちらかの hash が変われば判定結果は失効し、変わったペアだけが再レビューされる。これが差分キャッシュであり、変わっていないペアは再評価しない。この仕組みにより、時間のかかる意味論検証をやり直す回数を削減できる。
このとき注意すべきは、hash の一致それ自体を「確かめた証拠」として扱わないことだ。hash の再計算は機械的にできてしまうので、その一致は「変更を読んで確かめた」ことを何も保証しない。だから、失効した判定結果の鮮度を回復させる手順は「意味論検証をやり直す」という経路しか用意しない。hash の再計算は、つねに意味論検証とセットで行う。
規律 3: 既知の誤り例を混ぜて、検出精度そのものを検査する
同じ判定器でも、モデルの更新やプロンプトの変化で判定基準は静かに緩みうる。LLM は非決定的で、しかもいつの間にか判定が甘くなることがある。そこで、答えが「不合格」と分かっているペア (既知の誤り例) を各バッチに混ぜて実行し、それらを正しく不合格と判定できているかを監視する(以下、この仕掛けを「精度検査」と呼ぶ)。検出率が閾値を下回れば、判定器が劣化したと判断してエスカレーション経路に入り、判定をより高位のモデルへ引き上げてやり直す(次の規律 4 で扱う)。
なお、精度検査が乗るのは、実際に評価すべき変更があるときだけである。すべてキャッシュで済む実行には、測るべきバッチが無いので精度検査も乗らない。
規律 4: 判定は安い順に三段で行う
検証コストを抑えつつ信頼性を確保するため、判定は安い順の三段で行う。
- 段 1: 軽量モデルで全ペアを並列レビューする
- 段 2: 不合格や判定保留のペア、あるいは精度検査で劣化が疑われたケースを、重量級モデルへ引き上げる
- 段 3: 重量級でも解決しないとき、または判定器の劣化が確認されたときに、人間へ報告する
引き上げの単位は参照ペアである。段 1 で全ペアを評価し、不合格か判定保留になったペアだけを段 2 に上げる。不合格のペアをわざわざ上げ直すのは、軽量モデルの不合格が誤検出かもしれないからだ。不合格が確定すれば、その参照を書いた成果物の書き手に差し戻して修正させることになるが、誤検出でそれをやると手戻りがまるごと無駄になる。だから差し戻しの前に、重量級モデルで確度を確かめる。一方、精度検査による劣化検出が引き金の場合は、差し戻しではなく判定器そのものの点検に向かう。人間は最もコストの高い判定器なので、安価な手段を尽くしてから最後に呼ぶ。
では逆向きの誤り、つまり誤った合格(見逃し)はどうか。こちらは個別には検出できない。その代わり、合格に証拠の引用を義務づけて「根拠に欠ける合格」を出しにくくし(規律 1)、既知の誤り例の検出率で見逃す傾向そのものを監視する(規律 3)。個々の見逃しを拾う仕組みではなく、見逃しやすくなった判定器を検出する仕組みで守っている。
規律 5: fail-closed な適用範囲
この判定器の適用範囲——どの参照・引用を検証の対象に含めるか——は、どう決めるべきだろうか。個々の判定をどれだけ厳しくしても、そもそもゲートに入らない対象は検査されない。サイレントパスの最大の抜け穴は、判定の中身ではなく適用範囲の決め方にある。筆者の実装の答えは、検証ペアの集合を「何を検証するか」の申告からではなく、成果物ファイルの存在から機械的に導出する、である。申告に任せれば、申告漏れがそのまま検査漏れになるからだ。
このとき、「まだ無い」と「あるべきものが欠けている」の区別が要る。仕様書がまだ書かれていない初期状態では、仕様書 → ADR の検証ペアは 0 件で、ゲートは正当に通過する——「整合的な不在」である。だが、仕様書はあるのに引用先の ADR が無いという上下関係の違反や、存在するのに parse できない壊れた成果物は、「欠けている」として必ず止める。不明、欠損、不整合を「通す」のではなく「止める」——この既定を fail-closed と呼び、迂回するためのフラグは用意しない。
なお、判定器の入力にも同じ発想を適用し、機構で封をしている。判定器に渡すのは hash を取った主張と証拠だけで、それ以外のファイルを読むことは、ツールの無効化や読み取り専用サンドボックスで機械的に禁じる。プロンプトの指示で「他を読むな」と頼むのではなく、読めない環境で実行するのだ。こうして「判定器が見たものはすべて hash に写っている」状態を保つことが、hash 凍結(規律 2)の前提を支える。判定器が hash の外の情報を読めるなら、hash が同じでも判定の前提は変わりうるからだ。
コストの正直な話
LLM の判定はタダではない。時間もかかるしお金もかかる。ここは誇張せず正直に書いておく。
コストが実際に発生するのは、初回の実行と、入力が変わったときだけである。差分キャッシュのおかげで、変わっていないペアは再評価されず、すべてキャッシュで済む実行は (精度検査の見送りと合わせて) LLM 呼び出しコスト 0 で完了する。三段の判定も、大半のペアを軽量モデルで捌き、不合格になったものだけを重量級に上げることでコストを抑える。それでも、大きな仕様変更を入れた直後のコミットでは実際にコストが乗る。これはトレードオフであり、隠さない。
得られるのは、「参照は形式として揃っているのに意味的に矛盾している」という、決定論検査では原理的に捕まえられないクラスの不整合を捕まえられること。そして人間のレビューと違い、判定が hash に凍結されて再現し、忙しさの中で素通りしないことだ。意味論の検証を、高価で再現しない人手の作業から、キャッシュの効く決定的なゲートへと変える。これが、引用・参照の意味論検証の狙いである。
SoT Chain の中での位置づけ
最後に、このシリーズが取り扱っている SoTOHE における位置づけについてもふれておこう。SoT Chain の各リンクは 2 系統のゲートで守られている。決定論的な構造信号 (存在信号と参照先の実在チェック) と、LLM による意味論レーンである。前者は「参照が形式として揃っているか」を、後者は「参照が意味として裏付けているか、その確認はいまも有効か」を見る。両者は独立に動き、コミットの最終関門ではコードレビューの承認と意味論側の承認を独立した 2 つのゲートとして AND する。第 2 回で見たレビュー指摘ゼロのゲートに、意味論ゲートがもう一枚重なる形だ。
構造信号側の厳しさ (🟡 をブロックするか警告に留めるか) は、リンク × ゲートの表として専用の設定ファイルに宣言的に書き出される。テンプレート利用者は、この表を自分のワークフローに合わせて編集できる。この config は必須かつ完全で、不在、不正、キー欠落はいずれも hard error になる。厳しさの設定(policy)は利用者が持ち、検証の仕組み(mechanism)はテンプレートが持つ。この policy と mechanism の分離は、SoTOHE 全体を貫く方針の一例である。
意味論レーンは現在、仕様 → ADR と型契約書 → 仕様の 2 リンクに存在する。残る「実装 → 型契約書」のリンクは、TDDD の型シグネチャ突合が構造的な一致を担っている。その意味論版にあたるのが、「宣言された義務に対して、書くべきテストが実際に書かれているか」を問うテスト義務ゲートである。これが最新の機能であり、次回 (第 5 回) で扱う。
シリーズの地図
本稿は 📍 の位置、チェーンの参照リンクを意味論で検査するゲートの回である。
シリーズ一覧
- AI エージェントに「仕様どおり」を保証させる — SoT Chain という設計
- ADR から PR まで自走する track ワークフローとマルチエージェント分業
- 型契約書を SSoT にする — TDDD(型定義駆動開発)
- LLM による意味論検証を支える規律 〜参照整合性への応用例を添えて〜(本記事)
- LLM が書いたテストを信頼する方法 — テスト義務ゲート
- SoTOHE を使い始める — テンプレート export と新規プロジェクト実走記録(公開予定)
- SoTOHE を支える設計原則(公開予定)
リポジトリ: https://github.com/Flip451/SoTOHE-core