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

nanoGentzen-Jev-v3 is a 4.93M parameter (4,927,780 params) Neuro-Symbolic Typed-Decision Engine that unifies a Bidirectional Policy-Value Transformer with a deterministic Gentzen Intuitionistic Sequent Calculus (LI) Verification Kernel.

It evaluates structured JSON states, numeric/regex predicates, natural-language policies, and free-text rubric criteria across three typed decision primitives:

noul: Constructive boolean judgment (true / false / INTUITIONISTIC_UNDECIDED) with formal proof/refutation and missing-fact diagnosis.
choice: Verified multi-option routing (options: [...]) backed by constructive derivations.
score: Ordinal rubric tier scoring (levels: [1, 2, 3, 4]) with verified level proofs and calibrated distributions.

NOTE: This is still in the testing/development phase. Improved version is available. Sagicc/nanoGentzen-v3

Dual JEV Decision APIs (`jev_server.py` & `AutoModel`)

Both APIs accept the exact same DecideRequest payload (state, predicates, policy_rules, questions) and are available both in Python (model.decide(...) / model.system_one(...)) and over HTTP (POST /v1/decide / POST /v1/systemone):

API Endpoint / Method	Mode	Latency	Description
`POST /v1/decide` (`model.decide(...)`)	System-2 Verified Proof Search	`1–25 ms`	Runs neural-guided Gentzen LI proof search (`search.py`) + formal verification (`kernel.verify_proof_tree`), returning certified `proof_tree`s, `missing_facts` diagnosis, and calibrated probabilities.
`POST /v1/systemone` (`model.system_one(...)`)	System-1 Fast Epistemic Gate	`~2 ms`	Single Transformer forward pass returning the 3-Class Epistemic Distribution (`[P(False), P(Undecided), P(True)]`), predicted top rule (`top_rule`), and Span Pointer pivot (`top_pivot`) with zero search overhead.

Key Architectural Features

Span Pointer Antecedent Pivot Head (max_antecedents = 32): Pools token hidden states h_i of each comma-delimited antecedent formula in Γ and scores each premise against the goal representation h_Δ via scaled dot-product attention:
```
logit(pivot_i) = ((W_q · h_Δ)^T · (W_k · h_i)) / sqrt(d_ptr) + b_i
```
3-Class Intuitionistic Epistemic Value Head ([P(False), P(Undecided), P(True)]): Outputs native 3-valued intuitionistic probabilities (PROVEN_FALSE, INTUITIONISTIC_UNDECIDED, PROVEN_TRUE) in a single forward pass, with expected constructive provability:
```
V = P(True) + 0.5 * P(Undecided)
```
Bijective Alpha-Renaming (kernel.py): Automatically compresses arbitrary long enterprise variable names (>300 chars) into canonical symbols (P, Q, R, S, v0..v15) before tokenization and restores original domain names in the verified proof_tree.
Unified Real-World Compiler (parser.py & jev_server.py): Compiles JSON states + PredicateSpec rules (==, !=, >, >=, <, <=, in, contains, regex), symbolic formulas (a & b => c), natural-language conditionals ("If X then Y"), and free-text/JSON rubric criteria (compile_criteria_and_state) directly into Gentzen sequents.

`LocalLLaMA/typed-decisions` Benchmark (400 Test Cases / 2,000 Decisions)

Model	Params	Overall Acc ↑	`noul` Acc ↑	`choice` Acc ↑	`score` Acc ↑	`score` ±1 ↑	Mean KL ↓	Mean Brier ↓	ECE ↓
`Baseline-27B`	`27,000M`	`0.761`	`0.832`	`0.732`	`0.730`	`0.979`	`0.150`	`0.081`	—
`nanoGentzen-Jev-v3` (Ours)	`4.93M`	`0.731`	`0.828`	`0.685`	`0.693`	`0.973`	`0.150`	`0.081`	`0.087`
`SafeDecide-140M`	`140M`	`0.728`	`0.793`	`0.692`	`0.708`	`0.974`	`0.168`	`0.089`	—
`JEV-35B`	`35,000M`	`0.700`	`0.778`	`0.648`	`0.680`	`0.964`	`0.214`	`0.111`	—
`GEV-26B-Decide`	`26,000M`	`0.522`	`0.670`	`0.517`	`0.415`	`0.833`	`0.391`	`0.193`	—
`JEV-27B`	`27,000M`	`0.495`	`0.680`	`0.422`	`0.410`	`0.815`	`0.431`	`0.211`	—

Quickstart

1. Install Dependencies

pip install -r requirements.txt

2. Python API (`AutoModel.decide` & `AutoModel.system_one`)

import json
from transformers import AutoModel

model = AutoModel.from_pretrained(".", trust_remote_code=True).eval()

payload = {
    "state": {
        "user": {"kyc_verified": True, "age": 29, "sanctions_flag": False},
        "tx": {"amount_usd": 450},
    },
    "predicates": {
        "kyc_ok": {"field": "user.kyc_verified", "op": "==", "value": True},
        "is_adult": {"field": "user.age", "op": ">=", "value": 18},
        "clean_aml": {"field": "user.sanctions_flag", "op": "==", "value": False},
        "within_limit": {"field": "tx.amount_usd", "op": "<=", "value": 1000},
    },
    "policy_rules": [
        "kyc_ok & is_adult & clean_aml => verified_customer",
        "verified_customer & within_limit => approve_tx",
        "approve_tx => risk_tier_1",
    ],
    "questions": {
        "approve_tx": {"type": "noul", "target": "approve_tx"},
        "routing_action": {
            "type": "choice",
            "options": ["auto_approve", "manual_review", "reject"],
            "rules": ["approve_tx => auto_approve", "~approve_tx => manual_review"],
        },
        "risk_tier": {
            "type": "score",
            "levels": [1, 2, 3, 4],
            "level_atoms": ["risk_tier_1", "risk_tier_2", "risk_tier_3", "risk_tier_4"],
        },
    },
}

# 1. Fast System-1 Epistemic Gate (~2 ms)
fast_res = model.system_one(payload)

# 2. Full System-2 Verified Gentzen Proof Search + Proof Tree
verified_res = model.decide(payload)
print(json.dumps(verified_res, indent=2))

3. FastAPI Server (`/v1/decide` & `/v1/systemone`)

# Start HTTP server
uvicorn jev_server:app --host 127.0.0.1 --port 8000

# Run full verification suite (in-process or against HTTP server)
python test_jev.py --local

4. Command-Line Interface (`cli.py`)

# Evaluate a single rule/state with System-2 formal proof
python cli.py --mode decide --state "If it is raining then the ground is wet. It is raining." --target "the ground is wet"

# Evaluate with System-1 fast epistemic gate
python cli.py --mode systemone -f request.json

# Launch interactive JEV decision shell
python cli.py

Repository Structure

├── config.json                     # GentzenConfig (4.93M params, pointer_dim=64, max_antecedents=32)
├── vocab.json                      # 95-token character & logical operator vocabulary
├── tokenizer_config.json           # Hugging Face AutoTokenizer configuration
├── special_tokens_map.json         # Special tokens mapping
├── model.safetensors               # Stage-3 production weights (safetensors)
├── configuration_nanogentzen.py    # GentzenConfig
├── modeling_nanogentzen.py         # GentzenPolicyValueModel (.decide() & .system_one())
├── tokenization_nanogentzen.py     # LogicTokenizerHF
├── kernel.py                       # Gentzen LI calculus + Bijective Alpha-Renaming
├── search.py                       # NeuralProofSearch with alpha-renaming & subformula fast-path
├── parser.py                       # Unified symbolic, natural-language & rubric criteria grounder
├── jev_server.py                   # LocalGentzenJevEngine + FastAPI /v1/decide & /v1/systemone
├── example_usage.py                # Real-world example of both `decide` and `system_one` APIs
├── cli.py                          # CLI & interactive shell for `decide` and `systemone`
├── test_jev.py                     # 6-part verification test suite for both JEV APIs
├── requirements.txt                # Runtime dependencies
└── .eval_results/
    └── Sagicc__nanoGentzen-Jev-v3.yaml         # Official Hugging Face evaluation results metadata

License

Released under the MIT License.

Downloads last month: 186

Safetensors

Model size

4.93M params

Tensor type

F32

Model tree for Sagicc/nanoGentzen-Jev-v3

Base model

Sagicc/nanoGentzen-v2

Finetuned

(1)

this model

Dataset used to train Sagicc/nanoGentzen-Jev-v3

Collection including Sagicc/nanoGentzen-Jev-v3

nanoGentzen

Collection

Test for Genzen calculus in LLM logic verification. • 9 items • Updated 9 days ago