nanoGentzen-v3: Neuro-Symbolic Typed-Decision Engine (4.93M Params)

nanoGentzen-v3 is a 4.93M parameter (4,927,812 params) Neuro-Symbolic Formal Decision Engine that unifies a Bidirectional RoPE Policy-Value Transformer with Gerhard Gentzen (1935) Intuitionistic Sequent Calculus (LJ) and Roy Dyckhoff (1992) Contraction-Free Proof Search (G4ip).

It delivers certified, mathematically explainable decisions across arbitrary JSON states, numeric/regex predicates, natural language policies, and rubric criteria without hallucination:

• Saul Kripke (1965) 3-Class Epistemic Valuation: Classifies sequents into PROVEN_FALSE (0.0), INTUITIONISTIC_UNDECIDED (0.5), and PROVEN_TRUE (1.0) in < 1.5 ms.
• Intuitionistic Relevance Logic (IR) Witness Tracking: Isolates causal premises actively exercised in derivation from unused distractor facts.
• Curry-Howard Typed λ-Term Serialization: Generates verifiable 1-line mathematical certificates (apply(pair(A, B))) isomorphic to the verified proof tree DAG.
• Dual-System Execution: System 1 fast neural forward pass (~780 decisions/sec, < 1.3 ms latency) + System 2 deductive proof search and post-verification calibration.
• S1MB Compliant: Evaluated across all 137 benchmarks in S1MB-english-v1 (26,269 decisions, 100% valid).
• Typed Decisions: Outperforms large language models up to 35B parameters and surpasses the Teacher Consensus Ceiling with 76.75% accuracy on LocalLLaMA/typed-decisions (400 cases, 2,000 decisions).

---

NOTE: This is development phase. Any feedback is wellcome.

---

Benchmark Results

1. S1MB English-v1 Benchmark (137 Benchmarks, 26,269 Decisions)

nanoGentzen-v3 was evaluated on the official S1MB System One Benchmark (english-v1) with 100% coverage and zero failures:

Key Highlights on S1MB:

• Score Task (#183 out of 212 on Leaderboard): System 2 achieved 2.50, outperforming 29 published models on the official leaderboard, including:
  • CLM-v0.1-8B (7.6B params, Score: 1.19) — nanoGentzen is >1,500× smaller!
  • JevK5-Lite (437M params, Score: 1.57)
  • Verdict ModernBERT 151M (151M params, Score: 1.57)
  • LFM2.5-350M-RLCD (354M params, Score: 1.26)
  • gliner2.5-small-v1 (74M params, Score: 0.86)
• laya--typed-decisions Performance:
  • laya--typed-decisions-score: 52.52 (+11.22 points boost from System 2 deductive verification).
  • laya--typed-decisions-noul: 44.00 (72.0% balanced accuracy).
  • laya--typed-decisions-choice: 30.96 (49.1% target mass).
  • Typed Decisions Domain Average: 42.49 (~10× higher than open-domain text averages).
• Overall Task Avg: At 4.42, beats 8 published models between 120M and 600M parameters (DM-JEPA, MXBAI Rerank, gliner2.5, mini-Jev, LFM2.5, GTE ModernBERT, Needle 3, certo).

---

2. LocalLLaMA/typed-decisions (400 Cases, 2,000 Decisions)

(Evaluated on the full 400-case / 2,000-decision test split from LocalLLaMA/typed-decisions).

Per-Workflow Breakdown (500 Decisions Each)

---

Dual Decision APIs

nanoGentzen-v3 exposes two complementary modes, available in Python via AutoModel and over HTTP via jev_server.py:

---

Quickstart

Installation

pip install torch transformers safetensors fastapi uvicorn pydantic

Python API (AutoModel & AutoTokenizer)

import json
import torch
from transformers import AutoModel, AutoTokenizer

# Load model and tokenizer directly from HuggingFace
model = AutoModel.from_pretrained("Sagicc/nanoGentzen-v3", trust_remote_code=True)
if torch.cuda.is_available():
    model = model.cuda()
model.eval()

# Enterprise loan approval decision payload
payload = {
    "model": "nanoGentzen-v3",
    "state": {
        "applicant": {"income": 95000, "credit_score": 740, "employment_years": 4},
        "loan": {"amount": 250000, "purpose": "mortgage"},
    },
    "predicates": {
        "high_income": {"field": "applicant.income", "op": ">=", "value": 70000},
        "good_credit": {"field": "applicant.credit_score", "op": ">=", "value": 700},
        "stable_job": {"field": "applicant.employment_years", "op": ">=", "value": 2},
    },
    "policy_rules": [
        "high_income & good_credit => creditworthy",
        "creditworthy & stable_job => approve_loan",
        "approve_loan => tier_premium",
    ],
    "questions": {
        "approve_loan": {
            "type": "noul",
            "target": "approve_loan",
            "require_relevance": True,
        },
        "routing_action": {
            "type": "choice",
            "options": ["tier_premium", "tier_standard", "tier_reject"],
        },
        "risk_tier": {
            "type": "score",
            "levels": [0, 1, 2, 3],
        },
    },
}

# Run System 2 verified formal proof search
res = model.decide(payload)
print(f"Latency: {res['latency_ms']} ms")
print(f"Decision: {res['answers']['approve_loan']['verification']}")
print(f"Curry-Howard Proof Term: {res['answers']['approve_loan']['curry_howard_term']}")
print(f"Relevant Witnesses: {res['answers']['approve_loan']['relevance']['relevant_witnesses']}")

Production REST API Server (jev_server.py)

Launch the standalone server:

python jev_server.py --port 8000

Query the server with curl:

curl -s -X POST http://127.0.0.1:8000/v1/decide \
  -H "Content-Type: application/json" \
  -d '{
    "model": "nanoGentzen-v3",
    "state": {"is_adult": true, "kyc_passed": true},
    "policy_rules": ["(is_adult & kyc_passed) => approved"],
    "questions": {"approved": {"type": "noul", "target": "approved"}}
  }' | jq .

Output:

{
  "model": "nanoGentzen-v3",
  "mode": "system_two_verified",
  "latency_ms": 1.2,
  "usage": {
    "input_tokens": 14,
    "output_tokens": 16,
    "requests": 1,
    "retries": 0
  },
  "answers": {
    "approved": {
      "type": "noul",
      "answer": true,
      "noul": 1.0,
      "verification": "PROVEN_TRUE",
      "confidence": 1.0,
      "probabilities": {"false": 0.0, "true": 1.0},
      "epistemic": {"false": 0.0, "undecided": 0.0, "true": 1.0},
      "relevance": {
        "relevant_witnesses": ["is_adult", "kyc_passed", "((is_adult & kyc_passed) => approved)"],
        "unused_premises": [],
        "is_strictly_relevant": true,
        "relevance_ratio": 1.0
      },
      "curry_howard_term": "apply(pair(is_adult, kyc_passed))",
      "proof_tree": {
        "sequent": "is_adult, kyc_passed, ((is_adult & kyc_passed) => approved) |- approved",
        "rule": "L_IMP_2",
        "branches": []
      }
    }
  }
}

Command Line Interface (cli.py)

python cli.py --state '{"age": 25}' --goal is_adult --rules 'age >= 18 => is_adult'

CPU Execution & Low-Resource Deployment

nanoGentzen-v3 is designed to run efficiently on standard x86 and ARM CPUs without requiring an NVIDIA GPU or CUDA drivers. Because the model contains only 4.93M parameters (~19.6 MB weights in model.safetensors), it has an ultra-compact memory footprint (< 150 MB total RAM).

Tested CPU Latency & Resource Footprint

1. In Python with AutoModel:

import torch
from transformers import AutoModel, AutoTokenizer

# Load directly onto CPU
model = AutoModel.from_pretrained("Sagicc/nanoGentzen-v3", trust_remote_code=True).to("cpu")
tokenizer = AutoTokenizer.from_pretrained("Sagicc/nanoGentzen-v3")

2. In Python with ProductionGentzenEngine:

from jev_server import ProductionGentzenEngine

# Force CPU execution
engine = ProductionGentzenEngine(device="cpu")

3. Via CLI & REST Server:

# Run CLI decision on CPU
python cli.py --device cpu --state '{"age": 25}' --goal is_adult --rules 'age >= 18 => is_adult'

# Run REST server on CPU
DEVICE=cpu python jev_server.py --port 8000
# Or by setting CUDA_VISIBLE_DEVICES empty:
CUDA_VISIBLE_DEVICES="" python jev_server.py --port 8000

Target Deployment Environments:

• Serverless & Edge: AWS Lambda, Google Cloud Run, Cloudflare Workers, Azure Functions.
• Micro-containers: Minimal Alpine / Debian Docker containers without NVIDIA Container Toolkit.
• Developer Machines & Embedded: Local laptops (macOS / Linux / Windows) and IoT/edge devices (Raspberry Pi, industrial gateways).

---

Theoretical Foundations

1. Saul Kripke (1965) Epistemic Semantics

In intuitionistic logic, a proposition is not simply assigned true or false by default (the classical Law of Excluded Middle, P ∨ ¬P, is not universally assumed). Truth requires constructive evidence. An intuitionistic Kripke frame is a partially ordered set of epistemic stages:

$$ \mathcal{M} = \langle W, \le, \Vdash \rangle $$

Where W is a set of epistemic worlds, ≤ is a preorder representing monotonic evidence accumulation, and ⊩ is the intuitionistic satisfaction relation. nanoGentzen-v3 models sequents across three epistemic states:

• Class 2 (PROVEN_TRUE, V = 1.0): Constructively proved at origin world w₀.
• Class 1 (INTUITIONISTIC_UNDECIDED, V = 0.5): Underdetermined; satisfiable in some future world w' ≥ w₀, but unproven at present due to missing facts or non-constructive classical tautologies (e.g. Law of Excluded Middle). Produces an explicit 2-world countermodel (G ≤ H).
• Class 0 (PROVEN_FALSE, V = 0.0): Refuted; deriving the goal leads to absurdity (Γ ⊢ ¬Δ or Γ, Δ ⊢ ⊥).

2. Intuitionistic Relevance Logic (IR)

In standard sequent calculus, the structural rule of Weakening allows irrelevant facts to accumulate in the antecedent Γ. In enterprise governance, decisions should not pass based on extraneous background noise. The IR tracker walks the verified derivation DAG and isolates:

• relevant_witnesses: The exact causal premises used at identity axiom leaves.
• unused_premises: Distractor facts present in state but unreferenced in proof.
• is_strictly_relevant: Enforces that no unnecessary premises were included.

3. Curry-Howard Typed λ-Calculus Isomorphism

Under the Curry-Howard correspondence, every intuitionistic proof tree is isomorphic to a typed λ-calculus term:

• Identity Axiom (A ⊢ A) ↔ x
• Modus Ponens / Left Implication (L_IMP) ↔ apply(f, x)
• Conjunction Introduction (R_AND) ↔ pair(M, N)
• Disjunction Case Analysis (L_OR) ↔ case(s, ...)
• Negation Elimination / Refutation (R_NOT) ↔ refute(A)

This produces a compact, 1-line mathematical certificate verifiable in O(n) time by external type checkers.

---

Model Architecture Specifications

• Parameters: 4,927,812 (~4.93M)
• Layers: 6 Transformer Blocks with Bidirectional Cross-Attention
• Hidden Dimension (d_model): 256
• Attention Heads: 8
• Span Pointer Head: Scaled dot-product attention pooling over comma-delimited antecedent spans (up to 32 antecedents)
• Epistemic Head: 3-Class linear projection ([P(False), P(Undecided), P(True)])
• Block Size (Context): 256 tokens
• Vocabulary Size: 95 logical and domain tokens
• Weight Precision: FP32 / BF16 (model.safetensors, 19.6 MB)

---

Training Data

nanoGentzen-v3 was trained on the Gentzen-Kripke-240K dataset, containing 240,000 certified sequents and derivation steps balanced 1:1:1 across Saul Kripke (1965) epistemic states:

• Class 2 (PROVEN_TRUE, V = 1.0): 80,000 certified constructive proofs & multi-hop Horn policies.
• Class 1 (INTUITIONISTIC_UNDECIDED, V = 0.5): 80,000 premise-deprived policies & non-constructive fallacies (LEM, Peirce's Law, DNE).
• Class 0 (PROVEN_FALSE, V = 0.0): 80,000 certified refutations & policy violations.

---

Technical Documentation & Training Code

The complete training codebase, synthetic dataset generators, and extended documentation are available in the open-source GitHub repository DigitLib/nanoGentzen-v3_train:

• Methodology & Theoretical Foundations: Gentzen LJ calculus, Dyckhoff G4ip termination, Saul Kripke relational semantics, Relevance Logic witness tracking, and Curry-Howard isomorphism.
• Neural Architecture Specifications: Transformer backbone, Span Pointer antecedent attention head (32 slots), Kripke 3-class projection head, and parameter breakdown.
• Training Workflow & Methodology: 3-class synthetic corpus curriculum, trajectory-grouped cross-validation, multi-task joint loss supervision, AdamW optimization schedule, and fine-tuning commands.

---