SATQuest: Um Verificador para Avaliação de Raciocínio Lógico e Ajuste Fino de 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
Resumo
Os recentes avanços em Modelos de Linguagem de Grande Escala (LLMs) têm demonstrado capacidades impressionantes de raciocínio geral. No entanto, avaliar e aprimorar sistematicamente essas capacidades de raciocínio é desafiador devido à falta de ferramentas controláveis e escaláveis para análises detalhadas. Os benchmarks e conjuntos de dados existentes frequentemente carecem do controle de variáveis necessário para análises e treinamentos multidimensionais e sistemáticos, ou possuem tipos e formatos de problemas limitados. Para abordar essas limitações, introduzimos o SATQuest, um verificador sistemático projetado para avaliar e aprimorar o raciocínio lógico em LLMs, gerando problemas diversos de raciocínio lógico baseados em Satisfatibilidade diretamente a partir de instâncias de Forma Normal Conjuntiva (CNF). O SATQuest estrutura esses problemas ao longo de três dimensões ortogonais: escala da instância, tipo de problema e formato da questão, empregando geração de problemas randomizada baseada em SAT e verificação objetiva de respostas via PySAT. Esse design mitiga problemas de memorização, permite insights detalhados sobre o desempenho do raciocínio e possibilita um ajuste fino eficaz por reforço. Nossa extensa avaliação de vários LLMs usando o SATQuest identificou limitações significativas em seu raciocínio lógico, particularmente na generalização além de formatos matemáticos familiares. Além disso, mostramos que o ajuste fino por reforço com recompensas do SATQuest melhora substancialmente o desempenho em tarefas específicas e generaliza para instâncias mais complexas, ao mesmo tempo em que destaca os desafios remanescentes na adaptação entre formatos. Por meio dessas demonstrações, evidenciamos o potencial do SATQuest como uma ferramenta fundamental e um ponto de partida valioso para o avanço do raciocínio lógico em 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.