SATQuest : Un vérificateur pour l'évaluation du raisonnement logique et le réglage fin des LLM
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
Les récents progrès des modèles de langage à grande échelle (LLMs) ont démontré des capacités de raisonnement général remarquables. Cependant, l'évaluation systématique et l'amélioration de ces capacités de raisonnement posent des défis en raison du manque d'outils contrôlables et évolutifs pour une analyse fine. Les benchmarks et ensembles de données existants manquent souvent du contrôle nécessaire des variables pour une analyse et un entraînement multidimensionnels et systématiques, ou se limitent à des types et formats de problèmes restreints. Pour pallier ces limitations, nous présentons SATQuest, un vérificateur systématique conçu pour évaluer et améliorer le raisonnement logique des LLMs en générant des problèmes de raisonnement logique diversifiés basés sur la satisfiabilité directement à partir d'instances de forme normale conjonctive (CNF). SATQuest structure ces problèmes selon trois dimensions orthogonales : l'échelle de l'instance, le type de problème et le format de question, en utilisant une génération de problèmes aléatoire basée sur SAT et une vérification objective des réponses via PySAT. Cette conception atténue les problèmes de mémorisation, permet des insights nuancés sur les performances de raisonnement et facilite un réglage fin par renforcement efficace. Notre évaluation approfondie de divers LLMs avec SATQuest a révélé des limitations significatives dans leur raisonnement logique, notamment en ce qui concerne la généralisation au-delà des formats mathématiques familiers. De plus, nous montrons que le réglage fin par renforcement avec les récompenses de SATQuest améliore substantiellement les performances sur les tâches ciblées et généralise à des instances plus complexes, tout en mettant en lumière les défis persistants dans l'adaptation inter-formats. À travers ces démonstrations, nous illustrons le potentiel de SATQuest en tant qu'outil fondamental et point de départ précieux pour faire progresser le raisonnement logique des 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.