SATQuest: Верификатор для оценки логического мышления и тонкой настройки LLM
SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs
August 31, 2025
Авторы: Yanxiao Zhao, Yaqian Li, Zihao Bo, Rinyoichi Takezoe, Haojia Hui, Mo Guang, Lei Ren, Xiaolin Qin, Kaiwen Long
cs.AI
Аннотация
Последние достижения в области больших языковых моделей (LLM) продемонстрировали впечатляющие способности к общему рассуждению. Однако систематическая оценка и улучшение этих способностей остаются сложными задачами из-за отсутствия контролируемых и масштабируемых инструментов для детального анализа. Существующие эталонные тесты и наборы данных часто не обеспечивают необходимого контроля переменных для многомерного систематического анализа и обучения или ограничены узкими типами и форматами задач. Для устранения этих ограничений мы представляем SATQuest — систематический верификатор, предназначенный для оценки и улучшения логического рассуждения в LLM путем генерации разнообразных задач на основе логического рассуждения, связанных с проблемами выполнимости (SAT), непосредственно из экземпляров конъюнктивной нормальной формы (КНФ). SATQuest структурирует эти задачи по трем ортогональным измерениям: масштаб экземпляра, тип задачи и формат вопроса, используя рандомизированную генерацию задач на основе SAT и объективную проверку ответов с помощью PySAT. Такой подход устраняет проблемы запоминания, позволяет получить детальные insights о производительности рассуждений и обеспечивает эффективную тонкую настройку с подкреплением. Наше обширное тестирование различных LLM с использованием SATQuest выявило значительные ограничения в их логическом рассуждении, особенно в обобщении за пределами знакомых математических форматов. Кроме того, мы показываем, что тонкая настройка с подкреплением с использованием наград от SATQuest существенно улучшает производительность на целевых задачах и обобщается на более сложные экземпляры, одновременно выявляя оставшиеся проблемы в адаптации к различным форматам. Эти демонстрации подчеркивают потенциал SATQuest как основополагающего инструмента и ценной отправной точки для продвижения логического рассуждения в 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.