SATBench：基于 SAT 公式自动生成的数独基准用于评估 LLM 的逻辑推理能力
人工智能
2025-09-23 v2 计算与语言
机器学习
计算机科学中的逻辑
摘要
我们提出 SATBench，这是一个评估大语言模型 (LLM) 逻辑推理能力的基准测试，通过从布尔满足问题 (SAT) 中派生的逻辑谜题实现。与先前关注基于推理规则的推理（通常涉及从给定前提中推导出结论）的工作不同，我们的方法利用 SAT 问题的搜索本质，即目标是找到满足指定逻辑约束的解。SATBench 中的每个实例都是从 SAT 公式生成的，然后通过 LLM 翻译成谜题。生成过程完全自动化，可通过调整子句数量来调整难度。所有 2100 个谜题都通过了基于 LLM 和求解器的一致性检查，并在子集上进行了人类验证。实验结果表明，即使是最强的模型 o4-mini 在困难的 UNSAT 问题上也仅 achieving 65.0% 的准确率，接近随机基线的 50%。我们的错误分析揭示了系统性失败，如 satisfiability bias、context inconsistency 和 condition omission，凸显了当前 LLM 在搜索-based 逻辑推理中的局限性。我们的代码和数据已公开 available at https://github.com/Anjiang-Wei/SATBench
引用
@article{arxiv.2505.14615,
title = {SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas},
author = {Anjiang Wei and Yuheng Wu and Yingjia Wan and Tarun Suresh and Huanmi Tan and Zhanke Zhou and Sanmi Koyejo and Ke Wang and Alex Aiken},
journal= {arXiv preprint arXiv:2505.14615},
year = {2025}
}