nanoGentzen-v2 is a compact 4.86M parameter Bidirectional Policy-Value Network engineered to guide backward proof search in Gentzen’s Intuitionistic Sequent Calculus (LI).

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

Source Code & Training Suite: GitHub - nanoGentzen
Interactive UI: GitHub - nanoGenzen_GUI

NEW: nanoGentzen-MCP experiment available on Github

Core MCP Architectural Principle

Model Architecture & Training Profile

Hyperparameter / Metric	Value	Description
Parameters	4,863,244 (~4.86M)	Lightweight & high-throughput inference
Layers (`n_layer`)	6	Bidirectional Transformer blocks
Attention Heads (`n_head`)	8	Multi-head self-attention
Hidden Size (`n_embd`)	256	Dense token & formula representation
Context Window (`block_size`)	256	Max sequence context
Vocabulary Size	95	Special logic tokens + alphanumeric character alphabet
Action Space (`num_rules`)	11	Complete discrete propositional LI rule set
Pivot Space (`max_antecedents`)	16	Antecedent premise index targeting
Training Split	380k Train / 20k Val	Certified Gentzen derivation transitions
Training Hardware	1× NVIDIA GeForce RTX 4090 (24 GB)	Native `bfloat16` mixed precision
Training Time	61.0 minutes (20 epochs @ ~183s/epoch)	Cosine learning rate decay with linear warmup
Weights Format	`safetensors` & PyTorch	Zero-copy, secure tensor serialization

Training Dynamics (20 Epochs on 400k Certified Transitions):

Loss Convergence (Left): Joint optimization of Rule Policy, Antecedent Pivot, and Branch Provability Value heads. Loss drops steadily from 0.6205 → 0.0105 (Train) and stabilizes at 0.1661 (Val).

Rule Policy Accuracy (Middle): Top-1 rule prediction reaches 98.4% validation accuracy (99.8% train).

Provability Accuracy (Right): Binary value classification achieves 98.9% validation accuracy (99.1% train), providing sharp pruning signals for search tree exploration.

What's New in v2 (Improvements over v1)

nanoGentzen-v2 represents a major architectural, dataset, and tooling upgrade over v0.1, significantly improving search precision, rule classification, and natural language reasoning.

Comparison: v1 vs. v2

Dimension	nanoGentzen	nanoGentzen-v2	Impact
Dataset Scale	200,000 transitions	400,000 transitions (380k / 20k)	2× training data covering deeper proof trees
Rule Policy Acc (Val)	~80.5%	98.4% (99.8% train)	Drastic reduction in exploratory branch backtracking
Provability Acc (Val)	Basic confidence	98.9% (99.1% train)	High-precision value estimation for branch pruning
Validation Loss	0.6550	0.1661 (0.0105 train)	Monotonic multi-task convergence without overfitting
Search Guidance	Heuristic ranking	Joint Policy P(Rule) × P(Pivot)	Integrated value-head pruning for subgoals
NLP Translation	None (Symbolic only)	Built-in NLP Compiler (`parser.py`)	Compiles English syllogisms directly into sequents
Developer Tooling	Single script	`example_usage.py` + `cli.py` + `benchmarks.txt`	Out-of-the-box Python API template, batch testing, and live REPL
Packaging & Hub	Custom loading scripts	Hugging Face `AutoModel` Auto-Map	1-line remote loading via `trust_remote_code=True`

Key Technical Upgrades in Detail

1. High-Accuracy Joint Policy-Value Engine:
- v2 trains the rule head, antecedent pivot head, and value estimator jointly on an expanded 400k transition dataset, boosting Top-1 action accuracy from 80.5% to 98.4%.
- The search engine now prunes branches whose value score indicates provable falsehood before expanding child nodes.
2. Natural Language Deductive Reasoning (parser.py):
- Added recursive parsing for English syllogisms, implication chains, negations, and compound connectives (and, or, if...then, assuming).
- Normalizes non-standard modal verbs, question patterns, and Unicode logic symbols (⊢, →, ⇒, ∧, ∨, ¬) into canonical Gentzen sequents.
3. Comprehensive Validation & Adversarial Suite:
- Variable Invariance (100%): Fully invariant to unseen proposition tokens (Alpha, Beta, Gamma).
- Out-of-Distribution Depth (100%): Zero-shot extrapolation to 4–6 step implication chains.
- Adversarial Fallacy Rejection (100%): Rejects single-token corrupted near-miss fallacies (Affirming the Consequent, Broken Links) and classical non-constructive axioms (Peirce's Law, Law of Excluded Middle).
4. Complete Standalone Tooling:
- example_usage.py: Self-contained script demonstrating programmatic loading via AutoModel and AutoTokenizer for both symbolic and natural language inputs.
- cli.py: Interactive terminal REPL and batch file evaluator supporting single-line queries (-q) and test files (-f).
- benchmarks.txt: 19-sample reference suite testing identity, depth chains, NLP syllogisms, classical non-theorems, and fallacies.
- Standardized 95-token vocabulary serialization (vocab.json) and flat-namespace import resolution for Hugging Face Hub distribution.

System 2 Architecture: `kernel.py`, `search.py`, & `parser.py`

nanoGentzen strictly decouples heuristic action ranking (neural) from logical verification (symbolic). The neural network prioritizes and prunes search paths; the deterministic Gentzen kernel verifies every step to guarantee 100% mathematical soundness.

text

                  [ Natural Language / Symbolic Input ]
                                    │
                                    ▼
   ┌── parser.py: Propositional & Natural Language Compiler
   │   • Compiles English syllogisms & implication chains into sequents
   │   • Normalizes operators (Unicode symbols → ASCII turnstiles)
   └───┬────────────────────────────────────────────────────────────
       │ Sequent: Γ ⊢ Δ
       ▼
   ┌── search.py: Neural Proof Search Controller
   │   • Queries Policy-Value Transformer for Rule, Pivot, and Value
   │   • Prioritizes actions via Joint Policy: P(Rule) × P(Pivot)
   │   • Prunes provably unprovable branches (Value < Threshold)
   └───┬────────────────────────────────────────────────────────────
       │ Candidate (Rule, Pivot)
       ▼
   ┌── kernel.py: Deterministic Gentzen LI Kernel
   │   • apply_rule(seq, rule, idx): Decomposes goal into subgoals
   │   • is_axiom(seq): Checks Identity (A ⊢ A) or Ex Falso (0 ⊢ Δ)
   │   • verify_proof_tree(tree): Recursively certifies 100% soundness
   └────────────────────────────────────────────────────────────────

Evaluation Methodology & Validation Tiers

To rigorously verify that the network learned genuine deduction rather than memorizing surface character patterns, the model is evaluated across four validation dimensions (implemented in validate_random and eval_bench):

Variable Invariance (Isomorphism): Variables are replaced with unseen names (Alpha, Beta, Gamma). Success requires the policy to attend exclusively to operator syntax and structural position.
Depth Out-of-Distribution (OOD): Evaluates formulas of depth 4–6 and 5-step implication chains (the training set focused on depth 1–3) to test structural recursion.
Adversarial Near-Miss Detection: Multi-step theorems are corrupted by exactly one premise token (e.g., Affirming the Consequent, Missing Link). The value head must assign low confidence (< 0.10) and the searcher must refute the goal.
Independent Kernel Verification: Every discovered derivation tree is passed to kernel.py:verify_proof_tree() to ensure zero false positives and 100% mathematical soundness.

Empirical Benchmark & Generalization Results

1. Generalization & Adversarial Evaluation (`validate_random`)

Evaluation Tier	Test Description	Score	Result
Variable Invariance	Testing unseen variable names (`Alpha`, `Beta`, `Gamma`)	3/3	100.0% (Invariant)
Depth Extrapolation	Implication chains of depth 4–6 and multi-step subgoals	3/3	100.0% (Passed)
Adversarial Fallacies	1-token near-miss fallacies (Missing link, Broken chain)	4/4	100.0% (Rejected)
Classical Non-Theorems	Refuting non-constructive axioms (LEM, Peirce's Law)	2/2	100.0% (Rejected)
Kernel Soundness	Formal verification of generated positive proofs	100%	100.0% Sound

2. Canonical Constructive Benchmarks (`eval_bench`)

Proposition / Theorem	Sequent	Status	Average Latency
Identity	`⊢ P ⇒ P`	PROVEN	147.67 ms
Conjunction Intro	`P, Q ⊢ P ∧ Q`	PROVEN	3.88 ms
Transitivity	`(P ⇒ Q), (Q ⇒ R) ⊢ (P ⇒ R)`	PROVEN	11.06 ms
Constructive De Morgan	`¬(P ∨ Q) ⊢ (¬P ∧ ¬Q)`	PROVEN	25.19 ms
Law of Excluded Middle	`⊢ (P ∨ ¬P)`	REFUTED (LI Invalid)	13.47 ms

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

bash

pip install torch safetensors huggingface_hub transformers

2. Inference via Hugging Face Hub (`trust_remote_code=True`)

python

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

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

# 1. Load Model & Tokenizer
model = AutoModel.from_pretrained("Sagicc/nanoGentzen-v2", trust_remote_code=True).to(device)
tokenizer = AutoTokenizer.from_pretrained("Sagicc/nanoGentzen-v2", trust_remote_code=True)
searcher = NeuralProofSearch(model, tokenizer, device=device)

# 2. Example 1: Symbolic Transitivity [(P => Q), (Q => R) |- (P => R)]
P, Q, R = Var("P"), Var("Q"), Var("R")
seq1 = Sequent((Imp(P, Q), Imp(Q, R)), (Imp(P, R),))
proof1 = searcher.prove(seq1, max_depth=8)
print(f"Proof 1 Sound: {verify_proof_tree(proof1)}")

# 3. Example 2: Natural Language Syllogism
nl_prompt = "If it rains and it is windy, then power goes out. It rains. It is windy. Does power go out?"
seq2, _ = parse_natural_language(nl_prompt)
proof2 = searcher.prove(seq2, max_depth=8)
print(f"Proof 2 Sound: {verify_proof_tree(proof2)}")

3. Interactive CLI Prover & Batch Evaluation

Run the interactive logic terminal directly or test batch benchmarks:

bash

# Start interactive shell
python cli.py

# Evaluate a single prompt
python cli.py -q "Assuming A and B then C. A. B. Is C?"

# Batch evaluate the included benchmark suite
python cli.py -f benchmarks.txt

Scope & Guarantees

Mathematical Soundness (0% Hallucinations): Evaluates deductive entailment in single-succedent Gentzen Sequent Calculus (LI). Proof trees verify axiomatically against the formal kernel.
Constructive Logic: Validates constructive proofs. Classical tautologies that lack computational witnesses (such as Double Negation Elimination ¬¬P ⊢ P) are soundly refuted.
Propositional vs First-Order Arithmetic: Operates on propositional formulas. Quantified First-Order Logic (∀x, ∃y) and continuous arithmetic inequalities are outside the discrete propositional action space.

License

This project is released under the MIT License.

Sagicc/nanoGentzen-v2

nanoGentzen-v2: Neural-Guided Automated Theorem Prover for Intuitionistic Logic