Sagicc/nanoGentzen

nanoGentzen Synthetic Deduction Dataset (200k Transitions)

The nanoGentzen Dataset is a formal synthetic dataset designed to train Policy-Value Transformers for automated theorem proving in Intuitionistic Logic (LI) and Classical Logic (LK via Glivenko's Theorem) using Gentzen Sequent Calculus.

Each record represents a single state-action derivation transition along an AND-OR proof search tree, providing multi-task supervision for inference rule selection, antecedent premise targeting, and branch provability estimation.

Complete code for train workflow is available on GitHub

Dataset generation link

File Formats & Artifacts

Data Schema & Field Definitions

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

{
  "sample_id": 1,
  "sequent": "Q ⟶ (Q | P)",
  "rule": "R_OR_1",
  "rule_idx": 5,
  "pivot": 0,
  "target_value": 1.0,
  "root_sequent": "Q ⟶ (Q | P)",
  "trace_step": 1,
  "total_trace_steps": 2,
  "input_ids": [65, 22, 5, 22, 84, 65, 22, 8, 22, 64, 85],
  "token_length": 11
}

Field Descriptions:

• —`sample_id` (int): Unique sequential index for the training transition step.
• —`sequent` (str): The current Gentzen sequent in formal 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).
• —`pivot` (int): Index of the antecedent hypothesis in Γ targeted by left-side rules (0 to 15).
• —`target_value` (float): Branch provability ground truth in [0.0, 1.0] (1.0 = constructively provable in LI, 0.0 = unprovable counter-model).
• —`root_sequent` (str): The top-level goal theorem from which this sub-goal was derived.
• —`trace_step` (int): Step number in the active backward reduction path.
• —`total_trace_steps` (int): Total number of reduction steps in the complete proof derivation.
• —`input_ids` (List[int]): The tokenized integer sequence generated by encoding the sequent string with LogicTokenizer (mapped against vocab.json)[cite: 4, 6].
• —`token_length` (int): Length of the active token sequence before padding. ---

Gentzen Rule Label Mapping (rule_idx)

Multi-Core Generation Methodology

The 200,000 samples were synthesized using parallel CPU worker pools across two generative distributions:

1. 1.Hard Theorem Schemas (30% Distribution Weight):
2. 2.Fixed structural theorem patterns (Transitivity, Modus Ponens, Modus Tollens, Constructive De Morgan, Glivenko Contraction theorems).

1. 1.Random Propositional Syntax Trees (70% Distribution Weight):
2. 2.Recursively generated formulas across depths 1 to 3 with 0 to 4 antecedent premises in Γ.
3. 3.Exhaustively verified via deterministic backward solver with proof depth budget ≤ 8 and contraction budget = 1.

How to Load the Dataset

1. PyTorch Training Tensor Loader (.pt)

Directly matches the DataLoader input dictionary used in train.py:

import torch

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

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

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())

2. JSON Lines Loader (.jsonl)

import json

samples = []
with open("data/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"], "⟶ Apply:", samples[0]["rule"])

3. Hugging Face Datasets Hub

from datasets import load_dataset

dataset = load_dataset("json", data_files="data/gentzen_dataset.jsonl")
print(dataset["train"][0])

License

This dataset is released under the MIT License.