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

逻辑为评估基于 LLM 的推理器提供了受控测试床，但标准 SAT 风格的基准常将表面难度（长度、措辞、子句顺序）与真正决定可满足性的结构现象混为一谈。我们引入一个面向 2-SAT 的诊断基准，它由结构化 2-CNF 公式的参数化族构成，其可满足性由蕴含图刻画，并可沿可解释的轴进行调节。我们的生成器隔离出不同的能力与失败模式：(i) 大小与失衡程度可控的矛盾圈 UNSAT 核；(ii) 以规定比例自由变量控制解多样性的 SAT 实例；(iii) 调节传播过程的植入骨架（planted backbone）；(iv) 将原本单调区域耦合起来、以探测对排序与修订敏感性的后置桥接子句；(v) 在重命名与冗余结构下检验抽象能力的对称/复制变体。我们从决策准确率与赋值有效性两方面评估基于 LLM 的推理器，并在子句重排、填充子句与变量重命名等保语义扰动下量化鲁棒性。在各模型上，我们观察到即使表面统计量保持不变，针对性的结构干预仍会引发剧烈的性能跃变，暴露出总体 SAT 准确率无法察觉的脆弱区间。