评估参数化逻辑问题上推理模型的鲁棒性

逻辑为基于LLM的推理器提供了一个可控的测试环境，但标准SAT风格基准常常将表面难度（如长度、措辞、子句顺序）与决定可满足性的结构性现象混淆。本文引入了一个用于2-SAT的诊断基准，该基准由参数化的结构化2-CNF公式构建，其中可满足性由蕴含图表征，并可通过可解释的维度进行调整。生成器隔离了不同的能力与失败模式，包括可控大小和不平衡的矛盾循环UNSAT核心、具有预设自由变量比例的SAT实例、调节传播的植入骨干、探测对排序和修订敏感性的晚期桥接子句以及测试重命名和冗余结构下抽象能力的对称/复制变体。我们从决策准确性和赋值有效性两个方面评估基于LLM的推理器，并量化在语义保持扰动（如子句重新排序、填充子句和变量重命名）下的鲁棒性。结果显示，在固定表面统计信息的情况下，针对结构干预的性能出现显著变化，揭示了传统SAT准确率无法发现的脆弱性区域。