nanoGentzen

nanoGentzen 合成推导数据集（200k 转换）是一个为自动定理证明设计的形式化合成数据集，专注于直觉逻辑（LI）和经典逻辑（LK，通过 Glivenko 定理）的 Gentzen 序列演算。每条记录表示一个 AND-OR 证明搜索树中的单一状态-动作推导转换，提供多任务监督信号，用于推理规则选择、前件前提定位和分支可证明性估计。数据集包含 200,000 条转换记录，以 PyTorch 张量（.pt）和 JSON Lines（.jsonl）两种格式提供。每条记录包含字段：样本标识符、当前序列（sequent，形式字符串表示）、目标推理规则（如 AXIOM、R_IMP 等）、规则索引（0-10 的整数类别标签）、前件假设索引（pivot，0-15）、分支可证明性真值（target_value，0.0 或 1.0）、根定理（root_sequent）、推导步骤编号、总步骤数、token 化整数序列（input_ids）以及 token 长度。规则标签映射覆盖 11 种 Gentzen 规则：AXIOM（0）、R_IMP（1）、L_IMP（2）、R_AND（3）、L_AND（4）、R_OR_1（5）、R_OR_2（6）、L_OR（7）、R_NOT（8）、L_NOT（9）、L_CONTR（10）。数据集通过两种分布生成：30% 的硬定理模式（如传递性、假言推理、拒取式等）和 70% 的随机命题语法树（深度 1-3，前件前提 0-4），并通过确定性反向求解器验证（证明深度 ≤8，收缩预算=1）。该数据集适用于训练神经符号定理证明器、策略网络、价值网络以及序列到序列推理模型。The nanoGentzen Synthetic Derivation Dataset (200k transitions) is a formal synthetic dataset designed for automated theorem proving, focusing on Gentzen sequent calculi for intuitionistic logic (LI) and classical logic (LK via Glivenkos theorem). Each record represents a single state-action derivation transition in an AND-OR proof search tree, providing multi-task supervision signals for inference rule selection, antecedent premise localization, and branch provability estimation. The dataset contains 200,000 transition records, available in both PyTorch tensor (.pt) and JSON Lines (.jsonl) formats. Each record includes fields: sample identifier, current sequent (string representation), target inference rule (e.g., AXIOM, R_IMP), rule index (integer category label 0-10), antecedent premise index (pivot, 0-15), branch provability truth value (target_value, 0.0 or 1.0), root theorem (root_sequent), derivation step number, total number of steps, tokenized integer sequence (input_ids), and token length. The rule label mapping covers 11 Gentzen rules: AXIOM (0), R_IMP (1), L_IMP (2), R_AND (3), L_AND (4), R_OR_1 (5), R_OR_2 (6), L_OR (7), R_NOT (8), L_NOT (9), L_CONTR (10). The dataset is generated via two distributions: 30% hard theorem patterns (e.g., transitivity, modus ponens, modus tollens) and 70% random propositional syntax trees (depth 1-3, antecedent premises 0-4), and verified by a deterministic backward solver (proof depth ≤8, contraction budget=1). This dataset is suitable for training neuro-symbolic theorem provers, policy networks, value networks, and sequence-to-sequence reasoning models.

原始信息汇总

数据集概述

nanoGentzen Synthetic Deduction Dataset 是一个用于自动定理证明的形式化合成数据集，专注于直觉主义逻辑（LI）和经典逻辑（LK，通过 Glivenko 定理）的 Gentzen 相继式演算。

基本信息

• 规模: 200,000 条推导转移记录（约 205 MB）
• 语言: 英语
• 许可证: MIT License
• 标注类型: 合成数据（synthetic）
• 任务类别: 文本分类、特征提取
• 标签: 逻辑、Gentzen、相继式演算、直觉主义逻辑、自动定理证明、形式化验证、神经符号

数据文件格式

文件	格式	规模/大小	描述
gentzen_dataset.pt	PyTorch 二进制	200,000 行（~205 MB）	预张量化的训练张量（input_ids、target_rule、target_pivot、target_value）
gentzen_dataset.jsonl	JSON Lines	200,000 条转移记录	包含 AST 相继式和 token 序列的完整推导追踪记录

数据模式与字段定义

每条记录包含用于逆向 Gentzen 证明步骤监督的结构化元数据，字段如下：

• sample_id (int): 训练转移步骤的唯一顺序索引
• sequent (str): 当前 Gentzen 相继式（形式化字符串表示，如 Γ ⟶ Δ）
• rule (str): 目标推导规则（包括 AXIOM, R_IMP, L_IMP, R_AND, L_AND, R_OR_1, R_OR_2, L_OR, R_NOT, L_NOT, L_CONTR）
• rule_idx (int): 规则策略头的离散整数类别标签（0 到 10）
• pivot (int): 左侧规则针对的 Γ 中前提假设的索引（0 到 15）
• target_value (float): 分支可证明性真值，范围 [0.0, 1.0]（1.0 表示在 LI 中可构造性证明，0.0 表示不可证明的反模型）
• root_sequent (str): 推导出该子目标的顶层目标定理
• trace_step (int): 当前逆向归约路径中的步骤编号
• total_trace_steps (int): 完整证明推导的总归约步数
• input_ids (List[int]): 使用 LogicTokenizer 对 sequent 字符串编码生成的 token 化整数序列（映射到 vocab.json）
• token_length (int): 填充前的有效 token 序列长度

规则标签映射

rule_idx	规则符号	名称	形式化相继式归约
0	AXIOM	恒等/爆炸公理	Γ, A ⊢ A 或 0, Γ ⊢ Δ
1	R_IMP	右蕴含	Γ ⊢ (A ⇒ B) ⟹ A, Γ ⊢ B
2	L_IMP	左蕴含	(A ⇒ B), Γ ⊢ Δ ⟹ Γ ⊢ A 和 B, Γ ⊢ Δ
3	R_AND	右合取	Γ ⊢ (A & B) ⟹ Γ ⊢ A 和 Γ ⊢ B
4	L_AND	左合取	(A & B), Γ ⊢ Δ ⟹ A, B, Γ ⊢ Δ
5	R_OR_1	右析取 1	Γ ⊢ (A
6	R_OR_2	右析取 2	Γ ⊢ (A
7	L_OR	左析取	(A
8	R_NOT	右否定	Γ ⊢ ~A ⟹ A, Γ ⊢ 0
9	L_NOT	左否定	~A, Γ ⊢ Δ ⟹ Γ ⊢ A
10	L_CONTR	左收缩	重复假设 Γ[i] 用于多前提定理

生成方法

使用并行 CPU 工作池合成 200,000 个样本，涵盖两种生成分布：

1. 硬定理模式（30% 分布权重）: 固定结构定理模式（传递性、肯定前件、否定后件、构造性德摩根、Glivenko 收缩定理）
2. 随机命题语法树（70% 分布权重）: 深度 1 到 3 递归生成的公式，Γ 中 0 到 4 个前提；通过确定性逆向求解器穷举验证，证明深度预算 ≤ 8，收缩预算 = 1

加载方式

支持三种加载方式：

1. PyTorch 张量加载器 (gentzen_dataset.pt): 直接匹配 train.py 中 DataLoader 的输入字典，张量形状为 input_ids (200000, 256)，target_rule、target_pivot、target_value 形状均为 (200000,)
2. JSON Lines 加载器 (gentzen_dataset.jsonl): 逐行解析 JSON 记录
3. Hugging Face Datasets Hub: 使用 load_dataset("json", data_files="data/gentzen_dataset.jsonl") 加载

设计目标

该数据集专为训练 Policy-Value Transformer 设计，用于自动定理证明，每条记录表示 AND-OR 证明搜索树上的单一状态-动作推导转移，为推理规则选择、前提定位和分支可证明性估计提供多任务监督信号。

搜集汇总

数据集介绍

构建方式

nanoGentzen数据集是一项精心构建的合成演绎数据集，旨在为直觉主义逻辑（LI）与经典逻辑（LK）的自动化定理证明提供策略-价值Transformer的训练监督。该数据集的构建采用了多核并行生成策略，融合了两种分布：其一，30%的样本源自固定结构定理模式，如传递性、肯定前件、否定后件等；其二，70%的样本经由递归生成的命题语法树（深度1至3，前件0至4）产生，并经由确定性回溯求解器验证，确保证明深度不超过8且收缩预算为1。每个记录均代表证明搜索树中单步状态-动作推导转换，为推理规则选择、前件目标定位及分支可证性估计提供了多任务监督信号。

使用方法

数据集的使用灵活便捷，支持多种加载途径。通过PyTorch加载预张量化的.pt文件，可直接获取input_ids（形状200000×256）、target_rule、target_pivot和target_value张量，与标准DataLoader无缝对接。JSON Lines格式则提供了完整的可读元数据，适合数据探索与预处理。此外，借助Hugging Face的datasets库，可一行代码加载JSON文件，快速构建训练集。该数据集适用于训练策略头、价值头或多任务模型，并可用于规则选择预测、前件焦点定位及分支可证性估计等任务，为定理证明的深度学习研究提供坚实数据基础。

背景与挑战

背景概述

nanoGentzen数据集由DigitLib团队于近年构建，旨在推动直觉主义逻辑与经典逻辑的自动定理证明研究。该数据集通过Gentzen相继式演算，为策略-价值Transformer提供了20万条状态-动作推导转换样本，覆盖规则选择、前件定位及分支可证性估计等核心任务。其生成方法融合了固定定理模式与随机命题语法树，经确定性反向求解器验证，确保了数据的高质量与多样性。该数据集的问世，为神经符号AI与形式验证领域提供了标准化的训练基准，显著促进了深度学习在逻辑推理中的应用潜力。

当前挑战

该数据集所面临的挑战主要源于逻辑推理的复杂性与数据构建的精细度。在领域层面，自动定理证明需应对指数级搜索空间与规则选择的歧义，nanoGentzen通过提供细粒度的推导轨迹与分支可证性标签，缓解了策略学习中的稀疏反馈问题。在构建过程中，挑战在于平衡随机生成公式的覆盖度与证明深度限制，确保样本既具代表性又无冗余。此外，数据规模的扩展与多核并行生成的高效协调，以及对经典逻辑通过Glivenko定理进行的间接编码，均要求细致的设计与验证，以维持数据的逻辑一致性与可解释性。

常用场景

经典使用场景

nanoGentzen数据集为自动化定理证明领域提供了一个创新的训练基础，其核心作用在于指导Policy-Value Transformer模型在直觉主义逻辑和经典逻辑（经由Glivenko定理）的Gentzen相继式演算中执行精确的推理步骤。该数据集精心构造的200,000条状态-动作转换记录，涵盖了推理规则选择、前提定位及分支可证性估计等多任务监督信号，为强化学习驱动的证明搜索策略提供了丰富的学习范例。通过利用该数据集，研究人员能够训练模型逐步逼近人类数学家般的推理模式，从而有效推动神经符号方法在形式推理任务上的融合与进步。

解决学术问题

该数据集直面形式逻辑中自动推理的长期挑战，即如何在指数级膨胀的证明搜索空间中高效导航。nanoGentzen通过提供细粒度的逐步推导标签，使模型能够学习判别可证与不可证子目标，从而缓解了传统方法中因盲目搜索带来的计算瓶颈。其设计巧妙地将规则选择视为分类问题，将前提索引视为回归任务，并借助目标值传递可证性概率，这一多任务学习框架显著增强了模型对逻辑结构的深层理解，为解决复杂数学定理的自动化验证提供了切实可行的研究路径和评价基准。

实际应用

在实际应用中，nanoGentzen数据集对于构建智能证明助手和形式验证工具具有重要意义。基于该数据训练的模型可以集成到交互式定理证明器（如Coq、Isabelle）中，辅助用户自动生成证明脚本或提示关键推理步骤，从而大幅提升软件验证和数学形式化的效率。此外，该数据集还可用于教育技术领域，为逻辑学课程提供个性化的推理练习生成与自动反馈。在人工智能安全方面，具备稳健推理能力的模型有助于验证关键系统的逻辑一致性，推动可靠人工智能系统的落地实施。

数据集最近研究

最新研究方向

nanoGentzen数据集作为神经符号形式化验证领域的创新资源，深刻契合了当前自动定理证明与深度学习交叉融合的前沿热潮。该数据集以Gentzen矢列演算为基石，通过200,000条精细的转移轨迹，为策略-价值Transformer提供了多任务监督信号，推动模型在直觉主义逻辑与经典逻辑中习得规则选择、前提定位及分支可证性估计的复合能力。其多核并行生成策略巧妙融合了固定定理模式与随机语法树，不仅保证了数据的覆盖度与挑战性，更强化了模型对深层逻辑结构的泛化表征。该数据集的问世不仅助力于可解释、可验证的神经推理系统的发展，更为形式化数学、程序验证及安全关键系统提供了坚实的数据支撑，标志着智能定理证明迈向数据驱动新范式的关键一步。