技術要約：同一の論理式、異なる意味論

問題提起

本論文は、様相論理に関する大規模言語モデル（LLM）の推論能力を評価する際の決定的な欠落に対処している。既存のベンチマーク（例：ProofWriter、FOLIO、LogicNLI）は、固定された暗黙的な背景論理の下での演繹を評価しているが、明示的に述べられた意味論的仕様に適応できるかどうかをテストできていない。様相論理において、推論の妥当性は、特定のフレーム特性（例：反射性、推移性、対称性）やドメイン条件（例：定常ドメイン対変動ドメイン）に依存することが多い。モデルは、プロンプトで与えられた特定の制約に従うのではなく、支配的な推論レジーム（「馴染みのある」論理であるS5など）を学習することによって、高い性能を発揮してしまう可能性がある。核心となる問題は、LLMが、規定された（場合によっては非標準的な）意味論的条件に従うために、デフォルトの論理的直感を抑制できるかどうかを判断することである。

手法

著者らは、論理式のパターンマッチングから意味論的な制御を分離するように設計された診断用ベンチマークを構築した。

1. ベンチマークの構築:

• ペア問題: コアとなるデータセットは、前提（$P$）と推論（$C$）は同一であるが、意味論的仕様（$S$）が正確に1つの条件（例：反射的なフレームを推移的なものに、あるいは累積的なドメインを減少するドメインに入れ替えるなど）だけ異なる問題のペアで構成されている。
• オラクルによる検証: 自動推論オラクル（LETエンベディング・ツールチェーンを介したVampireおよびLeo-IIIを使用）を用いて、2つの仕様が同じ論理式に対して逆の真理値（$y_a \neq y_b$）をもたらすことを検証している。
• バランスの取れたコア: モデルが「条件のみ」によるショートカット（条件ラベルのみを見て答えを決定する手法）を利用することを防ぐため、著者らは「バランスの取れた非入れ子コア」として160組のペアを作成した。このサブセットでは、各意味論的条件がTrueとFalseの両方のラベルに対して等しく出現する。ここでの成功は、その条件が論理式を妥当にするかどうかを判断するために、厳密に論理式を読み取ることを要求する。
• 範囲: データセットは、5つのフレーム特性の対比（K–D, K–T, T–B, T–S4, B–S5）と、3つのドメインの対比（変動–累積, 変動–減少, 累積–定常）をカバーしており、合計800組の入れ子構造のシステムペアと160組のバランスの取れたコアを含む。
• プロンプティング: プロンプトは、制御された英語を使用し、従来のシステム名（「S4」のような）を使わずに、ルール（例：「アクセシビリティ関係は反射的かつ対称的である」）を明示的に述べる形式をとっており、モデルが提供されたルールに依存するように強制している。

2. 実験プロトコル:

• モデル: 最近の5つのモデルを評価対象としている：DeepSeek V4 (FlashおよびPro)、GPT-5.6 (LunaおよびTerra)、およびClaude Sonnet 5。
• 条件:
  • 直接プロンプティング: 推論モードを使用しない標準的な推論。
  • 推論モード: 特定のモデル（例：DeepSeek Flashの「high effort」）で有効化し、推論時計算量の増加が意味論への適応を助けるかどうかをテストする。
  • 表現の感受性: 名前付きの英語条件、関係的定義、および形式的なTPTP構文を用いたサブセットテスト。
  • 意味論的親和性: フレーム指定を省略し、制約がない場合にモデルがどの「デフォルト」の論理を好むかを特定する実験。

主な結果

1. 直接プロンプティング下での意味論的制御の失敗:
バランスの取れたコアにおいて、5つのモデルのうち4つが、「条件のみ」のベースライン（モデルが論理式を無視して条件ラベルに基づいて推測すると仮定した場合）を大幅に下回る性能を示した。

• DeepSeek V4 Flash: 厳密なペア精度 4.4%。
• DeepSeek V4 Pro: 2.5%。
• GPT-5.6 Luna: 21.2%。
• GPT-5.6 Terra: 25.0%。
• Claude Sonnet 5: 65.0%（ベースラインを超える唯一のモデル）。
  これは、ほとんどのモデルが、プロンプトの制約に関わらず、固定された馴染みのある論理を適用しており、記述された意味論を追跡できていないことを示している。

2. 回復メカニズムとしての推論モード:
推論モードを有効にすると、DeepSeek V4 Flashの性能が劇的に向上し、バランスの取れたコアにおける精度が4.4%から**88.1%**へと上昇した。同様の向上が、フレーム問題におけるGPT-5.6 Lunaでも観察された。これは、失敗の本質が必ずしも論理的知識の欠如ではなく、特定の制約を処理するための正しい推論モードを起動できていないことにあることを示唆している。

3. 意味論的親和性とデフォルト:
仕様が省略された場合、モデルは馴染みのある論理との一貫した親和性を示した（例：DeepSeek FlashはKを好み、SonnetもKを好み、他はTを好む）。しかし、これらのデフォルトは、明示的な制約が存在する場合のエラーを信頼性高く予測するものではなかった。モデルは、指定が不十分な問題には一致することもあるが、制約が追加された際に調整することに失敗することが多い。

4. 表現の感受性:
入力形式（名前付きの条件から、関係的定義やTPTPへ）を変更すると、性能の順位は変わるものの、意味論的制御を一貫して回復させることはなかった。例えば、GPT-5.6 Terraの精度は、名前付きの38%から関係的定義の6%へと低下しており、表面的なフォーマットの変更は、根本的な意味論的適応の問題に対する単純な解決策ではないことを示している。

主な貢献

• 診断用ベンチマーク: オブジェクトレベルの問題を固定したまま、意味論的仕様を変化させることで、「仕様への感受性」をテストするために特別に設計された制御された評価フレームワークの導入。
• バランスの取れたコア: 意味論的条件を回答にマッピングすることで、論理式を読まずに問題を解く可能性を排除する、新しいデータセット設計。
• モード依存性の実証的証拠: 推論モード（直接 vs 推論）が様相意味論に従う能力に強く依存していることを示し、LLMにおける静的な論理推論能力という概念に疑問を投げかける。
• リソースの公開: 論理式、オラクル生成物、反例、およびモデルの応答の公開。

意義と主張

本論文は、固定された意味論のベンチマークは、LLMの推論の堅牢性を過大評価している可能性があると論じている。主要な発見は、様相的知識（論理を知っていること）は、意味論的制御（与えられた特定の論理を適用すること）とは別物であるということである。モデルは必要な論理規則を備えているかもしれないが、ローカルな仕様が自身の回答を支配することを許容できず、代わりに馴染みのある推論レジームをデフォルトとして使用してしまう。

著者らは、自らの研究がこれら2つの能力を分離していると控えめに主張している。彼らは、推論モードが意味論的介入への感受性を回復させることはできるものの、中間的な導出ステップ（例：モデルは論理の切り替えには成功しても、推論エラーのために誤った結論を導き出す可能性がある）の正当性を保証するものではないと指摘している。本研究は、将来の評価においては、固定された背景の仮定に頼るのではなく、記述された制約に適応できるかどうかを明示的にテストする必要があると結論付けている。本論文は、新しいアプリケーションや将来のアーキテクチャの変更を提案するものではなく、現在のモデルの診断的評価にのみ焦点を当てている。