SATQuest: Een Verificatiemiddel voor de Evaluatie en Versterking van Logisch Redeneren bij Fijnafstemming van LLM's

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

August 31, 2025

Auteurs: Yanxiao Zhao, Yaqian Li, Zihao Bo, Rinyoichi Takezoe, Haojia Hui, Mo Guang, Lei Ren, Xiaolin Qin, Kaiwen Long

cs.AI

Samenvatting

Recente ontwikkelingen in Large Language Models (LLMs) hebben opmerkelijke algemene redeneervaardigheden aangetoond. Het systematisch evalueren en verbeteren van deze redeneervaardigheden is echter een uitdaging vanwege het gebrek aan controleerbare en schaalbare tools voor gedetailleerde analyse. Bestaande benchmarks en datasets missen vaak de noodzakelijke variabele controle voor multidimensionale, systematische analyse en training, of hebben beperkte probleemtypen en formaten. Om deze beperkingen aan te pakken, introduceren we SATQuest, een systematische verifier die is ontworpen om logisch redeneren in LLMs te evalueren en te verbeteren door diverse, op bevredigbaarheid gebaseerde logische redeneerproblemen direct te genereren uit Conjunctive Normal Form (CNF)-instanties. SATQuest structureert deze problemen langs drie orthogonale dimensies: instantieschaal, probleemtype en vraagformaat, waarbij gebruik wordt gemaakt van gerandomiseerde, SAT-gebaseerde probleemgeneratie en objectieve antwoordverificatie via PySAT. Dit ontwerp vermindert problemen met memorisatie, biedt genuanceerde inzichten in redeneerprestaties en maakt effectieve reinforcement fine-tuning mogelijk. Onze uitgebreide evaluatie van verschillende LLMs met behulp van SATQuest identificeerde significante beperkingen in hun logisch redeneren, met name in het generaliseren buiten vertrouwde wiskundige formaten. Bovendien tonen we aan dat reinforcement fine-tuning met SATQuest-beloningen de prestaties voor specifieke taken aanzienlijk verbetert en generaliseert naar complexere instanties, terwijl het resterende uitdagingen in cross-formaat aanpassing benadrukt. Door deze demonstraties laten we het potentieel van SATQuest zien als een fundamenteel tool en een waardevol startpunt voor het bevorderen van logisch redeneren in LLMs.

English

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.