用大模型生成逻辑题，让推理能力评测更难更真实
Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation
- 用大模型与符号证明器结合生成逻辑推理题
- 新数据集ProverQA难题让顶尖大模型也难解
- 适合评估和训练逻辑推理能力的模型
一阶逻辑（FOL）推理涉及序列推导，对智能系统至关重要，是检验链式思维（CoT）能力的重要任务。现有基准多依赖人工标注或手工模板，难以实现足够的复杂性、可扩展性和多样性。为此，我们提出ProverGen框架，融合大语言模型的生成能力与符号证明器的严谨性，构建可扩展、多样化且高质量的FOL推理数据集ProverQA。该数据集包含每道题清晰连贯的中间推理步骤。评估显示，即使使用CoT提示，当前最先进大模型在ProverQA上表现依然不佳，凸显其挑战性。我们还基于该框架生成训练集，微调Llama3.1-8B-Instruct模型，在分布内与分布外测试集均表现提升，验证了数据生成框架的有效性。代码已开源。
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。