# SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs

arXiv: https://arxiv.org/abs/2509.00930 · HTML: https://mlsanity.com/paper/2509.00930/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 12 of its 32 references that are in the map.
- First posted on arXiv 31 Aug 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 12 of 12)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Logic-RL: Unleashing LLM Reasoning with Rule-Based Reinforcement Learning](https://mlsanity.com/paper/2502.14768/) (2025)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning](https://mlsanity.com/paper/2502.01100/) (2025)
- [BIG-Bench Extra Hard](https://mlsanity.com/paper/2502.19187/) (2025)
- [Multi-IF: Benchmarking LLMs on Multi-Turn and Multilingual Instructions Following](https://mlsanity.com/paper/2410.15553/) (2024)
- [SuperGPQA: Scaling LLM Evaluation across 285 Graduate Disciplines](https://mlsanity.com/paper/2502.14739/) (2025)
- [Benchmarking Reasoning Robustness in Large Language Models](https://mlsanity.com/paper/2503.04550/) (2025)
- [ThinkBench: Dynamic Out-of-Distribution Evaluation for Robust LLM Reasoning](https://mlsanity.com/paper/2502.16268/) (2025)
- [Have Large Language Models Learned to Reason? A Characterization via 3-SAT Phase Transition](https://mlsanity.com/paper/2504.03930/) (2025)

## Built on by (most cited first, 3 of 3)

- [Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning](https://mlsanity.com/paper/2607.17047/) (2026)
- [Recognition, Simulation, and Refusal: A Contamination-Aware Study of Classic Psychological Effects in LLM Agents](https://mlsanity.com/paper/2609.22090/) (2026)
- [Conditional Transfer from Controlled Pretraining Mixtures to Code](https://mlsanity.com/paper/2610.11548/) (2026)

## Abstract (arXiv)

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.