SATQuest: Un verificador para la evaluación y refuerzo del razonamiento lógico Ajuste fino de modelos de lenguaje grandes (LLMs)

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

August 31, 2025

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

cs.AI

Resumen

Los recientes avances en los Modelos de Lenguaje de Gran Escala (LLMs, por sus siglas en inglés) han demostrado capacidades de razonamiento general notables. Sin embargo, evaluar y mejorar sistemáticamente estas capacidades de razonamiento es un desafío debido a la falta de herramientas controlables y escalables para un análisis detallado. Los puntos de referencia y conjuntos de datos existentes a menudo carecen del control de variables necesario para un análisis y entrenamiento sistemático y multidimensional, o presentan tipos y formatos de problemas limitados. Para abordar estas limitaciones, presentamos SATQuest, un verificador sistemático diseñado para evaluar y mejorar el razonamiento lógico en LLMs mediante la generación de diversos problemas de razonamiento lógico basados en Satisfacibilidad directamente a partir de instancias de Forma Normal Conjuntiva (CNF). SATQuest estructura estos problemas en tres dimensiones ortogonales: escala de la instancia, tipo de problema y formato de la pregunta, empleando generación de problemas aleatorizada basada en SAT y verificación objetiva de respuestas mediante PySAT. Este diseño mitiga problemas de memorización, permite obtener insights detallados sobre el rendimiento del razonamiento y posibilita un afinamiento efectivo mediante refuerzo. Nuestra evaluación extensiva de varios LLMs utilizando SATQuest identificó limitaciones significativas en su razonamiento lógico, particularmente en la generalización más allá de formatos matemáticos familiares. Además, demostramos que el afinamiento mediante refuerzo con recompensas de SATQuest mejora sustancialmente el rendimiento en tareas específicas y generaliza a instancias más complejas, al tiempo que resalta los desafíos restantes en la adaptación entre formatos. A través de estas demostraciones, mostramos el potencial de SATQuest como una herramienta fundamental y un punto de partida valioso para avanzar en el razonamiento lógico de los 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.