論文「Reducing Hallucinations in LLM-Generated Code via Semantic Triangulation」の技術的サマリー

本論文は、大規模言語モデル（LLM）が自然言語記述から生成するコードにおける「幻覚（hallucination）」、すなわちバグや脆弱性の混入を低減するための新しい理論的枠組み**「セマンティック・トライアングレーション（Semantic Triangulation）」**を提案する研究です。

以下に、問題定義、手法、主要な貢献、実験結果、および意義について詳細をまとめます。

---

1. 背景と問題定義

1.1 背景

LLM は自然言語仕様から実行可能なコードを生成できますが、生成されたプログラムには頻繁にバグが含まれます。特に「vibe coding（感覚的なコーディング）」の流行により、開発者が生成コードを十分にレビューせず、ブラックボックス状態で利用するケースが増えています。

1.2 既存手法の限界

コードの正しさを評価する既存のアプローチには以下のようなものがありますが、それぞれに重大な欠点があります。

• 多数決（Plurality Voting）: 生成された複数のコードから最も頻出するものを選択します。しかし、LLM は**相関したエラー（correlated errors）**を起こす傾向があるため、間違ったコードが多数派になることが多く、誤った結論を強化してしまいます。
• 生成されたテストや仕様による検証: LLM 自身で生成したテストケースや自動形式仕様（Hoare 論理など）を用いて検証します。しかし、これらも同じ不完全なモデルによって生成されるため、**「同じ欠陥を持つ証人」**として機能し、誤ったコードを正当化（corroborate）してしまうリスクがあります。
• メタモルフィック・テスト（言い換え）: 問題文を言い換えて一貫性をチェックしますが、LLM は微細な変化に対して頑健であるため、同じ誤った回答を返す傾向があり、検出が困難です。

核心的な課題: 既存の「証人（plausibility witnesses）」は、元のコードと相関したエラーを起こしやすく、真実を見極めることができません。

---

2. 提案手法：セマンティック・トライアングレーション

本論文は、探偵が嘘つきを暴くために「予期せぬ角度」から問い質すように、**「相関を断ち切る（dissociative）」**問題変換を用いた新しい枠組みを提案します。

2.1 基本的な考え方

元のコーディング課題 $d$ を、本質的に異なるアルゴリズムを必要とする「分離された変種（dissociative variant）」$d'$ に変換します。その後、$d$ と $d'$ の両方に対して独立して生成されたソリューションの間で、**一貫性（consistency）**をチェックします。

• 正しいコード: 真実を反映しているため、変換された問題に対する回答とも整合性が取れます。
• 幻覚（バグ）を含むコード: 異なるアルゴリズムを要求されるため、変換された問題に対する回答と矛盾を露呈させます。

2.2 理論的基盤

この枠組みは、以下の 2 つの数学的性質を満たす変換と述語（ハイパープロパティ）$\phi$ で構成されます。

1. 双射誘発性（Bijection-inducing）: 元の問題のプログラムの等価クラスと、変換された問題のプログラムの等価クラスの間に一対一対応が存在すること。これにより、異なるエラーが一致する確率が低くなります。
2. 正しさの結合（Correctness-coupling）: その対応関係が正しさを保存すること（正しい解は正しい解に対応する）。

理論的保証: LLM の幻覚を「確率的オウム（stochastic parrot）」としてモデル化し、相関したエラーが存在すると仮定した場合、適切に設計されたトライアングレーションは、単純な多数決よりも正解を選択する確率を数学的に向上させることが証明されています（並べ替え不等式に基づく証明）。

2.3 具体的な実装手法（4 つのメソッド）

ツール just-tri-it として実装され、以下の 4 つの変換手法が提案されています。これらはすべて Lean による機械検証済みです。

1. FWD-INV（完全逆問題）: 入出力を逆転させた問題を解く（例：「出力から入力を求める」）。
2. FWD-SINV（部分集合値逆問題）: 特定の出力に対して、それを生成する可能性のあるすべての入力を列挙する問題を解く。これは「不正確な問題（複数の正解が存在する）」に対処するために重要です。
3. ENUM-SINV（答えの列挙と逆問題の組み合わせ）:
   • 元の課題 $d$ の正解候補を、**「すべての正解を列挙するプログラム（Enumerator）」と「逆問題を解くプログラム」**の両方と照合します。
   • これにより、不正確な問題（複数の正解がある場合）でも、エラーを相関させずに正解を選別できます。
4. STREAM（ストリーム処理の分解）: ストリーム処理タスクを、要素ごとの点処理タスクに分解してトライアングレーションを行います。

---

3. 実験評価

3.1 評価設定

• データセット: LiveCodeBench（最新セグメント、175 問）および CodeElo-Inexact（不正確な問題 31 問）。
• モデル: GPT-4o, DeepSeek-V3, Gemini 2.5 Flash。
• ベースライン: 多数決（Plurality）、生成テスト（CodeT）、自動形式仕様（Hoare 論理）、メタモルフィック・テスト（言い換え、OffByOne）。

3.2 主要な結果

1. 正解確率の向上:

   • トライアングレーションは、ベースライン（テスト生成や自動仕様など）と比較して、正解プログラムを選択する確率を平均 24% 向上させました。
   • 正解のサンプリング確率が低い（例：0.07）場合でも、信頼性を維持して正解を選別できました。

2. 選択・棄権（Selection-or-Abstention）の性能:

   • 「自信がなければ回答を棄権する」シナリオにおいて、棄権 F1 スコアが 26% 向上しました。
   • 従来の「確率 0.5 以上のみを選択」する手法（Majority0.5）と比較して、信頼性（Reliable Accuracy）が 8% 高い結果となりました。

3. 不正確な問題（Inexact Problems）への対応:

   • 複数の正解が存在する問題において、既存手法は失敗しましたが、just-tri-it は一貫して高い性能を示しました。これは、ENUM-SINV などの手法が不正確な問題に対処できる唯一の手法であることを示しています。

4. 失敗分析:

   • 失敗の主な原因は「偽陰性（棄権の増加）」であり、変換後の問題が難しすぎたり、情報欠落があったりすることによるものでした。
   • 「偽陽性（誤ったコードの選択）」は 34% であり、その多くは変換された問題と元の問題で相関したエラーが発生した場合でした。

5. コスト:

   • トライアングレーションは、単純な多数決に比べてトークン数が約 4.9 倍、実行時間が約 2.5 倍増加しますが、信頼性の向上と引き換えに許容可能な範囲とされています。

---

4. 主要な貢献

1. セマンティック・トライアングレーションの提案:
   LLM 生成コードの信頼性を高めるための、理論的に裏付けられた新しいハルシネーション検出フレームワーク。
2. 実用的な実装と形式検証:
   逆問題、答えの列挙、問題分解に基づく 4 つの具体的な手法を提案し、その設計が理論的要請（双射性など）を満たすことを Lean による機械検証で証明しました。
3. 不正確な問題への対応:
   既存手法が苦手とする「複数の正解が存在する問題」において、唯一一貫して機能する手法であることを実証しました。
4. 理論と実証の統合:
   LLM の幻覚を数学的にモデル化し、なぜトライアングレーションが有効なのか（相関エラーの低減）を理論的に証明すると同時に、大規模ベンチマークでその有効性を示しました。

---

5. 意義と結論

本論文は、LLM によるコード生成の信頼性向上において、単なる「多数決」や「同じモデルによる検証」の限界を突破する重要なステップです。

• 理論的意義: LLM のエラーが相関しているという性質を逆手に取り、**「異なるアルゴリズムを要求する変換」**によってエラーを非相関化し、真実を浮き彫りにするという新しいアプローチを確立しました。
• 実用的意義: 難易度の高い課題や、仕様があいまいな（不正確な）タスクにおいても、LLM が生成したコードから信頼性の高いものを選別できるツールを提供します。
• 将来的展望: この枠組みは、形式検証やメタモルフィック・テストの限界を補完し、より堅牢な AI 支援開発（AI-assisted development）の実現に寄与すると考えられます。

要約すれば、**「同じモデルに同じ質問を繰り返すのではなく、本質的に異なる角度から問い質すことで、LLM の嘘（バグ）を見抜く」**という、探偵的なアプローチを理論的に体系化した画期的な研究です。