SATQuest: Un Verificatore per la Valutazione e il Rafforzamento del Ragionamento Logico attraverso il Fine-Tuning di LLM

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

August 31, 2025

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

cs.AI

Abstract

I recenti progressi nei Modelli Linguistici di Grande Scala (LLM) hanno dimostrato capacità di ragionamento generale notevoli. Tuttavia, valutare e migliorare sistematicamente queste capacità di ragionamento è complesso a causa della mancanza di strumenti controllabili e scalabili per un'analisi granulare. I benchmark e i dataset esistenti spesso non dispongono del controllo variabile necessario per un'analisi e un addestramento sistematici e multidimensionali, o presentano tipologie e formati di problemi limitati. Per affrontare queste limitazioni, introduciamo SATQuest, un verificatore sistematico progettato per valutare e migliorare il ragionamento logico negli LLM generando problemi di ragionamento logico basati sulla Soddisfacibilità direttamente da istanze in Forma Normale Congiuntiva (CNF). SATQuest struttura questi problemi lungo tre dimensioni ortogonali: scala dell'istanza, tipo di problema e formato della domanda, impiegando una generazione casuale di problemi basata su SAT e una verifica oggettiva delle risposte tramite PySAT. Questo design mitiga i problemi di memorizzazione, consente approfondimenti sfumati sulle prestazioni di ragionamento e abilita un efficace fine-tuning di rinforzo. La nostra valutazione estesa di vari LLM utilizzando SATQuest ha identificato significative limitazioni nel loro ragionamento logico, in particolare nella generalizzazione oltre i formati matematici familiari. Inoltre, dimostriamo che il fine-tuning di rinforzo con ricompense di SATQuest migliora sostanzialmente le prestazioni nei compiti mirati e generalizza a istanze più complesse, evidenziando al contempo le sfide rimanenti nell'adattamento cross-format. Attraverso queste dimostrazioni, mostriamo il potenziale di SATQuest come strumento fondamentale e un punto di partenza prezioso per avanzare il ragionamento logico degli LLM.

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.