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

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 ClearCoT Studio available on Github

nanoGentzen ClearCoT Studio is a 100% local dataset factory and GUI application for transforming unstructured documents (PDFs, technical papers, domain manuals, monographs) into logically verified ClearCoT datasets in strict Q–R–A format (Question – Reasoning – Answer).

More about ClearCot on Sagicc/Occam-2B-CCoT

NEW: nanoGentzen-MCP experiment available on Github

Core MCP Architectural Principle

Model Architecture & Training Profile

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

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.

                  [ 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):

1. 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.
2. 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.
3. 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.
4. 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)

2. Canonical Constructive Benchmarks (eval_bench)

Action Space: Supported Gentzen Rules (LI)

Quickstart & Usage

1. Installation

pip install torch safetensors huggingface_hub transformers

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

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:

# 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.