SATBench

SATBench是一个用于评估大型语言模型（LLMs）逻辑推理能力的基准数据集，它通过从布尔可满足性（SAT）问题中派生的逻辑谜题来实现。数据集包含2100个逻辑谜题，每个谜题都从SAT公式生成，然后使用LLMs翻译成故事背景和条件。数据集的生成过程是完全自动化的，并且可以通过改变CNF公式中的子句数量来调整难度。所有谜题都通过LLM辅助和基于求解器的验证来确保质量，其中一部分还进行了人工验证。SATBench揭示了当前LLMs在基于搜索的逻辑推理能力方面的基本局限性，并为未来逻辑推理研究提供了一个可扩展的测试平台。SATBench is a benchmark dataset for evaluating the logical reasoning capabilities of Large Language Models (LLMs). It leverages logical puzzles derived from Boolean Satisfiability (SAT) problems to fulfill this purpose. The dataset comprises 2100 logical puzzles, each generated from a SAT formula and then translated into story contexts and conditions via LLMs. The entire dataset generation pipeline is fully automated, and its difficulty can be adjusted by varying the number of clauses in the Conjunctive Normal Form (CNF) formulas. All puzzles are validated for quality through LLM-assisted and solver-based methods, with a subset also undergoing manual verification. SATBench reveals the fundamental limitations of current LLMs in search-based logical reasoning, and provides a scalable testbed for future research on logical reasoning.

原始信息汇总

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

基本信息

• 标题: SATBench: Benchmarking LLMs Logical Reasoning via Automated Puzzle Generation from SAT Formulas
• arXiv标识符: arXiv:2505.14615v1
• 提交日期: 2025年5月20日
• 作者: Anjiang Wei, Yuheng Wu, Yingjia Wan, Tarun Suresh, Huanmi Tan, Zhanke Zhou, Sanmi Koyejo, Ke Wang, Alex Aiken
• 领域: 计算机科学 > 人工智能 (cs.AI)
• DOI: https://doi.org/10.48550/arXiv.2505.14615

摘要

SATBench是一个用于评估大型语言模型（LLMs）逻辑推理能力的基准测试，通过从布尔可满足性（SAT）问题中生成的逻辑谜题进行评估。与之前专注于基于推理规则的推理工作不同，SATBench利用SAT问题的搜索性质，目标是找到满足一组逻辑约束的解决方案。每个SATBench实例均从SAT公式生成，然后通过LLMs转换为故事背景和条件。生成过程完全自动化，并可通过调整子句数量调整难度。所有2100个谜题均通过LLM辅助和基于求解器的一致性检查进行验证，并对子集进行人工验证。实验结果表明，即使是最强的模型o4-mini，在困难的UNSAT问题上也仅达到65.0%的准确率，接近随机基线的50%。SATBench揭示了当前LLMs在基于搜索的逻辑推理能力上的根本局限性，并为未来逻辑推理研究提供了一个可扩展的测试平台。

主题分类

• 人工智能 (cs.AI)
• 计算与语言 (cs.CL)
• 机器学习 (cs.LG)
• 计算机科学中的逻辑 (cs.LO)

相关链接

• PDF: http://arxiv.org/pdf/2505.14615v1
• TeX源码: http://arxiv.org/format/2505.14615v1

搜集汇总

数据集介绍

构建方式

SATBench数据集通过自动化流程从布尔可满足性（SAT）问题中生成逻辑谜题，构建过程分为三个阶段：SAT公式采样、基于大型语言模型（LLM）的故事生成以及一致性验证。首先，从合取范式（CNF）中采样SAT公式，通过调整子句数量控制问题难度；随后，利用LLM将公式变量映射到故事背景中的实体，并将每个子句转化为自然语言条件；最后，通过LLM辅助和基于求解器的双重验证确保谜题逻辑一致性，并对生成过程进行人工抽样验证。

特点

SATBench的核心特点在于其专注于搜索式逻辑推理任务，通过SAT问题生成多样化的逻辑谜题。数据集包含2100个实例，难度可动态调整（子句数4-50），并区分可满足（SAT）与不可满足（UNSAT）问题类型。其创新性体现在完全自动化的生成流程、自然语言表述的模板无关性设计，以及通过求解器验证的答案可靠性。特别地，UNSAT类问题能够有效检验模型穷举搜索能力，而多阶段验证机制（LLM辅助、求解器核对及人工抽查）确保了数据质量。

使用方法

使用SATBench时，研究者可通过零样本提示（zero-shot prompting）评估模型在逻辑推理任务上的表现。每个谜题包含故事背景、自然语言条件及可满足性查询问题，模型需输出SAT/UNSAT判断并生成推理轨迹。评估指标包括预测准确率和推理轨迹有效性，后者通过LLM-as-a-judge策略验证。对于SAT实例需检查变量赋值合理性，UNSAT实例则需分析矛盾推导过程。该数据集支持对模型在搜索空间复杂度、约束条件处理等方面的细粒度分析。

背景与挑战

背景概述

SATBench是由斯坦福大学、UCLA、UIUC、CMU及Visa Research等机构的研究团队于2025年提出的逻辑推理基准数据集，旨在通过布尔可满足性问题（SAT）衍生的逻辑谜题评估大语言模型（LLM）的搜索式推理能力。该数据集包含2100个自动化生成的逻辑谜题，其核心创新在于将CNF公式转化为自然语言叙述，并通过调整子句数量实现难度控制。相较于传统基于推理规则的逻辑评估（如FOLIO、RuleTaker），SATBench首次系统性地将NP完全问题的求解范式引入LLM能力评估，揭示了现有模型在穷举搜索类任务中的显著缺陷——顶尖模型o4-mini在困难UNSAT问题上仅达65%准确率。

当前挑战

SATBench面临双重挑战：在领域问题层面，其需解决LLM对搜索式逻辑推理（特别是UNSAT问题）的固有缺陷，这类问题要求模型遍历指数级解空间验证不可满足性，而当前模型表现接近随机基线；在构建层面，自动化生成过程需攻克逻辑一致性验证难题，研究团队通过LLM辅助与求解器双重校验机制确保CNF公式与自然语言条件的双向可逆转换，但变量映射的语义保真度与复杂子句的语境化表达仍存在约3%的人工修正率。此外，推理轨迹评估中暴露的SAT/UNSAT不对称性（模型对可满足问题的解验证可靠性显著低于不可满足问题）也构成了新的研究挑战。

常用场景

经典使用场景

SATBench作为评估大语言模型（LLM）逻辑推理能力的基准工具，其经典使用场景在于通过自动生成的布尔可满足性（SAT）问题衍生的逻辑谜题，系统性地测试模型在搜索式逻辑推理中的表现。研究者通过调整子句数量控制谜题难度，构建从简单到复杂的任务梯度，从而精确量化模型在解决SAT与UNSAT问题时的性能差异。该数据集尤其擅长揭示模型在需穷举搜索的UNSAT问题上的薄弱环节，为逻辑推理研究提供了标准化测试环境。

实际应用

在实际应用中，SATBench的自动化生成框架可快速构建定制化逻辑评估系统。教育领域可基于其调整子句数量生成阶梯式训练题库，提升学生的形式逻辑能力；AI产业界则能通过该基准筛选具备强逻辑推理能力的LLM，优化智能客服、自动定理证明等场景的解决方案。其故事化的问题呈现方式尤其适用于需要自然语言交互的AI系统测试，为产品逻辑可靠性提供验证标准。

衍生相关工作

SATBench的发布催生了多项探索LLM逻辑推理边界的衍生研究。例如，DeepSeek-R1通过强化学习在SATBench上实现76.2%的推理轨迹准确率，验证了改进模型可解释性的可能路径；ZebraLogic等后续工作借鉴其搜索式推理评估范式，进一步扩展至谓词逻辑领域。这些研究共同构成了当前LLM形式化推理评估的方法体系，推动着从布尔逻辑到高阶逻辑的系统性能力测评。