Sagicc/nanoGentzen-v2

nanoGentzen-v2 Synthetic Deduction Dataset (400k Transitions)

The nanoGentzen-v2 Dataset is a formal synthetic corpus designed to train Policy-Value Transformers for automated theorem proving in Intuitionistic Propositional Logic (LI) using Gentzen Sequent Calculus.

Scaled to 400,000 certified state-action derivation transitions, each record represents a discrete backward proof step along an AND-OR search tree. The dataset provides balanced multi-task supervision for inference rule selection, antecedent premise targeting, and branch provability value estimation.

Code & Generation Pipeline: GitHub - nanoGentzen

Model Checkpoint: Hugging Face - nanoGentzen-v2

Dataset Balance & Key Statistics

The dataset is constructed with a balanced 50/50 binary provability distribution to eliminate value-head bias during proof search:

File Formats & Artifacts

Data Schema & Field Definitions

Each record in gentzen_dataset.jsonl contains structured metadata for backward Gentzen proof step supervision:

{
  "sample_id": 10482,
  "sequent": "(P => Q), (Q => R) ⟶ (P => R)",
  "rule": "R_IMP",
  "rule_idx": 1,
  "pivot": 0,
  "target_value": 1.0,
  "root_sequent": "(P => Q), (Q => R) ⟶ (P => R)",
  "trace_step": 1,
  "total_trace_steps": 5,
  "input_ids": [2, 64, 22, 6, 22, 65, 23, 24, 22, 65, 22, 6, 22, 66, 23, 22, 5, 22, 64, 22, 6, 22, 66, 23, 4],
  "token_length": 25
}

Field Descriptions:

• —`sample_id` (int): Unique sequential index for the derivation transition.

• —`sequent` (str): The active Gentzen sequent in string notation (Γ ⟶ Δ or Gamma |- Delta).

• —`rule` (str): Target deduction rule to apply (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): Discrete integer class label for the Rule Policy Head (0 to 10; -100 for unprovable negative samples).

• —`pivot` (int): Index of the targeted antecedent premise in Γ (0 to 15; -100 if right-side rule or unprovable).

• —`target_value` (float): Branch provability ground truth in [0.0, 1.0] (1.0 = provable in LI, 0.0 = unprovable counter-model or fallacy).

• —`root_sequent` (str): The top-level goal theorem from which this sub-goal was derived.

• —`trace_step` (int): Step index along the active backward derivation path.

• —`total_trace_steps` (int): Total steps required to close the full proof tree.

• —`input_ids` (List[int]): Tokenized integer sequence mapped via vocab.json (95-token vocabulary).

• —`token_length` (int): Active sequence length before batch padding.

Action Space & Rule Classification (rule_idx)

Generation Methodology & Sampling Distribution

The 400,000 transitions were synthesized using parallel CPU worker pools across three generative distributions:

1. 1.Hard Theorem Schemas (35% Distribution Weight):
2. 2.Multi-step constructive schemas (Transitivity, Modus Tollens, Constructive De Morgan, Glivenko Double Negation theorems).

1. 1.Random Propositional Syntax Trees (50% Distribution Weight):
2. 2.Recursively sampled propositional trees across depths 1 to 4 with 0 to 6 antecedent premises in Γ.

• —Solved and certified via deterministic backward Gentzen solver with depth budget ≤ 10.

1. 1.Adversarial & Unprovable Counter-Models (15% Distribution Weight):
2. 2.1-token near-miss fallacies (Affirming the Consequent, Denying the Antecedent, broken implication chains) and classical non-theorems (LEM, Peirce's Law).
3. 3.Supervised with target_value = 0.0 and masked policy targets (-100) to train value-head pruning.

How to Load the Dataset

1. PyTorch Binary Tensor Loader (.pt)

Directly matches the DataLoader pipeline used during training:

import torch

data = torch.load("gentzen_dataset.pt", weights_only=False)

input_ids = data["input_ids"]        # Shape: (400000, 256)
target_rule = data["target_rule"]    # Shape: (400000,)
target_pivot = data["target_pivot"]  # Shape: (400000,)
target_value = data["target_value"]  # Shape: (400000,)

print(f"Loaded {input_ids.shape[0]:,} training steps.")
print("Sample Sequent Tensor:", input_ids[0][:12])
print("Target Rule Label    :", target_rule[0].item())
print("Target Value Label   :", target_value[0].item())

2. JSON Lines Loader (.jsonl)

import json

samples = []
with open("gentzen_dataset.jsonl", "r", encoding="utf-8") as f:
    for line in f:
        samples.append(json.loads(line))

print(f"Total parsed records: {len(samples):,}")
print("Transition 0:", samples[0]["sequent"], "⟶ Target Rule:", samples[0]["rule"])

3. Hugging Face Datasets Hub

from datasets import load_dataset

dataset = load_dataset("Sagicc/nanoGentzen-v2", split="train")
print(dataset[0])

License

This dataset is released under the MIT License.