技术摘要：相同的公式，不同的语义

问题陈述

本文探讨了评估大语言模型（LLM）在模态逻辑方面推理能力的一个关键空白。现有的基准测试（如 ProofWriter、FOLIO、LogicNLI）虽然评估了在固定且隐式背景逻辑下的演绎能力，但未能测试模型是否能够根据显式说明的语义规范来调整其推理过程。在模态逻辑中，推论的有效性往往取决于特定的框架属性（例如自反性、传递性、对称性）或领域条件（例如常数域与变动域）。模型表现出色，可能是因为它学习了一种占主导地位的推理机制（如一种“熟悉的”逻辑 S5），而不是遵循提示词中提供的特定约束。核心问题在于：模型能否抑制其默认的逻辑直觉，转而遵循所规定的、可能并非标准的语义条件。

方法论

作者构建了一个诊断性基准测试，旨在将语义控制从公式模式匹配中分离出来。

1. 基准构建：

• 配对问题： 核心数据集由成对的问题组成，其中前提（$P$）和结论（$C$）完全相同，但语义规范（$S$）仅有一个条件的差异（例如，将一个自反框架替换为传递框架，或将一个累积域替换为递减域）。
• 预言机验证： 使用自动化推理预言机（通过 LET 嵌入工具链使用 Vampire 和 Leo-III）来验证这两个规范是否会导致相反的真值（$y_a \neq y_b$）。
• 平衡核心： 为了防止模型利用“仅靠条件”的捷径（即答案仅由语义标签决定，而不阅读公式），作者创建了一个包含 160 个配对的“平衡非嵌套核心”。在这个子集中，每种语义条件在 True 和 False 标签中出现的频率相等。在此处的成功严格要求模型必须阅读公式以确定哪种条件使其成立。
• 范围： 数据集涵盖了五种框架属性对比（K–D、K–T、T–B、T–S4、B–S5）和三种领域对比（变动–累积、变动–递减、累积–常数），总计 800 个嵌套系统配对和 160 个平衡核心配对。
• 提示词设计： 提示词使用受控的英语来显式说明规则（例如，“该可达关系是自反且对称的”），而不使用传统的系统名称（如“S4”），从而迫使模型依赖于提供的规则。

2. 实验方案：

• 模型： 研究评估了五种最新的模型：DeepSeek V4 (Flash 和 Pro)、GPT-5.6 (Luna 和 Terra) 以及 Claude Sonnet 5。
• 条件：
  • 直接提示（Direct Prompting）： 标准推理，不开启推理模式。
  • 推理模式（Reasoning Mode）： 为特定模型启用（例如 DeepSeek Flash 的“高强度计算”），以测试增加推理时计算量是否有助于提升语义遵循能力。
  • 表示敏感性（Representation Sensitivity）： 一个子集测试了在命名英语条件、关系定义以及形式化 TPTP 语法下的表现。
  • 语义亲和力（Semantic Affinity）： 通过省略框架规范进行实验，以识别模型在不受约束时倾向于哪种“默认”逻辑。

关键结果

1. 直接提示下的语义控制失效：
在平衡核心测试中，五个模型中有四个的表现显著低于 50% 的“仅靠条件”基准线（该基准假设模型忽略公式并根据条件标签进行猜测）。

• 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 推理的鲁棒性。主要发现是：模态知识（了解逻辑）与语义控制（应用给定的特定逻辑）是截然不同的。 模型可能拥有必要的逻辑规则，但无法让局部规范主导其答案，而是退回到一种熟悉的推理机制。

作者对自己的工作提出了适度的主张。他们指出，虽然推理模式可以恢复敏感性，但这并不保证中间推导步骤的正确性（例如，模型可能正确切换了逻辑，但仍因推理错误而得出错误的结论）。研究结论是，未来的评估必须明确测试模型是否能够适应所陈述的约束，而非仅仅依赖于固定的背景假设。本文并未提出新的应用或未来的架构变革，而是专注于对当前模型的诊断性评估。