ProverQA

ProverQA是一个由大型语言模型和符号证明器共同生成的 first-order logic (FOL) 推理数据集，包含1500个实例，分为简单、中等和困难三个难度级别。该数据集通过结合大型语言模型的生成能力和符号证明器的精确性，创建了可扩展、多样化、高质量的数据集，特点是每个问题都包含可访问的、逻辑上一致的中间推理步骤。数据集旨在解决逻辑推理能力评估的问题，特别是针对链式思维（CoT）场景。

ProverQA is a first-order logic (FOL) reasoning dataset jointly generated by large language models and symbolic theorem provers, containing 1500 instances categorized into three difficulty levels: easy, medium, and hard. By integrating the generative strengths of large language models and the rigorous precision of symbolic theorem provers, this dataset features scalability, diversity and high-quality data, with each problem including accessible and logically consistent intermediate reasoning steps. The dataset is designed to address the evaluation of logical reasoning capabilities, particularly in chain-of-thought (CoT) scenarios.

原始信息汇总

ProverGen 数据集概述

数据集简介

ProverGen 是一个用于逻辑推理评估的合成数据集，它结合了大语言模型和符号证明器，旨在评估大型语言模型在逻辑推理方面的性能。

数据集结构

数据集的生成分为三个关键步骤：

1. 逻辑骨架生成（Logic Skeleton Generation）
2. 逻辑骨架翻译（Logic Skeleton Translation）
3. 一阶逻辑问题生成（FOL Problem Generation）

安装说明

• 环境搭建：使用conda创建虚拟环境并激活，克隆ProverGen仓库，安装所需依赖。
• Prover9安装：从官网下载并按照指南安装，可能需要针对Linux和MacOS进行特定的错误修复。

数据生成

• 逻辑骨架生成：通过logic_skeleton_generator.py脚本生成逻辑骨架，支持自定义生成数量、难度、答案分布等参数。
• 逻辑骨架翻译：使用logic_skeleton_translator.py脚本将逻辑表达式转换为自然语言，可通过指定LLM模型进行翻译。
• 一阶逻辑问题生成：通过fol_problem_generator.py脚本生成最终的问题，支持数据增强技术如问题分步生成或句子改写。

评估方法

使用evaluation.py脚本评估LLM在ProverGen数据集上的性能，支持直接模式和CoT模式，并提供指标计算。

模型性能

论文中额外评估了OpenAI-O1和DeepSeek-R1两个推理模型在零样本设置下的性能。

引用信息

如若数据集对您的研究有所帮助，请引用以下论文：

@inproceedings{ qi2025large, title={Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation}, author={Chengwen Qi and Ren Ma and Bowen Li and He Du and Binyuan Hui and Jinwang Wu and Yuanjun Laili and Conghui He}, booktitle={The Thirteenth International Conference on Learning Representations}, year={2025}, url={https://openreview.net/forum?id=C25SgeXWjE} }

搜集汇总

数据集介绍

构建方式

ProverQA数据集的构建过程涉及三个主要步骤。首先，使用大型语言模型(LLM)为每个问题生成一个独特的背景故事，以实现语言的自然性和多样性。其次，采用符号证明器（如Prover9）构建逻辑骨架，即推理树，并计算相关事实的真值，确保逻辑的严谨性。最后，LLM将这些逻辑表达式转换为自然语言陈述。整个框架将LLM的生成能力和符号证明器的精确性相结合，确保了数据集的质量和多样性。

使用方法

使用ProverQA数据集进行评估和训练时，可以采用标准提示或思维链提示策略。标准提示使用2-shot上下文学习直接提示LLM回答问题，而思维链提示则使用2-shot示例指导模型逐步解决问题。此外，还可以通过数据增强技术，如将推理链的每个步骤分解成新问题，以及用随机事实替换最终结论来创建答案不确定的问题，进一步扩展数据集。在微调实验中，可以选择不同的训练超参数，如训练周期、学习率和训练集大小，并在保留的验证集上选择最佳配置。

背景与挑战

背景概述

ProverQA数据集，由北京航空航天大学、上海人工智能实验室、复旦大学、中关村实验室和北京智能制造系统技术国家重点实验室的研究人员于2025年提出，旨在解决现有的一阶逻辑（FOL）推理数据集在复杂度、可扩展性、多样性和推理链透明度方面的不足。ProverQA数据集通过结合大型语言模型（LLMs）的生成能力和符号证明器的严谨性，创造了一个可扩展、多样且高质量的FOL推理数据集。该数据集的独特之处在于其包含易于访问且逻辑上连贯的中间推理步骤，为每个问题提供。该数据集的提出对相关领域产生了重大影响，为评估和改进LLMs的逻辑推理能力提供了一个强大的基准。

当前挑战

ProverQA数据集面临的挑战包括：1)现有FOL推理数据集在复杂度、可扩展性、多样性和推理链透明度方面的不足；2)构建过程中遇到的挑战，例如如何确保生成的数据集在逻辑上是一致的，以及如何避免数据污染。ProverQA数据集通过结合LLMs和符号证明器，成功地解决了这些问题，并创建了一个具有挑战性的数据集，即使是使用CoT提示的SOTA LLMs也很难解决其中的问题。

常用场景

经典使用场景

ProverQA数据集主要用于评估大型语言模型（LLMs）在逻辑推理方面的能力，尤其是在链式思维（CoT）情境下的推理能力。该数据集包含了丰富的自然语言表达，涵盖了多种复杂的逻辑规则，以及中间推理步骤的清晰阐述，使得ProverQA成为了一个全面且具有挑战性的评估基准。

解决学术问题

ProverQA数据集解决了现有FOL推理数据集在复杂性、可扩展性、多样性和逻辑连贯性方面的不足。它通过结合大型语言模型的生成能力和符号证明器的严谨性和精确性，创建了一个可扩展、多样且高质量的FOL推理数据集。此外，ProverQA还提供了易于访问且逻辑上连贯的中间推理步骤，促进了模型的透明度和进一步训练。

实际应用

ProverQA数据集的实际应用场景包括但不限于：1）用于评估和比较不同LLMs在逻辑推理任务上的性能；2）作为训练数据，用于微调和提升LLMs的逻辑推理能力；3）作为研究工具，用于探索和解决逻辑推理中的挑战性问题。

数据集最近研究

最新研究方向

ProverQA数据集通过结合大型语言模型（LLMs）和符号证明器的优势，为逻辑推理评估提供了一个新颖的框架。该数据集不仅包含丰富多样的自然语言表达，还具备形式化的符号结构，并提供了清晰的推理步骤，为评估LLMs的逻辑推理能力提供了一个全面的基准。此外，ProverQA的生成框架能够生成新的、未受污染的数据集，有助于LLMs的进一步训练和评估。该数据集的提出对于推动LLMs在逻辑推理领域的应用和发展具有重要意义，并为相关研究提供了新的方向和思路。

相关研究论文

• Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation

  北京航空航天大学, 上海人工智能实验室, 复旦大学, 中关村实验室, 北京智能制造系统技术国家重点实验室 · 2025年