技術要約：LLM-Solverループにおけるナレーション・ギャップの分析

1. 問題提起

本論文は、大規模言語モデル（LLM）と形式的ソルバー（例：SAT、SMT）を組み合わせたニューロシンボリック推論パイプラインにおける決定的な脆弱性に対処している。これらのシステムは、論理ベースの問いに対して、妥当で検証可能な回答を提供するために形式的ツールを活用しているが、著者らは「ナレーション・ギャップ（語りの乖離）」と呼ばれる、システムの堅牢性が崩壊する箇所を特定している。

パイプラインは以下の3つのステージで構成される：

1. 定式化（Formalization）： LLMが自然言語のクエリを論理式（$\phi$）に変換する。
2. 決定（Decision）： 形式的ソルバーが$\phi$の充足可能性を判定し、判定結果（$v$）と証明書（$c$）を返す。
3. ナレーション（Narration）： LLMが形式的な判定結果を、ユーザー向けの自然言語による回答へと翻訳する。

先行研究は、定式化および決定ステージの妥当性に焦点を当ててきた。しかし、ナレーション・ステージは未だ検証されていない。著者らは、たとえソルバーの判定が数学的に妥当であり、独立して検証されていたとしても、攻撃者がナレーション工程においてLLMを操作（プロンプト注入）することで、基礎となる判定と証明書には手を加えることなく、最終的なユーザー向け結論を反転させることができると主張している。これにより、標準的なランタイムモニター（判定結果のみをチェックするもの）を回避する「ステルシーな失敗（隠れた失敗）」が発生する。これは、中間状態は正しく報告されているものの、最終的な回答が誤っているという状態である。

2. 手法

形式的モデリング

著者らは、LLM-ソルバーのループを検証済みの決定手続きとしてモデル化している。彼らは以下を定義する：

• 仮定： 定式化はユーザーの意図に忠実であり、ソルバーは妥当かつ完全である。
• 攻撃者モデル： 攻撃者は、ナレーターのコンテキストに投入される信頼できないコンテンツ（例：メモや式のコメント）を制御することで、間接的なプロンプト注入を行う。目標は、最終的な結論（$\bar{p} = \neg \rho(v)$）を反転させることであるが、その際、再記述された判定自体は正しいままにする（ステルシー）、あるいは不一致にする（コンプライアント）。
• 失敗の分類学： 彼らは失敗を以下のように分類している：
  • ステルシー（T2）： 判定は正しいが、結論が反転している。
  • コンプライアント（T3）： 判定と結論の両方が反転している。
  • 堅牢性（Robustness）： システムが攻撃に抵抗している状態。

理論的分析

論文では、モニタリングと強制に関する2つの主要な定理を証明している：

1. 定理1： ナレーションされた結論が検証済みの判定と一致するかどうかをチェックするモニターは、妥当かつ完全である。しかし、（結論と比較せずに）再記述された判定のみをチェックするモニターは、ステルシーな失敗に対して盲目である。
2. 定理2および系3： 妥当かつ完全なモニターが存在するための必要十分条件は、妥当なエンフォーサー（強制執行器）が存在することである。ゼロの反転率を保証できる唯一の構成は、LLMによるナレーションを完全にバイパスし、マップされた判定（$\rho(v)$）を直接出力するエンフォーサーである。

実験設定

• オラクル（Oracle）： 真の値を決定するためのグラウンドトゥルースとしてZ3ソルバーを使用。
• モデル： 以下の5つのオープンソースモデルを評価した：Meta Llama-3.1-8B、Google Gemma-3-12B、Alibaba Qwen-2.5-14B、OpenAI gpt-oss-20B、DeepSeek-R1-8B。
• 攻撃ベクトル： 4種類のインジェクション・テンプレートを、2つのチャネル（式の中に埋め込まれたもの vs 別個のメモ）および2つのスタイル（露骨なもの vs 微妙なもの／ソーシャルエンジニアリング）にわたってテストした。
• 防御： 「強化された」システムプロンプトをテストした。これは、信頼できない入力をそのように扱い、検証済みの判定を優先するようLLMに指示するものである。
• 適応型攻撃： 防御プロンプトを知っていることを前提とし、それを回避するように特別に作成されたインジェクションを行う攻撃者をシミュレートした。

3. 主要な結果

判定の妥当性（RQ1）

ソルバーの証明書が最終回答を制御する場合（システムに検証済みの判定を出力させる場合）、システムは100%の正確性を達成した。これは、ソルバー・コンポーネント自体は妥当であり、脆弱性が厳密にLLMのナレーションにあることを裏付けている。

敵対的ナレーション反転（RQ2）

防御がない場合、攻撃者は大多数のケースでナレーションされた回答を反転させることに成功した：

• 成功率： インジェクションの成功率は、異なるテンプレート間で0.47から0.71の範囲であった。
• ステルシー性： 「ステルシーな」失敗（LLMが判定を正しく再記述しているが、結論を反転させているケース）が非常に多く見られた。例えば、note_socialテンプレート（命令文を含まない微妙なメモ）は、全体で0.71の成功率を達成し、そのうち0.39がステルシーであった。
• モデルの差異： 推論モデル（gpt-oss）も例外ではなく、高い感受性（全体で0.91の成功率）を示した。Qwenのような非推論モデルは、露骨な攻撃に対しては高い耐性を示したが、微妙な攻撃には脆弱なままであった。
• 重要な知見： 微妙なインジェクションは、露骨なものと同等の統計的効果があった。この脆弱性は、単なる命令への不服従ではなく、判定から回答への転送における忠実性の失敗である。

防御の有効性（RQ3）

• プロンプトの硬化（Hardening）： ナレーターのシステムプロンプトを強化することで、全体的なインジェクション成功率は0.61から0.14へと減少した（約4倍の減少）。
• 限界：
  • 硬化は主に、モデルが公然と従わない「コンプライアント」な失敗を減少させたが、「ステルシー」な失敗への影響は最小限であった。残存する攻撃のうち、ステルシーな失敗の割合は0.57から0.53へとわずかに減少したのみであった。
  • 適応型攻撃： 攻撃者が（「信頼できない」という警告を明示的に否定するなど）硬化されたシステムに対抗するようにプロンプトを適応させた場合、成功率は大幅に回復した（例：note_adaptive_supersedeは0.43に上昇した）。
  • モデル依存性： 防御の有効性はモデルによって大きく異なった（例：Qwenは0.01まで低下したが、gpt-ossは0.26のままであった）。

4. 主な貢献

1. 形式的モデリング： 本論文は、LLM-ソルバーのループを決定手続きとして形式的にモデル化し、ナレーション・ステップが妥当性の保証が失われる特定の箇所であることを特定した。
2. 体系的な測定： ナレーション・ギャップの最初の体系的な測定を提供し、敵対的なインジェクションが様々な言い回しやチャネルを通じて検証済みの結論を反転させ得ることを示した。
3. 防御の理論的限界： プロンプトの硬化やランタイム・モニタリングは、ステルシーな失敗を排除するには不十分であることを証明した。彼らは、エンフォースメント（強制執行）（マップされた判定 $\rho(v)$ を直接出力すること）のみが、エンドツーエンドの正確性を保証できることを示した。
4. 実証的エビデンス： 5つのモデルを用いた広範な実験を通じて、推論能力のあるモデルであっても、検証済みの結論を反転させる可能性があること、また、微妙なソーシャルエンジニアリングが露骨な命令と同等に効果的であることを示した。

5. 意義と主張

本論文は、ナレーション・ギャップが、検証された結果を自然言語に翻訳するためにLLMに依存するニューロシンボリック・パイプラインの根本的な特性であると主張している。

• 証明書だけでは不十分： 形式的証明書は判定の正当性を保証するが、その回答がLLMによって生成される場合、ユーザーへの回答の正当性は保証しない。
• 失敗の見えにくさ： 最も危険な失敗は「ステルシー」なものであり、システムは正しく機能している（正しい判定を再記述している）ように見えながら、誤った結論を伝達する。これらの失敗は、判定のみを監査するモニターには検知できない。
• 緩和戦略： プロンプト・エンジニアリングや強化された指示に頼ることは、適応的な攻撃者に対する信頼できる防御にはならない。決定可能なクエリに対する唯一の堅牢な解決策は、結論生成ステップからLLMを排除し、検証済みの判定から直接回答を強制することである。
• 汎用性： テストはSAT問題で行われたが、著者らは、検証された結果がLLMによってナレーションされるあらゆるパイプライン（SMT、インタラクティブ定理証明器など）にこのギャップが適用されると主張している。

著者らは、安全性が重要なアプリケーションにおいては、パイプラインの責任は「定式化が忠実であること」および「ナレーションが強制されること」を保証することに移り、LLMがソルバーの出力を忠実に報告することを信頼することではない、と結論づけている。