以配对SAT实例检验语言模型的推理能力

大语言模型（LLM）越来越多地被用于那些在隐含层面可归约为布尔可满足性（SAT）的任务，但它们在SAT上的推理能力仍不清楚。我们对LLM在2-SAT和3-SAT上的表现进行了系统研究，并结合两种经典归约——Vertex Cover和离散3D装箱——来探究表示不变的推理能力。我们首先使用常规指标（包括准确率、精确率、召回率和F1）以及SAT相变设定对模型进行评估。我们发现这些指标可能具有误导性：许多模型通过过度预测可满足公式而获得高分，未能复现3-SAT阈值附近经典的“易—难—易”特征，且随着变量数量增长性能急剧下降。为解决这一问题，我们提出了一种基于最小差异的可满足与不可满足实例的成对公式协议，并引入精确区分率（Accurate Differentiation Rate，ADR），该指标要求每一对中的两个成员都被正确分类。ADR能够将面向推理的模型与启发式模型区分开来，并与见证有效性（witness validity）相关。除CNF之外，我们通过将CNF转换为Vertex Cover、将3-SAT转换为离散3D装箱来测试跨表示一致性。对于大多数模型而言，模型在CNF上的决策与在对应图或装箱实例上的决策在超过80%的实例上一致，这表明其决策规则在不同表示之间是稳定的。总体而言，我们的结果表明SAT是探测LLM推理的一种保守手段，而基于配对评估与ADR的方法比常规指标提供了更忠实、对表示更鲁棒的评估。