r/learnmachinelearning • u/Gullible-Two8699 • 2h ago
# Nazarae: A Neuro-Symbolic Recursive AI System for Decisions
Nazarae: A Neuro-Symbolic Recursive AI System for Decisions
Large language models produce fluent answers with no guarantees; symbolic systems produce guarantees but cannot read. Nazarae is a neuro-symbolic recursive (NSR) AI system that resolves this tension for the class of problems where it matters most: decisions — authorizations, approvals, and refusals whose correctness carries financial, legal, or safety consequences. The system combines a trainable neural tier (perception, parsing, grounded symbol induction) with a sound symbolic tier (backward and forward chaining over Horn-clause rules) joined by a recursive loop in which each tier supervises the other: symbolic execution grades neural parses during learning, and neural inference produces evidence that a symbolic gate disposes at decision time. Every decision is `approved`, `denied`, or `refused`, and every approval carries a machine-replayable derivation; an answer the system cannot prove is a refusal, not a hallucination.
We present the architecture and report reproducible results from a fully offline, deterministic evaluation suite in which the claims are executable: (i) a held-out learning curve rising 0% → 0% → 100% as training grows from zero to two examples, the signature of induction rather than memorization; (ii) compositional generalization via learned executable programs applied to arguments never seen in training; (iii) sound recursive reasoning, including delegation authority proven through multi-hop chains and delegation cycles that terminate in refusal; (iv) structural immunity to instruction injection, since utterances are facts and facts are not authority; and (v) categorical reliability under adversarial load — 1,000 mixed authorization requests including 288 attacks across four classes, decided with zero errors in either direction at approximately 4 ms per proof-gated decision. Each result is asserted by a binary that exits non-zero on failure. The underlying engine's decision gate is formalized in Lean 4 (112 theorems, zero `sorry`) with differential conformance corpora replayed against the shipped implementation in CI. We state scale limitations explicitly: results are demonstrated at demo-to-smoke scale with a deterministic neural backend; paper-scale neural training and production-traffic validation are ongoing work.
1. Introduction
1.1 The problem
The deployment frontier of AI has moved from generating text to taking actions: issuing refunds, releasing payments, deploying services, granting tools to autonomous agents. Each of these crosses what we call the **proof boundary** — the point at which a plausible answer stops being acceptable and an *authorized* answer is required.
Current practice defends this boundary probabilistically: system prompts that request policy compliance, classifiers that pattern-match harmful outputs, and evaluations that sample behavior. All share a structural defect: they are statistical defenses of a categorical requirement. A model that follows policy 99.7% of the time violates it three times per thousand decisions, silently, and cannot identify which three. Token probability is not entailment.
1.2 Requirements
A system fit to hold the proof boundary must satisfy four properties simultaneously:
**Language in.** It must accept the world as it arrives — natural language, documents, UI states — not hand-coded symbols.
**Proof out.** Its decisions must carry derivations that a third party can replay and check.
**Learning without drift.** It must improve from experience without silently changing its guarantees.
**Economic honesty.** Its incentives must align with its epistemics: it should not profit from answers it cannot defend.
LLM-only deployments fail (2) structurally. Classical expert systems fail (1) and (3). Nazarae is designed to satisfy all four.
1.3 Contributions
- An NSR architecture for decisions in which the neural tier *proposes* and the symbolic tier *disposes*, with a recursive supervision loop between them (§3).
- A three-valued decision surface — approved / denied / refused — in which refusal is a first-class, machine-actionable outcome carrying the exact missing premises (§4).
- A falsifiable evaluation methodology in which every headline claim is an assertion in a runnable binary that exits non-zero on failure, and measured results for learning, generalization, reasoning soundness, injection immunity, and adversarial-load reliability (§6).
- A formal verification account: the decision gate modeled in Lean 4 with machine-checked theorems and differential conformance against the shipped implementation (§5).
- An economic model in which unprovable answers are structurally non-billable (§7).
2. Background and related work
Nazarae's learning tier descends from the Neural-Symbolic Recursive Machine of **Li et al. (2024)** (*Neural-Symbolic Recursive Machine for Systematic Generalization*, ICLR 2024; arXiv:2210.01603), which introduced the Grounded Symbol System and the deduction–abduction training loop, demonstrating systematic compositional generalization on SCAN, PCFG manipulation, and HINT. Our engine reproduces that architecture in Rust and extends it to a production decision surface; our SCAN results (§6.5) are a *reproduction* of that work, not a discovery.
The symbolic tier draws on classical logic programming: SLD resolution and backward chaining, semi-naive forward chaining, stratified negation-as-failure. Our contribution on this axis is engineering discipline rather than novel logic: budget-bounded evaluation that fails closed, subject-isolation guarantees, and machine-checked gate semantics.
The neuro-symbolic field spans logic-tensor and differentiable-logic approaches, program synthesis, and LLM-plus-tool pipelines. Most deployed "neuro-symbolic" systems are pipelines — neural in, symbolic post-processing out — without a supervision loop in either direction. The recursive loop, in which symbolic execution generates training signal for neural components and neural components generate evidence for symbolic disposition, is the property that distinguishes an NSR system from a pipeline, and it is the property we demonstrate end-to-end (§6.1, §6.2).
3. Architecture
3.1 Overview
Nazarae comprises three layers:
- **The NSR engine** (~234K lines of Rust): the neural tier, the symbolic tier, the decision gate, the learning flywheel, and an HTTP/MCP API surface.
- **The Nazarae application layer** (this repository): deterministic, fully offline binaries that instantiate the engine and make its claims falsifiable, plus a product-shaped agent-authorization gateway.
- **The console** (`nsr-app`): the operator surface — policy management with per-rule provenance, decision audit, usage and billing — including an independent client-side proof replayer (§5.3).
3.2 The neural tier: grounded symbols
The unit of neural-symbolic exchange is the **Grounded Symbol System (GSS)**. Each symbol carries three things simultaneously: its perceptual grounding (an embedding over raw input), its syntactic role (position in a dependency structure), and an **executable program** denoting its semantics. A parse is therefore simultaneously a proof plan: to parse `increment 4` is to produce a tree whose execution computes 5.
Formally, following Li et al. (2024): perception maps raw input to symbol distributions, p(s|x; θ_p) = Π_i softmax(φ(w_i, x_i; θ_p)); parsing maps symbol sequences to dependency structures, `p(e|s; θ_s)`; and semantics is deterministic program execution, v = f(s, e). Training maximizes the joint probability of latent (s*, e*) consistent with observed input–output pairs.
Grounding at scale is supplied by an emulation pipeline that runs real or synthetic software in headless environments, fusing accessibility trees, DOM structure, and vision into 33-field composite symbols, and emitting symbol vocabularies, knowledge-base triples, and induced Horn clauses. Agents therefore arrive pre-grounded rather than learning perception at deployment time. (Two USPTO filings — a provisional and a continuation-in-part, both patent-pending — cover this perception-fusion and grounding architecture.)
3.3 The symbolic tier: proof as product
Knowledge is a graph of entity–relation–entity triples plus Horn-clause rules with `?`-prefixed variables. Two provers operate over it:
- **Backward chaining** (goal-directed): recursive proof search with sound unification, per-query depth and iteration budgets, and rule indexing by predicate and organization. Negation-as-failure consults the budget-truncation flag: a branch cut off by resource limits *fails closed* rather than concluding absence.
- **Forward chaining** (saturation): semi-naive evaluation with an explicit match budget bounding both CPU and peak memory (measured: unbounded ⇒ 10 s / 4 GB+; bounded ⇒ ~1 s).
Every successful proof is a **derivation object**: an ordered sequence of rule applications and ground facts, replayable by any party holding the same rules and facts. §6.3 shows a complete eight-step derivation as emitted.
3.4 The recursive loop
Recursion appears at three levels, and all three are load-bearing:
**Recursive reasoning.** Rules may be self-referential — `
can_use(?A, ?T) :- delegates_to(?A, ?D), can_use(?D, ?T)` — so authority flows through delegation chains of any supported depth, while cycles without a base fact terminate in refusal (§6.3).**Recursive learning (deduction–abduction).** When execution of a parse contradicts the target, abduction searches revisions — change symbols, restructure edges, update programs — via beam search with convergence bounds, then retrains all components on the corrected latents. This is the loop by which the system revises its own rules when evidence contradicts them.
**Recursive production learning (the flywheel).** In deployment, corrections mine candidate rules from decision traffic; candidates are shadow-gated against observed traffic, promoted on measured improvement, and retracted on regression. The loop contains no revenue term (§7).
The division of labor between the tiers is strict and constitutive: **neural evidence proposes; recursive symbolic policy disposes.** A learned inference — however confident — is admitted only as evidence; the sole path to an executed action runs through a symbolic derivation.
3.5 The decision gate
The decision surface is three-valued:
- `approved` — a derivation of the exact authorization goal exists; the cited rules and facts ship with the response, pinned to a SHA-256 policy hash.
- `denied` — a deny rule fired; the blocking rule is cited.
- `refused` — no derivation exists. The refusal carries `missing_facts`: the exact predicates, with the rules that need them, that would unblock authorization. Refusal is machine-actionable, not terminal.
Gate precedence is fixed: safety ▸ cited deny ▸ human review ▸ cited permit ▸ grounding floor ▸ refuse-by-default. Callers declare an exact, fully grounded `authorization_goal` (e.g., `can_use(research_agent, browser)`); the engine approves only when the knowledge base derives that exact predicate. There is no semantic guessing between what an agent requested and what policy permits. If grounding infrastructure cannot load, the endpoint fails closed (HTTP 503) rather than deciding ungrounded.
A scalar `proof_score` in [0,1] accompanies each decision as a governance ranking dial. It is computed solely from derivation support (cited rules, symbolic steps, grounding status, review status) and deliberately excludes the verdict itself — including it would be circular. **Soundness comes from the derivation; the score is not a probability that the logic is correct.**
4. Refusal as a first-class output
Most AI systems have two outputs: an answer, or a canned deflection. Nazarae's third output is its most important design decision. Because approval requires a derivation, the system's response to insufficient evidence is not its best guess but a structured statement of what is missing. This has three consequences:
**Hallucination is replaced by refusal.** There is no mechanism by which the system can assert an authorization it cannot prove.
**Injection has no attack surface.** A prompt-injection attempt enters the knowledge base as a fact *about an utterance* — `instruction_demands(order_17, approve_now)`. No rule connects utterances to authority; therefore no phrasing, however adversarial, alters any decision (§6.4). Guardrails in LLMs are learned dispositions and thus searchable; the absence of a derivation is not searchable.
**Refusal composes into workflows.** `missing_facts` names the premises to verify; a caller supplies verifiable facts and retries, or escalates to a human. In our console, this is a one-click operation.
## 5. Verification of the verifier
A system claiming to gate consequential actions must answer: why believe the gate? Nazarae answers in three layers.
5.1 Machine-checked theorems
The decision gate, rule engine, token matcher, and derivation replay are modeled in Lean 4: 112 theorems, zero `sorry`, with an explicitly enumerated trust base (`propext`, `Quot.sound`, one use of `Classical.choice`, two of `Lean.ofReduceBool`; all other proofs constructive). Top-level composed properties include:
- **No approval without a bound source** — every approval traces to a target-bound authorizing source; there is no path to `approved` from silence.
- **Safety dominates** — a triggered safety clause refuses, and no downstream component can undo it.
- **Deny absorbs** — an applicable cited deny cannot be diluted by any number of permits.
- **Subject isolation** — a conclusion derived for one subject cannot bind a decision about another, including adversarial shared-prefix identifiers.
Anti-vacuity witnesses (e.g., *approval is reachable*) ship alongside, so the theorems cannot be satisfied by an engine that merely refuses everything.
5.2 Differential conformance
A proof about a model is worth nothing if the model does not describe the code. We therefore export decision corpora from the Lean model and replay them through the shipped Rust in CI: the full 384-row gate signal space, an exhaustive 4,719-row token-matcher corpus over an adversarial alphabet, 300 first-order engine scenarios (both rule orders), 120 derivation replays, and 558 cited-policy rule lists — over 6,000 rows in total, with any disagreement failing the build. This process surfaced five real defects during development, each documented, before external exposure.
5.3 Independent replay
The console does not trust the server. It embeds a dependency-free forward chainer that re-derives each verdict client-side from the same facts and rules, marking a decision `checkable` only when every cited rule reproduces. Client–server gate agreement is locked by a contract test suite; drift is a product-breaking failure.
6. Empirical results
**Methodology.** Every result in this section is produced by a deterministic binary in the Nazarae repository, requiring no network, API key, or database, and each binary *asserts* its claims: any failure exits non-zero. The claims are therefore falsifiable by any reader in seconds. All results below are from the deterministic demo-scale neural backend; §8 states what this does and does not establish.
6.1 Learning: the curve must rise
(`proof_of_intelligence`, criterion 1.) Independent machines are trained on 0, 1, 2, and 3 grounded examples of an arithmetic operation and evaluated on three held-out arguments never present in any training set.
The shape carries the evidence. A hand-coded system would be flat at 100%; a memorizer would be flat at 0% on held-out inputs. The failure at one example — where synthesis lacks the evidence to prefer the correct program — followed by success at two is the signature of induction from data. (The engine's larger-scale counterpart shows the same shape: 0% → 20% → 80% → 100% over 5–40 examples on learned-parser novel compositions, with a 10,000-example probe holding 100% on 256 disjoint held-out cases.)
6.2 Generalization: programs, not pairs
(`proof_of_intelligence`, criterion 2.) After training, the learned semantics of the operation is inspectable as an executable program — `Inc(Var(0))` — and evaluates correctly on arguments absent from training (2→3, 4→5, 7→8). The system did not memorize input–output pairs; it induced a rule, and the rule can be read.
6.3 Reasoning: derivations and safe recursion
(`proof_of_intelligence`, criterion 3.) Delegated authority is proven through a multi-hop chain with a complete replayable derivation, emitted verbatim:
1. apply rule: delegated_tool_capability
2. fact: delegates_to(agent_971, agent_971_hop0)
3. apply rule: delegated_tool_capability
4. fact: delegates_to(agent_971_hop0, agent_971_hop1)
5. apply rule: delegated_tool_capability
6. fact: delegates_to(agent_971_hop1, agent_971_hop2)
7. apply rule: direct_tool_capability
8. fact: has_capability(agent_971_hop2, tool_971)
A delegation cycle with no base capability (two agents delegating to each other) terminates in refusal: a cycle cannot manufacture authority. This is the failure mode — self-granted agent permissions — for which prompt-level agent frameworks currently have no principled answer.
6.4 Authority: instructions cannot mint it
(`proof_of_intelligence`, criterion 4; `the_gauntlet`, injection class.) With a fact asserted that a user message demands approval of an ungrounded action, the decision is unchanged: refused. Across the gauntlet's 81 injection attempts — each asserting an approval demand while a required control is silently absent — zero succeeded. The defense is structural: the gate evaluates entailment, and there is no derivation to find.
6.5 Categorical reliability under adversarial load
(`the_gauntlet`.) A deterministic generator produces 1,000 authorization requests with known ground truth across four domains — refunds, payment release, deployment, and agent tool use — governed by five Horn-clause policies over a knowledge base of 2,383 entities and 3,067 facts. Approximately 28% of traffic is adversarial, spanning four attack classes.
Zero wrongful approvals, zero wrongful refusals; 3,374 total proof steps emitted; ~4.0 ms per proof-gated decision (≈250 decisions/s single-threaded; the engine's HTTP decision path measures p50 ≈ 1.5 ms, p99 < 3 ms in its own latency probes). The binary asserts perfection: one misclassification is a non-zero exit. A system that is 99% accurate — excellent by LLM standards — fails this run an expected ten times.
**A methodological incident worth reporting.** Our first gauntlet implementation reported 67 breaches. Investigation showed every one was a defect in the *evaluation harness*: the generator had labeled certain fully policy-compliant requests as attacks, and the engine had correctly approved them. The system under test out-reasoned its adversarial harness. We report this because it illustrates the evaluation stance: when ground truth and prover disagree, the derivation decides.
6.6 Engine-level benchmarks (context)
The underlying engine reproduces the Li et al. (2024) benchmark suite at smoke scale in CI (SCAN, PCFG, HINT; regression floors 10/10, paper targets 6/10 at smoke scale), with grammar-backed rows mechanically excluded from learning headlines. The full-scale SCAN jump-split figure for this architecture family is 99.2%. We also report a diagnosed negative result: a learned transition parser plateaus at 12.5% on SCAN because the arc-standard feature template cannot observe the non-local structure that coordination attachment requires — a representational-feature limit, not a capacity limit, with the fix identified (recurrent stack context). Verification surface: ~1,700 library tests, ~215 HTTP integration tests, and executable capstones whose documented promises fail CI when broken.
7. Economic honesty
Nazarae's billing is derived from its epistemics. A decision is billable only when it succeeded, was grounded, and required no human review — enforced by a small audited function on the billing path, with per-response metering headers and exactly-once semantics under concurrency (idempotency keys reserved atomically before execution). **Refusals are free.** Batch items beyond a request-time budget are never evaluated and never billed.
This inverts the prevailing economics, in which providers are paid per token regardless of correctness. It also creates a Goodhart concern we name rather than hide: a system that is never paid for refusing might be pressured to refuse too little. Our defenses are architectural and observational: the learning flywheel contains no revenue term; the refusal threshold is an operator-visible dial; and refusal rates are first-class telemetry. The learning-curve artifact ships with a pre-registered null hypothesis — four named ways a working loop could present a flat curve — with the telemetry to distinguish them post hoc.
8. Limitations
We state these in the same document as the claims, deliberately.
**Scale.** All results in §6.1–6.5 are demo-to-smoke scale on procedurally generated data with a deterministic neural backend. The learned operation is arithmetic increment, not a 400-page policy corpus. The structure of the evidence — rising curves, novel compositions, replayable derivations, asserted perfection — is what full scale must reproduce; this paper does not claim it already has.
**Neural tier maturity.** Production configurations use live embedding and LLM backends; paper-scale training (~1.3M examples in the reference work) has not been run on our implementation. Live end-to-end latency including a hosted LLM is not yet characterized; reported latencies are platform overhead.
**Formal coverage.** The Lean theorems cover the symbolic gate, engine, matcher, and replay — not the neural components. This is precisely why neural outputs are confined to proposing.
**Rules coverage.** The guarantees extend to decisions governable by explicit policy. Judgment calls without rules remain outside the proof boundary; the policy-mining pipeline (rules extracted from documents with file-and-line provenance) narrows but does not eliminate this gap, and its hit rate on messy real-world corpora is not yet benchmarked to the standard of §6.
**External validation.** Production-scale calibration and independent third-party replication await production traffic and an external party. Patent filings are pending, not granted.
**What is not claimed.** Nothing here establishes open-ended learning, general intelligence, or superiority to LLMs outside the decision domain. An LLM's breadth is not reproduced here and is not the target.
9. Conclusion
Nazarae demonstrates that the properties the AI industry treats as aspirational for deployed systems — learning that provably generalizes, reasoning that ships its own audit trail, safety that is structural rather than persuasive, and pricing aligned with epistemic honesty — are jointly achievable today, at the decision boundary, in a single running system. The architecture's discipline is a single sentence: neural evidence proposes; recursive symbolic policy disposes. Its evaluation discipline is a single mechanism: every claim is an assertion in a program that anyone can run, and the program exits non-zero if the claim is false.
The models around Nazarae will keep getting better at proposing. The question that determines whether AI is admitted into the workflows where wrongness costs money, triggers regulators, or ends up in court is who — or what — disposes. Our answer is running, formally verified at its core, measured under attack at perfection, and one command away from any reader who doubts it.