SATQuest：用于大语言模型逻辑推理评估与强化微调的验证器
人工智能
2025-09-04 v1 机器学习
计算机科学中的逻辑
摘要
大语言模型（LLMs）的最新进展展示了其卓越的通用推理能力。然而，由于缺乏可控且可扩展的细粒度分析工具，系统性地评估和增强这些推理能力仍具挑战性。现有的基准和数据集往往缺乏多维度系统分析与训练所需的变量控制，或问题类型与格式过于狭窄。为解决这些局限性，我们引入了 SATQuest，这是一种系统性验证器，旨在通过直接从合取范式（CNF）实例生成多样化的基于可满足性的逻辑推理问题来评估和增强 LLMs 的逻辑推理能力。SATQuest 沿三个正交维度构建问题：实例规模、问题类型和问题格式，采用基于 SAT 的随机问题生成和通过 PySAT 进行的客观答案验证。该设计缓解了记忆问题，允许对推理性能进行细致入微的洞察，并实现了有效的强化微调。我们使用 SATQuest 对多种 LLMs 进行了广泛评估，发现其在逻辑推理方面存在显著局限，特别是在泛化到熟悉的数学格式之外时。此外，我们表明，使用 SATQuest 奖励进行强化微调可显著提高目标任务性能，并能泛化到更复杂的实例，同时突出了跨格式适应方面依然存在的挑战。通过这些演示，我们展示了 SATQuest 作为推进 LLM 逻辑推理的基础工具和宝贵起点的潜力。
引用
@article{arxiv.2509.00930,
title = {SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs},
author = {Yanxiao Zhao and Yaqian Li and Zihao Bo and Rinyoichi Takezoe and Haojia Hui and Mo Guang and Lei Ren and Xiaolin Qin and Kaiwen Long},
journal= {arXiv preprint arXiv:2509.00930},
year = {2025}
}