SATQuest: Ein Verifizierer zur Bewertung und Verstärkung logischen Denkens durch Feinabstimmung von LLMs

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

August 31, 2025

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

cs.AI

papers.abstract

Jüngste Fortschritte bei großen Sprachmodellen (LLMs) haben bemerkenswerte allgemeine Fähigkeiten im Bereich des logischen Denkens demonstriert. Die systematische Bewertung und Verbesserung dieser Fähigkeiten gestaltet sich jedoch aufgrund des Mangels an kontrollierbaren und skalierbaren Werkzeugen für eine feingranulare Analyse als herausfordernd. Bestehende Benchmarks und Datensätze bieten oft nicht die notwendige Variablenkontrolle für eine mehrdimensionale, systematische Analyse und Schulung oder beschränken sich auf eng gefasste Problemtypen und Formate. Um diese Einschränkungen zu überwinden, stellen wir SATQuest vor, einen systematischen Verifizierer, der entwickelt wurde, um das logische Denken in LLMs zu bewerten und zu verbessern, indem er vielfältige, auf Erfüllbarkeit basierende logische Denkprobleme direkt aus Konjunktiven Normalformen (CNF) generiert. SATQuest strukturiert diese Probleme entlang drei orthogonaler Dimensionen: Instanzgröße, Problemtyp und Fragestellungsformat, und nutzt dabei randomisierte, SAT-basierte Problemgenerierung sowie objektive Antwortverifizierung mittels PySAT. Dieser Ansatz minimiert Gedächtnisprobleme, ermöglicht differenzierte Einblicke in die Denkleistung und erlaubt eine effektive Verstärkungsfeinabstimmung. Unsere umfangreiche Bewertung verschiedener LLMs mit SATQuest offenbarte signifikante Einschränkungen in ihrem logischen Denken, insbesondere bei der Verallgemeinerung über vertraute mathematische Formate hinaus. Darüber hinaus zeigen wir, dass eine Verstärkungsfeinabstimmung mit SATQuest-Belohnungen die Leistung bei gezielten Aufgaben erheblich verbessert und auf komplexere Instanzen verallgemeinert, während sie gleichzeitig verbleibende Herausforderungen bei der Anpassung über verschiedene Formate hinweg aufzeigt. Durch diese Demonstrationen verdeutlichen wir das Potenzial von SATQuest als grundlegendes Werkzeug und wertvollen Ausgangspunkt für die Weiterentwicklung des logischen Denkens 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.