SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas

📄 arXiv: 2505.14615v2 📥 PDF

作者: Anjiang Wei, Yuheng Wu, Yingjia Wan, Tarun Suresh, Huanmi Tan, Zhanke Zhou, Sanmi Koyejo, Ke Wang, Alex Aiken

分类: cs.AI, cs.CL, cs.LG, cs.LO

发布日期: 2025-05-20 (更新: 2025-09-22)

🔗 代码/项目: GITHUB

💡 一句话要点

SATBench：通过SAT公式自动生成逻辑谜题，评估LLM的逻辑推理能力

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 逻辑推理 大型语言模型 基准测试 布尔可满足性 SAT问题 自动化谜题生成

📋 核心要点

  1. 现有工作侧重于基于推理规则的逻辑推理，忽略了基于搜索的逻辑推理能力评估。
  2. SATBench利用SAT问题的搜索本质，自动生成逻辑谜题，并调整难度，全面评估LLM的逻辑推理能力。
  3. 实验表明，即使是最强的LLM在困难的UNSAT问题上表现接近随机水平，存在可满足性偏差等问题。

📝 摘要（中文）

本文提出了SATBench，一个用于评估大型语言模型（LLM）逻辑推理能力的基准，它通过源自布尔可满足性（SAT）问题的逻辑谜题实现。与侧重于基于推理规则的推理（通常涉及从一组前提推导结论）的先前工作不同，我们的方法利用了SAT问题的搜索本质，其目标是找到满足指定逻辑约束集的解决方案。SATBench中的每个实例都从一个SAT公式生成，然后使用LLM将其转换为谜题。生成过程是完全自动化的，并且可以通过改变子句的数量来调整难度。所有2100个谜题都通过基于LLM和基于求解器的一致性检查进行验证，并在一个子集上进行人工验证。实验结果表明，即使是最强的模型o4-mini，在困难的UNSAT问题上也仅达到65.0%的准确率，接近50%的随机基线。我们的错误分析揭示了系统性错误，例如可满足性偏差、上下文不一致和条件省略，突出了当前LLM在基于搜索的逻辑推理方面的局限性。我们的代码和数据可在https://github.com/Anjiang-Wei/SATBench公开获取。

🔬 方法详解

问题定义：现有的大型语言模型（LLM）在逻辑推理方面存在不足，尤其是在需要进行搜索的逻辑问题上。以往的基准测试主要集中在基于推理规则的逻辑推理，而忽略了基于搜索的逻辑推理能力。因此，需要一个能够有效评估LLM在解决需要搜索的逻辑问题上的能力的基准。

核心思路：本文的核心思路是利用布尔可满足性（SAT）问题来生成逻辑谜题，并使用这些谜题来评估LLM的逻辑推理能力。SAT问题本质上是一个搜索问题，需要找到满足一组逻辑约束的解。通过将SAT公式转化为自然语言描述的谜题，可以测试LLM理解和解决复杂逻辑约束的能力。这种方法能够更全面地评估LLM的逻辑推理能力，特别是其在搜索问题上的表现。

技术框架：SATBench的整体框架包括以下几个主要阶段：1) SAT公式生成：使用随机SAT公式生成器生成不同难度的SAT公式，难度通过子句数量进行控制。2) 谜题生成：使用LLM将SAT公式转化为自然语言描述的逻辑谜题。3) 谜题验证：使用LLM和SAT求解器对生成的谜题进行一致性检查，确保谜题的逻辑正确性。4) LLM评估：使用不同的LLM来解决生成的谜题，并评估其准确率。5) 错误分析：对LLM的错误进行分析，找出其在逻辑推理方面的局限性。

关键创新：SATBench的关键创新在于：1) 提出了一种基于SAT公式自动生成逻辑谜题的方法，可以灵活控制谜题的难度。2) 构建了一个包含2100个验证过的逻辑谜题的基准数据集，可以用于评估LLM的逻辑推理能力。3) 通过实验和错误分析，揭示了当前LLM在基于搜索的逻辑推理方面的局限性，例如可满足性偏差、上下文不一致和条件省略。

关键设计：在谜题生成阶段，使用了Prompt Engineering来指导LLM生成高质量的自然语言描述的谜题。在谜题验证阶段，同时使用了LLM和SAT求解器进行一致性检查，以确保谜题的逻辑正确性。在实验评估阶段，使用了不同的LLM模型进行对比，并对LLM的错误进行了详细的分析。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，即使是最强的模型o4-mini，在困难的UNSAT问题上也仅达到65.0%的准确率，接近50%的随机基线。这表明当前LLM在基于搜索的逻辑推理方面存在明显的局限性。错误分析揭示了系统性错误，例如可满足性偏差、上下文不一致和条件省略。

🎯 应用场景

SATBench可用于评估和提升LLM在逻辑推理、问题解决和决策制定等方面的能力。该基准可以帮助研究人员更好地理解LLM的优势和局限性，并开发更有效的训练方法和模型架构。此外，SATBench还可以应用于教育领域，用于设计逻辑思维训练工具和评估学生的逻辑推理能力。

📄 摘要（原文）

We introduce SATBench, a benchmark for evaluating the logical reasoning capabilities of large language models (LLMs) through logical puzzles derived from Boolean satisfiability (SAT) problems. Unlike prior work that focuses on inference rule-based reasoning, which often involves deducing conclusions from a set of premises, our approach leverages the search-based nature of SAT problems, where the objective is to find a solution that fulfills a specified set of logical constraints. Each instance in SATBench is generated from a SAT formula, then translated into a puzzle using LLMs. The generation process is fully automated and allows for adjustable difficulty by varying the number of clauses. All 2100 puzzles are validated through both LLM-based and solver-based consistency checks, with human validation on a subset. Experimental results show that even the strongest model, o4-mini, achieves only 65.0% accuracy on hard UNSAT problems, close to the random baseline of 50%. Our error analysis reveals systematic failures such as satisfiability bias, context inconsistency, and condition omission, highlighting limitations of current LLMs in search-based logical reasoning. Our code and data are publicly available at https://github.com/Anjiang-Wei/SATBench