nanoGentzen

nanoGentzen: Neural-Guided Automated Theorem Prover for Intuitionistic Logic

NOTE: Use v2 model

nanoGentzen is a compact, high-efficiency neural policy-value transformer model trained to guide Gentzen Sequent Calculus (LI) backward proof search.

The model evaluates intuitionistic logical sequents Γ ⊢ Δ (|Δ| ≤ 1), predicting which deduction rule to apply, which premise antecedent to select, and estimating the sound provability value of the branch in [0, 1].

---

Complete training code is available on GitHub

Streamlit App for 100% local testing is available on GitHub nanoGenzen_GUI

---

Model Architecture & Hardware Profile

Training Dynamics Overview (20 Epochs on 200k Certified Transitions):

• Multi-Task Loss Convergence (Left): Joint optimization of Rule Policy (Cross-Entropy), Pivot Selection (Cross-Entropy), and Branch Provability Value (MSE). Shows monotonic convergence (Train: 1.042 → 0.575, Val: 0.861 → 0.655) with zero validation divergence across complex multi-branch proof states.
• Rule Action Top-1 Accuracy (Right): Discrete Gentzen rule classification rapidly climbs in epochs 1–4 and stabilizes at ~80.5% validation accuracy (82.6% train), providing over 98% Top-3 action coverage to effectively guide heuristic beam pruning during AND-OR proof search.

---

System 2 Engine Deep Dive: kernel.py & search.py

nanoGentzen strictly separates heuristic action ranking (neural) from logical verification (symbolic). The neural model proposes search steps; the kernel validates each transition and guarantees 100% soundness.

                     [ Sequent: Γ ⊢ Δ ]
                             │
                             ▼
 ┌─────────────────────────────────────────────────────────────┐
 │ search.py: Neural Proof Search Controller                   │
 │  1. Tokenizes sequent and queries Policy-Value Transformer  │
 │  2. Ranks candidate Gentzen rules by probability            │
 │  3. Prunes structurally invalid rules (e.g., R_IMP without ⇒) │
 └─────────────────────────────┬───────────────────────────────┘
                               │ Candidate Rule & Pivot Index
                               ▼
 ┌─────────────────────────────────────────────────────────────┐
 │ kernel.py: Deterministic Gentzen Kernel                     │
 │  1. apply_rule(seq, rule, idx): Decomposes goal into subgoals│
 │  2. is_axiom(seq): Checks Identity (A ⊢ A) or Ex Falso      │
 │  3. verify_proof_tree(tree): 100% Soundness Certification    │
 └─────────────────────────────────────────────────────────────┘

1. kernel.py — Deterministic Gentzen LI Kernel

The symbolic foundation of the prover. Implements propositional Abstract Syntax Trees (AST), sequent manipulation, and inverse Gentzen rule decompositions.

• Formula (Base AST Node): Immutable base class implemented by Var (atomic propositions), Not (~A), And (A & B), Or (A | B), and Imp (A => B).

• Sequent (gamma: Tuple, delta: Tuple): Represents the Gentzen judgment Γ ⊢ Δ. The single-succedent restriction (|Δ| ≤ 1) enforces constructive Intuitionistic Logic (LI).

• Sequent.is_axiom(): Base-case check. Returns True if any antecedent matches the succedent (Γ, A ⊢ A, Identity Axiom) or if Falsum appears in the premises (0, Γ ⊢ Δ, Ex Falso Quodlibet).

• apply_rule(seq, rule, idx=0): Backward rule applicator. Decomposes a sequent into required premises:

• Right Rules (R_IMP, R_AND, R_OR_1, R_OR_2, R_NOT) decompose the succedent formula in Δ.

• Left Rules (L_IMP, L_AND, L_OR, L_NOT) decompose the antecedent premise Γ[idx].

• Contraction (L_CONTR) duplicates hypothesis Γ[idx] for multi-premise Glivenko classical proofs.

• verify_proof_tree(tree): Standalone proof checker. Recursively verifies that every leaf node terminates in AXIOM and all branch reductions are valid.

2. search.py — Neural-Guided AND-OR Tree Search

Combines the policy-value network predictions with search budgeting, cycle detection, and memoization.

• rank_actions(seq): Runs neural inference to rank the 11 Gentzen rules (rule_logits) and 16 antecedent pivots (pivot_logits). Filters out rules whose target connectives are missing (e.g., skips R_NOT if Δ is not a negation).

• prove(seq, depth, max_depth, budget, memo, path_visited):

1. Axiom Check: Immediate base-case termination via seq.is_axiom().

2. Cycle Guard: Tracks current path in path_visited to prevent infinite contraction loops.

3. Transposition Memoization: Caches intermediate results in memo to avoid redundant sub-proof searches.

4. AND-Branching: Recursively ensures that all sub-goals of branching rules (R_AND, L_OR, L_IMP) close before declaring the step proven.

---

Training Convergence & Metrics

The model was trained on 200,000 certified Gentzen backward derivation transitions synthesized across multi-depth propositional logic formulas and structural constructive schemas.

• Multi-Task Loss Convergence: Steady, simultaneous decline in training (1.042 → 0.575) and validation loss (0.861 → 0.655) confirming zero overfitting across complex multi-branch sequents.

• Top-1 Action Accuracy: Reached 82.5% on deterministic target paths, providing >98% Top-3 coverage for neural heuristic beam ranking.

---

Empirical Benchmark & Validation Results

Evaluated on a balanced test distribution of certified constructive theorems, classical fallacies, and unprovable sequents:

Constructive Benchmark Suite

---

Action Space & Supported Gentzen Rules (LI)

|

---

Quickstart & Usage

1. Installation

pip install torch safetensors huggingface_hub transformers

2. Loading with Hugging Face from_pretrained

import torch
from transformers import AutoModel, AutoTokenizer
from kernel import Sequent, Imp, And, Var, verify_proof_tree
from search import NeuralProofSearch

device = "cuda" if torch.cuda.is_available() else "cpu"

# Load model and tokenizer from Hugging Face Hub
model = AutoModel.from_pretrained("Sagicc/nanoGentzen", trust_remote_code=True).to(device)
tokenizer = AutoTokenizer.from_pretrained("Sagicc/nanoGentzen", trust_remote_code=True)

# Initialize neural proof searcher
searcher = NeuralProofSearch(model, tokenizer, device=device)

# Define a goal: Modus Ponens [ P, (P => Q) |- Q ]
P, Q = Var("P"), Var("Q")
goal = Sequent((P, Imp(P, Q)), (Q,))

# Search for certified Gentzen proof tree
proof_tree = searcher.prove(goal, max_depth=8)

if proof_tree:
    print(f"Goal proved successfully: {goal.to_str()}")
    print(f"Kernel Certified Sound: {verify_proof_tree(proof_tree)}")
    print(f"Proof Tree: {proof_tree}")

3. Direct Loading via PyTorch / Safetensors

import json
import torch
from safetensors.torch import load_file
from configuration_nanogentzen import GentzenConfig
from modeling_nanogentzen import GentzenPolicyValueModel
from tokenization_nanogentzen import LogicTokenizerHF

# Initialize Tokenizer & Model
tokenizer = LogicTokenizerHF(vocab_file="vocab.json")

with open("config.json", "r") as f:
    cfg = json.load(f)

config = GentzenConfig(**{k: v for k, v in cfg.items() if k not in ["architectures", "auto_map", "model_type", "torch_dtype"]})
model = GentzenPolicyValueModel(config)
model.load_state_dict(load_file("model.safetensors"))
model.eval()

# Forward Inference
text = "P, (P => Q) |- Q"
inputs = tokenizer(text, return_tensors="pt")
with torch.no_grad():
    rule_logits, pivot_logits, value, _ = model(inputs["input_ids"])

print("Predicted Rule ID:", rule_logits.argmax(dim=-1).item())
print("Provability Value:", value.item())

---

⚠️ Scope, Mathematical Guarantees & Known Limitations

1. Deductive Validity vs. Empirical Grounding

• What nanoGentzen Guarantees (100% Soundness): nanoGentzen evaluates formal deductive validity. Given a set of premises Γ, it mathematically guarantees that conclusion Δ follows without structural fallacies (e.g., Affirming the Consequent, circular dependencies, or invalid contraposition) with a 0.00% hallucination rate.

• What Requires External Domain Axioms (Physical & Empirical Facts): nanoGentzen is a formal logical reasoner, not an empirical physics simulator or arithmetic SMT solver.

• Example (The Submerged Anchor Trap): If an LLM adopts a flawed physical premise (e.g., "an anchor inside a floating boat displaces its geometric volume rather than its mass"), the internal reasoning is structurally consistent, but the physical premise violates fluid dynamics.

• Example (The Mirror Reflection Trap): If an LLM constructs an argument around a false coordinate transformation (x -> -x instead of z -> -z), the deduction may be formally valid, but the optical model is factually inaccurate.

2. Propositional Logic vs. First-Order Arithmetic

• nanoGentzen operates over the Propositional Gentzen Sequent Calculus (LI).

• Quantified First-Order Logic (∀x, ∃y) and continuous non-linear arithmetic inequalities (x² + y² ≤ r²) are outside the discrete propositional action space and are best complemented with SMT solvers (such as Z3).

---

License

This project is released under the MIT License.