SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement
  Fine-Tuning of LLMs
Recent advances in Large Language Models (LLMs) have demonstrated remarkable
general reasoning capabilities. However, systematically evaluating and
enhancing these reasoning capabilities is challenging due to the lack of
controllable and scalable tools for fine-grained analysis. Existing benchmarks
and datasets often lack the necessary variable control for multi-dimensional,
systematic analysis and training, or have narrow problem types and formats. To
address these limitations, we introduce SATQuest, a systematic verifier
designed to evaluate and enhance logical reasoning in LLMs by generating
diverse, Satisfiability-based logical reasoning problems directly from
Conjunctive Normal Form (CNF) instances. SATQuest structures these problems
along three orthogonal dimensions: instance scale, problem type, and question
format, employing randomized, SAT-based problem generation and objective answer
verification via PySAT. This design mitigates memorization issues, allows for
nuanced insights into reasoning performance, and enables effective
reinforcement fine-tuning. Our extensive evaluation of various LLMs using
SATQuest identified significant limitations in their logical reasoning,
particularly in generalizing beyond familiar mathematical formats. Furthermore,
we show that reinforcement fine-tuning with SATQuest rewards substantially
improves targeted task performance and generalizes to more complex instances,
while highlighting remaining challenges in cross-format adaptation. Through
these demonstrations, we showcase SATQuest's potential as a foundational tool
and a valuable starting point for advancing LLM logical reasoning.
68b9c9be736018af705e8d9a
Yanxiao Zhao
claimed_verified
2025-09-04T19:32:45.230Z
63935b14b567032fe13b030d
https://cdn-avatars.huggingface.co/v1/production/uploads/1670601442899-noauth.jpeg
Yanxiao Zhao
user
sdpkjc
68b9c9be736018af705e8d9b
Yaqian Li
68b9c9be736018af705e8d9c
Zihao Bo
68b9c9be736018af705e8d9d
Rinyoichi Takezoe
68b9c9be736018af705e8d9e
Haojia Hui
68b9c9be736018af705e8d9f
Mo Guang
68b9c9be736018af705e8da0
Lei Ren
68b9c9be736018af705e8da1
Xiaolin Qin
68b9c9be736018af705e8da2
Kaiwen Long
SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement
  Fine-Tuning of LLMs
Recent advances in Large Language Models (LLMs) have demonstrated remarkable
general reasoning capabilities. However, systematically evaluating and
enhancing these reasoning capabilities is challenging due to the lack of
controllable and scalable tools for fine-grained analysis. Existing benchmarks
and datasets often lack the necessary variable control for multi-dimensional,
systematic analysis and training, or have narrow problem types and formats. To
address these limitations, we introduce SATQuest, a systematic verifier
designed to evaluate and enhance logical reasoning in LLMs by generating
diverse, Satisfiability-based logical reasoning problems directly from
Conjunctive Normal Form (CNF) instances. SATQuest structures these problems
along three orthogonal dimensions: instance scale, problem type, and question
format, employing randomized, SAT-based problem generation and objective answer
verification via PySAT. This design mitigates memorization issues, allows for
nuanced insights into reasoning performance, and enables effective
reinforcement fine-tuning. Our extensive evaluation of various LLMs using
SATQuest identified significant limitations in their logical reasoning,
particularly in generalizing beyond familiar mathematical formats. Furthermore,
we show that reinforcement fine-tuning with SATQuest rewards substantially
improves targeted task performance and generalizes to more complex instances,
while highlighting remaining challenges in cross-format adaptation. Through
these demonstrations, we showcase SATQuest's potential as a foundational tool
and a valuable starting point for advancing LLM logical reasoning.
SATQuest evaluates and enhances LLM logical reasoning by generating diverse SAT-based problems, offering insights into reasoning performance and enabling effective fine-tuning.
Large Language Models SATQuest logical reasoning Conjunctive Normal Form SAT-based problem generation PySAT reinforcement fine-tuning cross-format adaptation