用逻辑验证工具提升大模型推理能力，支持可复现的精细分析。
SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs
- 基于CNF生成多样逻辑题，用PySAT客观验证答案
- 发现高复杂度任务和跨格式迁移中存在显著推理短板
- 强化学习微调后模型性能提升，跨格式鲁棒性仍不足
大语言模型具备强大的通用推理能力，但社区缺乏可控、可扩展且可验证的分析与改进工具。本文提出SATQuest，一种从合取范式（CNF）实例直接生成多样化基于布尔可满足性（SAT）的推理任务，并利用PySAT进行客观答案验证的验证器。SATQuest沿实例、问题类型和问题形式三个正交维度分解评估，实现细粒度的多维分析与强化微调。通过随机化CNF生成，有效缓解记忆化问题，支持可复现实验。我们使用SATQuest对多种开源及闭源模型进行基准测试，发现其在高复杂度任务以及从数学符号到机器或叙事格式的迁移中存在持续差距。进一步表明，基于SATQuest的强化微调能显著提升目标性能并泛化至更大规模实例，但跨格式鲁棒性仍具挑战。总体而言，SATQuest为大模型逻辑推理及其训练提供了基于验证器的可控、可扩展、可复现的实证研究基础设施。
原文摘要 · Abstract (English)
Large language models (LLMs) exhibit strong general reasoning, yet the community lacks controllable, scalable, and verifiable tools to analyze and improve these abilities. We present SATQuest, a verifier that generates diverse SAT-based reasoning tasks directly from Conjunctive Normal Form (CNF) instances and checks answers objectively with PySAT. SATQuest factorizes evaluation along three orthogonal dimensions: instance, problem type, and question format, enabling fine-grained, multi-dimensional analysis and reinforcement fine-tuning. Randomized CNF generation mitigates memorization and supports reproducible experiments. Using SATQuest, we benchmark a range of open- and closed-weight LLMs and uncover persistent gaps in logical reasoning, particularly on higher-complexity tasks and in transfer beyond familiar mathematical notation to machine or narrative formats. We further show that reinforcement fine-tuning with SATQuest rewards substantially boosts targeted performance and generalizes to larger instances, while cross-format robustness remains challenging. Collectively, SATQuest provides verifier-backed infrastructure for controlled, scalable, and reproducible empirical research on LLM logical reasoning and its training.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。