Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability
作者: Leizhen Zhang, Shuhan Chen, Sheng Chen
分类: cs.AI, cs.CL, cs.LO
发布日期: 2026-05-27
备注: Accepted at the ACM International Conference on the Foundations of Software Engineering (FSE 2026)
💡 一句话要点
提出基于配对公式和ADR的评估方法，更可靠地评估LLM在SAT问题上的推理能力
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大型语言模型 可满足性问题 推理能力评估 配对公式 准确区分率
📋 核心要点
- 现有方法在评估LLM的SAT问题推理能力时，传统指标（如准确率）存在误导性，无法准确反映模型真实性能。
- 提出一种基于配对公式的评估协议和准确区分率（ADR）指标，通过区分细微差异的SAT实例来更准确地评估LLM的推理能力。
- 实验表明，ADR能有效区分基于推理和基于启发式的模型，且与witness有效性相关，并验证了模型在不同表征下决策的一致性。
📝 摘要（中文）
大型语言模型（LLM）越来越多地用于隐式地归结为布尔可满足性（SAT）的任务，但它们在SAT上的推理能力仍不清楚。本文针对2-SAT和3-SAT，以及两个典型的归约问题：顶点覆盖和离散3D packing，对LLM进行了系统的研究，以探究表征不变的推理能力。首先使用传统指标（包括准确率、精确率、召回率和F1）以及SAT相变设置来评估模型。研究发现这些指标可能具有误导性：许多模型通过过度预测可满足公式来获得高分，未能重现3-SAT阈值附近的经典易-难-易特征，并且随着变量数量的增加而急剧下降。为了解决这个问题，本文引入了一种基于最小差异的可满足和不可满足实例的配对公式协议，以及准确区分率（ADR），该指标要求每个配对公式的两个成员都被正确分类。ADR将面向推理的模型与启发式模型区分开来，并且与witness有效性相关。除了CNF之外，本文还通过将CNF转换为顶点覆盖，将3-SAT转换为离散3D packing来测试跨表征一致性。大多数模型在CNF以及相应的图或packing实例上的决策在80％以上的实例中一致，表明跨表征的决策规则稳定。总的来说，研究结果表明SAT是LLM推理的保守探针，并且与传统指标相比，使用ADR的配对评估提供了更真实和表征鲁棒的评估。
🔬 方法详解
问题定义：论文旨在解决如何更准确地评估大型语言模型（LLM）在解决布尔可满足性问题（SAT）时的推理能力。现有评估方法，如准确率、精确率等，在SAT问题上容易产生误导，因为模型可能通过简单地预测所有公式都是可满足的来获得高分，而没有真正进行推理。此外，现有方法难以捕捉SAT问题的难度变化，也无法保证模型在不同问题表征下的一致性。
核心思路：论文的核心思路是设计一种更敏感、更可靠的评估方法，能够区分真正具备推理能力的模型和仅依赖启发式规则的模型。为此，论文引入了“配对公式”的概念，即构造一对仅有细微差别的可满足和不可满足的SAT实例，并要求模型能够正确区分它们。同时，提出了“准确区分率”（ADR）作为评估指标，只有当模型正确分类配对公式中的两个实例时，才认为该配对公式被正确解决。
技术框架：论文的评估框架主要包括以下几个步骤：1）生成SAT公式：生成2-SAT和3-SAT公式，并控制变量数量和子句数量。2）构建配对公式：对于每个SAT公式，生成一个与其配对的、仅有细微差别的公式，确保一个公式可满足，另一个不可满足。3）模型预测：使用LLM对生成的SAT公式进行预测，判断其是否可满足。4）计算ADR：根据模型对配对公式的预测结果，计算ADR指标。5）跨表征一致性测试：将SAT问题转换为顶点覆盖和3D packing问题，测试模型在不同表征下的决策一致性。
关键创新：论文最重要的技术创新点在于提出了基于配对公式和ADR的评估方法。这种方法能够更有效地捕捉模型在解决SAT问题时的推理能力，避免了传统指标的误导性。ADR指标对模型的推理能力提出了更高的要求，能够区分真正具备推理能力的模型和仅依赖启发式规则的模型。此外，论文还通过跨表征一致性测试，验证了模型在不同问题表征下的决策一致性。
关键设计：配对公式的生成方式是关键设计之一。论文通过修改原始SAT公式中的一个子句来实现配对，确保两个公式仅有细微差别，从而增加了模型区分的难度。ADR的计算方式也很重要，只有当模型正确分类配对公式中的两个实例时，才认为该配对公式被正确解决，这使得ADR对模型的推理能力提出了更高的要求。此外，论文还精心设计了跨表征一致性测试，通过将SAT问题转换为顶点覆盖和3D packing问题，验证了模型在不同问题表征下的决策一致性。
🖼️ 关键图片
📊 实验亮点
实验结果表明，传统评估指标可能高估LLM在SAT问题上的推理能力，而基于配对公式和ADR的评估方法能够更准确地反映模型的真实性能。ADR指标能够有效区分基于推理和基于启发式的模型，且与witness有效性相关。此外，实验还验证了模型在不同问题表征下的决策一致性，表明模型在一定程度上具备跨表征的推理能力。
🎯 应用场景
该研究成果可应用于评估和改进大型语言模型在需要逻辑推理的任务中的性能，例如程序验证、自动规划和知识图谱推理。通过更准确地评估LLM的推理能力，可以更好地利用LLM解决实际问题，并推动LLM在相关领域的应用。
📄 摘要（原文）
Large language models (LLMs) are increasingly used for tasks that implicitly reduce to Boolean satisfiability (SAT), yet their reasoning ability on SAT remains unclear. We present a systematic study of LLMs on 2-SAT and 3-SAT, together with two canonical reductions, Vertex Cover and discrete 3D packing, to probe representation-invariant reasoning. We first evaluate models using conventional metrics, including accuracy, precision, recall, and F1, as well as the SAT phase-transition setting. We find that these metrics can be misleading: many models obtain high scores by over-predicting satisfiable formulas, fail to reproduce the classical easy-hard-easy signature around the 3-SAT threshold, and degrade sharply as the number of variables grows. To address this problem, we introduce a paired-formula protocol based on minimally different satisfiable and unsatisfiable instances, together with Accurate Differentiation Rate (ADR), which requires both members of each pair to be classified correctly. ADR separates reasoning-oriented models from heuristic ones and correlates with witness validity. Beyond CNF, we test cross-representation consistency by converting CNF to Vertex Cover and 3-SAT to discrete 3D packing. Model decisions on CNF and on the corresponding graph or packing instances agree for most models on more than 80 percent of instances, suggesting stable decision rules across representations. Overall, our results show that SAT is a conservative probe for LLM reasoning, and that paired evaluation with ADR provides a more faithful and representation-robust assessment than conventional metrics.