用自动生成的逻辑谜题测试大模型的搜索式推理能力
SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas
- 从布尔可满足性问题自动生成逻辑谜题
- 最强模型在难题上准确率仅65.0%，接近随机水平
- 适合评估模型在复杂逻辑搜索任务中的真实能力
我们提出SATBench，一个通过从布尔可满足性（SAT）问题衍生的逻辑谜题来评估大语言模型（LLMs）逻辑推理能力的基准。与以往侧重于基于推理规则的演绎推理不同，本方法利用SAT问题的搜索特性——目标是找到满足一组逻辑约束的解。每个SATBench实例由SAT公式生成，并经由大模型转换为谜题，整个过程完全自动化，可通过调整子句数量调节难度。所有2100个谜题均通过大模型和求解器双重一致性验证，部分经人工校验。实验结果表明，即使最强模型o4-mini在困难的非可满足（UNSAT）问题上也仅达65.0%准确率，接近50%随机基线。错误分析揭示了模型存在可满足性偏差、上下文不一致和条件遗漏等系统性缺陷，凸显当前大模型在搜索式逻辑推理中的局限性。代码与数据已公开于https://github.com/Anjiang-Wei/SATBench。
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。