大型语言模型结合符号证明器用于逻辑推理评估
Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation
AI总结：
本文提出ProverGen框架，结合大型语言模型与符号证明器生成高质量的一阶逻辑推理数据集ProverQA，实验表明现有模型在该数据集上表现不佳，而基于该框架数据微调的模型性能显著提升。
摘要：
一阶逻辑（FOL）推理涉及顺序演绎，对智能系统至关重要，并且是评估推理能力的一项有价值任务，尤其是在思维链（CoT）语境中。现有基准通常依赖大量人工标注或手工制作的模板，难以实现稳健评估所需的复杂性、可扩展性和多样性。为了解决这些局限性，我们提出了一个名为ProverGen的新颖框架，该框架将大型语言模型（LLMs）的生成优势与符号证明器的严谨性和精确性相结合，从而能够创建一个可扩展、多样且高质量的FOL推理数据集ProverQA。ProverQA的另一个特点是为每个问题提供了易于理解且逻辑连贯的中间推理步骤。我们的评估表明，即使使用CoT提示，最先进的LLMs也难以解决ProverQA问题，凸显了该数据集的挑战性。我们还在由我们的框架生成的独立训练集上对Llama3.1-8B-Instruct进行了微调。微调后的模型在分布内和分布外测试集上均表现出持续的改进，表明了我们提出的数据生成框架的价值。代码可在以下网址获取：https://github.com/opendatalab/ProverGen
英文摘要：
First-order logic (FOL) reasoning, which involves sequential deduction, is pivotal for intelligent systems and serves as a valuable task for evaluating reasoning capabilities, particularly in chain-of-thought (CoT) contexts. Existing benchmarks often rely on extensive human annotation or handcrafted templates, making it difficult to achieve the necessary complexity, scalability, and diversity for robust evaluation. To address these limitations, we propose a novel framework called ProverGen that synergizes the generative strengths of Large Language Models (LLMs) with the rigor and precision of symbolic provers, enabling the creation of a scalable, diverse, and high-quality FOL reasoning dataset, ProverQA. ProverQA is also distinguished by its inclusion of accessible and logically coherent intermediate reasoning steps for each problem. Our evaluation shows that state-of-the-art LLMs struggle to solve ProverQA problems, even with CoT prompting, highlighting the dataset's challenging nature. We also finetune Llama3.1-8B-Instruct on a separate training set generated by our framework. The finetuned model demonstrates consistent improvements on both in-distribution and out-of-distribution test sets, suggesting the value of our proposed data generation framework. Code available at: https://github.com/opendatalab/ProverGen
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
