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].
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
nanoGentzen Training Curves
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.
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.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).
Axiom Check: Immediate base-case termination via seq.is_axiom().
Cycle Guard: Tracks current path in path_visited to prevent infinite contraction loops.
Transposition Memoization: Caches intermediate results in memo to avoid redundant sub-proof searches.
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:
⚠️ 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).
