nanoGentzen: Neural-Guided Automated Theorem Prover for Intuitionistic Logic

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

Hyperparameter / Metric	Value	Description
Parameters	4,861,185 (~4.86M)	Lightweight & ultra-fast inference
Layers (n_layer)	6	Bidirectional Transformer blocks
Attention Heads (n_head)	8	Multi-head self-attention
Hidden Size (n_embd)	256	Dense token & graph representation
Block Size (block_size)	256	Max sequence context
Rule Space (num_rules)	11	Complete discrete propositional LI action space
Pivot Space (max_antecedents)	16	Antecedent premise index targeting
Training Hardware	1× NVIDIA GeForce RTX 4090 (24 GB)	Native bfloat16 mixed precision
Peak VRAM Usage	11.0 GB / 24.0 GB	High-throughput training with batch size 256
Total Training Time	30.5 minutes (20 epochs @ ~91.5s/epoch)	Cosine learning rate decay with linear warmup
Weights Format	safetensors & .pt	Zero-copy, secure tensor serialization

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.

Search Phase	Function / Module	Operational Role	Output
1. Action Proposal	search.py:rank_actions()	Neural inference + structural connective filter	Prioritized (rule, pivot) list
2. Reduction	kernel.py:apply_rule()	Backward sequent decomposition	Child sub-goal sequents
3. AND-OR Search	search.py:prove()	Recursive branch evaluation + cycle guard	Proof tree dictionary
4. Certification	kernel.py:verify_proof_tree()	Independent mathematical soundness verification	Soundness status (True/False)

---

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:

Metric	Result	Benchmark Target
Overall Accuracy	99.00%	> 90.0%
Soundness (Precision)	100.00% (0 Hallucinations)	100.0% (Kernel Guarantee)
Completeness (Recall)	98.00% (49/50 Provable Goals)	> 90.0%
Average Proof Latency	9.97 ms / proof	< 25.0 ms
Kernel Soundness Verification	49 / 49 (100% Sound Trees)	100.0%

Constructive Benchmark Suite

Proposition / Theorem	Sequent	Status
Identity	P ⊢ P	PROVEN
Modus Ponens	P, (P ⇒ Q) ⊢ Q	PROVEN
Conjunction Intro	P, Q ⊢ (P ∧ Q)	PROVEN
Transitivity	(P ⇒ Q), (Q ⇒ R) ⊢ (P ⇒ R)	PROVEN
Constructive De Morgan	¬(P ∨ Q) ⊢ (¬P ∧ ¬Q)	PROVEN
Contraction Double Negation	⊢ ¬¬(¬¬P ⇒ P)	PROVEN (Requires Contr_L)
Law of Excluded Middle	⊢ (P ∨ ¬P)	REFUTED (Invalid in Intuitionistic Logic LI)

---

Action Space & Supported Gentzen Rules (LI)

Rule ID	Rule Symbol	Name	Description
0	AXIOM	Identity Axiom	Γ, A ⊢ A
1	R_IMP	Right Implication (→_R)	Γ ⊢ (A ⇒ B) ⟹ A, Γ ⊢ B
2	L_IMP	Left Implication (→_L)	(A ⇒ B), Γ ⊢ Δ ⟹ Γ ⊢ A and B, Γ ⊢ Δ
3	R_AND	Right Conjunction (∧_R)	Γ ⊢ (A ∧ B) ⟹ Γ ⊢ A and Γ ⊢ B
4	L_AND	Left Conjunction (∧_L)	(A ∧ B), Γ ⊢ Δ ⟹ A, B, Γ ⊢ Δ
5	R_OR_1	Right Disjunction 1 (∨_R1)	Γ ⊢ (A ∨ B) ⟹ Γ ⊢ A
6	R_OR_2	Right Disjunction 2 (∨_R2)	Γ ⊢ (A ∨ B) ⟹ Γ ⊢ B
7	L_OR	Left Disjunction (∨_L)	(A ∨ B), Γ ⊢ Δ ⟹ A, Γ ⊢ Δ and B, Γ ⊢ Δ
8	R_NOT	Right Negation (¬_R)	Γ ⊢ ¬A ⟹ A, Γ ⊢ 0
9	L_NOT	Left Negation (¬_L)	¬A, Γ ⊢ Δ ⟹ Γ ⊢ A
10	L_CONTR	Left Contraction (Contr_L)	Duplicate hypothesis for multi-use premises

|

---

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.