MorishT/2024-07-08.JFLD.cmpl-0.2.dstrct-5.step-5

该数据集包含多个特征字段，如版本、假设、事实、证明等，这些字段分别存储了不同形式的数据，如字符串、序列和整数。数据集分为训练集和测试集，分别包含3000个样本。此外，还提供了数据集的下载大小和总大小信息。

The dataset includes multiple features such as version, hypothesis, facts, proofs, etc., each with its data type. The dataset is divided into training and testing parts, each containing 3000 samples. The size and download size of the dataset are also specified.

原始信息汇总

数据集概述

数据集特征

• version: 字符串类型
• hypothesis: 字符串类型
• hypothesis_formula: 字符串类型
• facts: 字符串类型
• facts_formula: 字符串类型
• proofs: 字符串序列类型
• proofs_formula: 字符串序列类型
• negative_hypothesis: 字符串类型
• negative_hypothesis_formula: 字符串类型
• negative_proofs: 字符串序列类型
• negative_original_tree_depth: 64位整数类型
• original_tree_steps: 64位整数类型
• original_tree_depth: 64位整数类型
• steps: 64位整数类型
• depth: 64位整数类型
• num_formula_distractors: 64位整数类型
• num_translation_distractors: 64位整数类型
• num_all_distractors: 64位整数类型
• proof_label: 字符串类型
• negative_proof_label: 字符串类型
• world_assump_label: 字符串类型
• negative_world_assump_label: 字符串类型
• prompt_serial: 字符串类型
• proof_serial: 字符串类型
• prompt_serial_formula: 字符串类型
• proof_serial_formula: 字符串类型

数据集分割

• train:
  • 字节数: 7885382
  • 样本数: 3000
• test:
  • 字节数: 7837211
  • 样本数: 3000

数据集大小

• 下载大小: 5106436 字节
• 数据集总大小: 15722593 字节

配置

• config_name: default
  • data_files:
    • train: data/train-*
    • test: data/test-*

搜集汇总

数据集介绍

构建方式

在形式化推理与数学证明的交叉领域，该数据集通过系统化的干扰项注入机制构建而成。其核心设计围绕自然语言与形式化公式的双模态表达，每个样本包含一个待验证的假设（hypothesis）及其对应的形式化公式，同时提供一组事实陈述（facts）与形式化证明步骤（proofs）。为增强推理难度，数据集引入了负样本假设（negative_hypothesis）及其证明，并通过控制干扰项数量（如公式干扰因子num_formula_distractors与翻译干扰因子num_translation_distractors）来调节复杂度。所有样本均源自原始树状证明结构的深度与步骤约束，最终生成3000条训练与测试样本，确保逻辑结构的严谨性与多样性。

特点

该数据集最显著的特点在于其多维度标签体系与结构化证明序列的有机融合。每个样本不仅包含假设与事实的文本-公式双通道表示，还记录了原始证明树深度（original_tree_depth）与步骤数（steps）等拓扑属性，为评估推理链的复杂度提供了量化基准。尤为突出的是，数据集通过proof_label与negative_proof_label等标签区分正误推理路径，并引入world_assump_label标记世界假设的一致性。此外，干扰项数量的精细调控（num_all_distractors）使得模型需在噪声环境中甄别有效逻辑链，这一设计显著提升了数据集在鲁棒性训练与对抗性评估中的实用价值。

使用方法

研究者可基于该数据集开展形式化推理与数学证明的监督学习任务。具体而言，利用prompt_serial与proof_serial字段构建序列到序列的生成模型，以自然语言或形式化公式为输入，训练模型输出对应的证明步骤。通过对比hypothesis与negative_hypothesis的推理路径差异，可设计判别式任务用于验证逻辑一致性。数据集预划分的train与test分片（各3000例）便于直接进行交叉验证，而干扰项配置字段（如num_formula_distractors）则支持分层采样，以评估模型在不同干扰强度下的泛化能力。建议结合序列标注或图神经网络架构，充分利用proofs_formula等结构化特征。

背景与挑战

背景概述

在形式逻辑与自动定理证明领域，构造高质量、多样化的推理数据集是推动神经符号学习发展的关键。MorishT/2024-07-08.JFLD.cmpl-0.2.dstrct-5.step-5 数据集由研究团队于2024年7月创建，旨在为逻辑推理模型提供包含正反例证明、干扰项以及序列化提示的结构化训练与测试样本。该数据集包含3000条训练样本和3000条测试样本，每条记录涵盖假设、事实、证明序列、负例假设及其证明，并引入公式化表示与多种干扰项（如公式干扰与翻译干扰），以模拟真实推理中的噪声与歧义。通过量化树深度、步骤数及标签信息，该数据集为评估模型在复杂逻辑结构下的泛化能力提供了基准，对推动可解释人工智能与数学推理系统的研究具有重要影响。

当前挑战

当前数据集面临的核心挑战包括三方面。其一，领域问题层面，自动定理证明需处理逻辑结构的组合爆炸与证明路径的搜索复杂度，而现有模型在对抗性干扰（如公式干扰与翻译干扰）下常出现语义偏移，难以区分有效证明与伪证明。其二，构建过程中，如何平衡正负例比例、设计具有足够区分度的干扰项（如num_formula_distractors与num_translation_distractors的设定）并确保树深度与步骤数的分布覆盖真实推理场景，是数据生成的关键难点。其三，序列化表示（prompt_serial与proof_serial）的标准化与公式化转换（如hypothesis_formula与facts_formula）需兼顾人类可读性与机器解析效率，避免信息丢失或冗余，这对标注一致性与格式鲁棒性提出了严苛要求。

常用场景

经典使用场景

该数据集聚焦于逻辑推理与形式化证明的交叉领域，为自然语言与符号逻辑的语义对齐提供了宝贵的资源。其核心应用场景在于训练和评估语言模型对数学命题的推导能力，尤其是在存在干扰信息（如公式翻译干扰或逻辑无关前提）的环境下，模型需从给定的假设与事实中生成完整、正确的证明链。数据集中包含正反假设及其对应的证明序列，并标注了证明的深度与步骤数，这使得它成为研究结构化推理、反事实推理以及逻辑鲁棒性的理想基准。研究者可借此探究模型能否在复杂逻辑迷宫中保持连贯的演绎路径，从而推动神经符号系统的融合。

解决学术问题

在学术研究中，该数据集主要解决了自然语言推理领域内形式化证明自动生成这一长期挑战。传统数据集多聚焦于简单的蕴含关系分类，而本数据通过引入多步证明序列、负样本干扰以及树状推理结构，直接回应了模型在复杂逻辑链条上的脆弱性问题。它使研究者能够系统评估模型在逐步推理中的错误传播现象，并量化干扰项对推理正确率的影响。此外，数据集中对证明深度与步骤数的精细控制，为探索推理复杂度与模型性能之间的缩放定律提供了数据支撑，从而深化了我们对语言模型逻辑泛化边界的理解。

衍生相关工作

该数据集衍生了一系列关于结构化推理与对抗性鲁棒性的经典工作。研究者基于其多步证明序列构建了分层推理框架，例如通过树状解码器逐步展开证明路径，并与传统的序列到序列模型进行比较，揭示了显式推理结构对逻辑一致性的提升作用。另一些工作则利用数据集中丰富的干扰项标签，设计了对抗性训练策略，使模型在推理时能够主动忽略无关信息，从而在逻辑谜题和数学竞赛题上取得突破性进展。此外，该数据集的负样本设计还催生了关于反事实推理可解释性的研究，通过对比正反证明链的差异，学者们提出了注意力剪枝与证明路径可视化方法，为理解黑盒模型的决策逻辑提供了新视角。