MorishT/2024-07-08.JFLD.step-3

该数据集包含与逻辑推理相关的数据，涵盖了假设、事实、证明、负面假设、负面证明等多个方面。每个样本包含假设、假设的公式表示、事实、事实的公式表示、证明、证明的公式表示、负面假设、负面假设的公式表示、负面证明等信息。此外，还包含与证明步骤、树深度、干扰项数量等相关的字段。数据集分为训练集和测试集，每个集合包含500个样本。

This dataset contains data related to logical reasoning, covering aspects such as hypotheses, facts, proofs, negative hypotheses, and negative proofs. Each sample includes hypotheses, their formula representations, facts, formula representations of facts, proofs, formula representations of proofs, negative hypotheses, formula representations of negative hypotheses, negative proofs, and more. Additionally, it includes fields related to proof steps, tree depth, number of distractors, etc. The dataset is divided into training and test sets, each containing 500 samples.

原始信息汇总

数据集概述

特征信息

• version: 数据集版本，类型为字符串。
• hypothesis: 假设，类型为字符串。
• hypothesis_formula: 假设公式，类型为字符串。
• facts: 事实，类型为字符串。
• facts_formula: 事实公式，类型为字符串。
• proofs: 证明序列，类型为字符串序列。
• proofs_formula: 证明公式序列，类型为字符串序列。
• negative_hypothesis: 负假设，类型为字符串。
• negative_hypothesis_formula: 负假设公式，类型为字符串。
• negative_proofs: 负证明序列，类型为字符串序列。
• negative_original_tree_depth: 负原始树深度，类型为整数。
• original_tree_steps: 原始树步骤数，类型为整数。
• original_tree_depth: 原始树深度，类型为整数。
• steps: 步骤数，类型为整数。
• depth: 深度，类型为整数。
• num_formula_distractors: 公式干扰项数量，类型为整数。
• num_translation_distractors: 翻译干扰项数量，类型为整数。
• num_all_distractors: 所有干扰项数量，类型为整数。
• proof_label: 证明标签，类型为字符串。
• negative_proof_label: 负证明标签，类型为字符串。
• world_assump_label: 世界假设标签，类型为字符串。
• negative_world_assump_label: 负世界假设标签，类型为字符串。
• prompt_serial: 提示序列，类型为字符串。
• proof_serial: 证明序列，类型为字符串。
• prompt_serial_formula: 提示序列公式，类型为字符串。
• proof_serial_formula: 证明序列公式，类型为字符串。

数据集划分

• train: 训练集，包含500个样本，大小为2485874字节。
• test: 测试集，包含500个样本，大小为2534403字节。

数据集大小

• 下载大小: 1730439字节。
• 数据集总大小: 5020277字节。

配置信息

• config_name: default
  • data_files:
    • train: 路径为data/train-*。
    • test: 路径为data/test-*。

搜集汇总

数据集介绍

构建方式

在形式逻辑推理领域，数据集的构建需兼顾严谨性与多样性。该数据集通过系统化生成逻辑命题及其证明过程而构建，涵盖了假设、事实、证明序列及其形式化表示。构建过程中，不仅生成了正向的逻辑推理链条，还特意引入了负例假设与干扰证明，以模拟真实推理场景中的复杂性与挑战性。数据生成基于预设的逻辑规则与树形结构深度控制，确保每个样本在步骤与深度上均具有可追溯的规范性。

特点

该数据集的核心特征在于其双重逻辑结构的设计，同时包含自然语言描述与形式化公式表达，为跨模态逻辑推理研究提供了丰富素材。样本中不仅标注了原始证明树深度与步骤，还集成了多种干扰项，如公式干扰与翻译干扰，以增强模型在噪声环境下的鲁棒性。此外，数据集明确区分了正向与负向证明标签及世界假设标签，支持对逻辑一致性、可证伪性等高级推理能力的评估。

使用方法

使用该数据集时，研究者可依据其分割为训练集与测试集的特性，开展逻辑推理模型的训练与验证。通过解析假设、事实及证明序列字段，可构建端到端的自动证明生成任务。形式化公式字段则为符号推理与神经符号结合方法提供了直接输入。负例与干扰项的引入使得数据集适用于对抗性训练或鲁棒性测试，而多标签结构支持细粒度的性能评估，如证明有效性分类与逻辑错误检测。

背景与挑战

背景概述

在形式逻辑推理领域，自动定理证明与自然语言理解相结合的研究长期面临数据稀缺的困境。MorishT/2024-07-08.JFLD.step-3数据集于2024年由相关研究团队构建，旨在提供结构化逻辑推理任务的大规模标注数据。该数据集的核心研究问题聚焦于从自然语言前提推导出逻辑假设的自动化过程，其特色在于同时包含自然语言表述与形式化逻辑公式的双重标注。此类数据集的建立，为训练和评估能够跨越自然语言与形式语言鸿沟的机器学习模型奠定了重要基础，推动了神经符号人工智能在复杂推理任务中的应用进展。

当前挑战

该数据集致力于解决形式逻辑推理自动化这一核心领域挑战，其难点在于模型需同时精准理解自然语言语义并执行严格的符号逻辑演算。在构建过程中，挑战具体体现在多个层面：首先，确保自然语言描述的事实与假设能够被无歧义地转换为形式逻辑公式，这要求标注者具备深厚的逻辑学与语言学交叉知识。其次，生成高质量的正例证明与负例干扰项需要精密的算法设计，以控制证明步骤的复杂度与干扰项的迷惑性，从而构建出具有恰当难度梯度的评估基准。最后，维持数据规模与标注质量之间的平衡，也是数据集构建中需要克服的关键难题。

常用场景

经典使用场景

在形式逻辑与自动推理领域，该数据集通过结构化的事实、假设与证明序列，为逻辑推理模型的训练与评估提供了标准化的基准。其经典使用场景聚焦于逻辑公式的自动推导与验证，研究者利用数据集中的假设、事实及证明步骤，训练模型从给定前提中生成严谨的逻辑证明链条，从而检验模型在符号推理任务中的准确性与泛化能力。

衍生相关工作

围绕该数据集，已衍生出多项经典研究工作，包括基于注意力机制的神经定理证明器、结合图神经网络与符号推理的混合模型，以及针对逻辑公式翻译与对齐的跨模态学习方法。这些工作不仅推动了自动推理技术的进步，也为自然语言处理与形式逻辑的交叉研究开辟了新的方向，促进了人工智能在复杂推理任务中的应用深化。

数据集最近研究

最新研究方向

在形式逻辑推理领域，JFLD数据集凭借其结构化特征，正推动神经符号人工智能的前沿探索。该数据集将自然语言假设与形式化逻辑表示相结合，为模型提供了从事实到证明的完整推理链条，包括正向与负向示例。当前研究聚焦于利用此类数据增强大语言模型的逻辑推理能力，特别是在数学定理证明和常识推理的交叉应用中。热点事件如GPT-4等模型在逻辑任务上的突破，促使学界更加关注如何通过类似JFLD的精细标注数据来提升模型的演绎准确性和抗干扰性。这一方向不仅深化了人工智能对复杂推理过程的理解，也为构建可解释、可靠的推理系统奠定了数据基础，具有重要的理论意义与应用价值。