SATQuest: 用于逻辑推理评估和语言模型（LLM）微调的验证器

近期，大型语言模型（LLM）在通用推理能力方面取得了显著进展。然而，由于缺乏可控且可扩展的精细化分析工具，系统地评估和增强这些推理能力面临挑战。现有的基准测试和数据集往往缺乏多维度、系统性分析和训练所需的变量控制，或者问题类型和格式较为狭窄。为了克服这些局限性，我们引入了 SATQuest，一个系统的验证器，旨在通过直接从合取范式（CNF）实例生成多样化的、基于可满足性（Satisfiability）的逻辑推理问题，来评估和增强 LLM 的逻辑推理能力。SATQuest 沿三个正交维度来构建这些问题：实例规模、问题类型和问题格式，并采用随机的、基于 SAT 的问题生成以及通过 PySAT 进行客观答案验证。这种设计缓解了记忆化问题，能够提供对推理性能的细致洞察，并实现有效的强化微调。我们使用 SATQuest 对各种 LLM 进行的广泛评估，发现了它们在逻辑推理方面存在的显著局限性，特别是在泛化到熟悉数学格式之外的推理能力方面。此外，我们证明了使用 SATQuest 奖励进行强化微调，可以显著提高目标任务的性能，并泛化到更复杂的问题，同时突显了跨格式适应性方面仍然存在的挑战。通过这些演示，我们展示了 SATQuest 作为基础工具和推动 LLM 逻辑推理发展的宝贵起点的潜力。