grounded-reasoning — Grounded, Guaranteed Reasoning for LLMs & Agents

TL;DR. LLMs hallucinate on multi-hop relational reasoning. This is a relation-algebra verifier an agent calls to check a claim before asserting it: zero model tokens, precision-guaranteed (accepts a claim iff a grounded proof path exists), language-agnostic, and provider-agnostic. Plugs in as a library, a function-calling tool, or an MCP server. Validated on real LLMs (DeepSeek et al.) and the public CLUTRR benchmark. See docs/integration.md.

📄 Full paper: PAPER.md · Integration guide: docs/integration.md · Try it in 30 seconds: quickstart notebook

Đọc bằng tiếng Việt: README.vi.md

Why this exists

LLMs are solid on one-hop facts but collapse on composition — chaining several correct facts into a multi-step conclusion. On CLUTRR (kinship reasoning), DeepSeek's accuracy falls off with depth, while a grounded operator-composition solver holds ~100% flat — at zero tokens:

acc
100% ●─────●─────●─────●─────●─────●─────●   ● Grounded solver (algebra, 0 tokens)
 90% |
 80% ○
 70% |  ╲
 60% |   ╲
 50% |    ╲
 40% |     ○           ○                     ○ DeepSeek (LLM)
 30% |      ╲         ╱ ╲
 20% |       ○─────○     ╲
 10% |                    ○─────○
  0% +──┴─────┴─────┴─────┴─────┴─────┴─────┴─
      hop 2    3     4     5     6     7     8   (composition steps)

     hop:      2     3     4     5     6     7     8
     DeepSeek: 83%   42%   25%   25%   42%   17%   8%
     Solver:   100%  100%  100%  100%  100%  100%  100%

(CLUTRR/v1 gen_train234_test2to10, clean-chain, n=12/hop; full test set n=635: solver covers 99.5%, accuracy 99.2%. grounded_reasoning/experiments/clutrr_eval.py.)

What it is / is NOT (honestly)

Is: a guaranteed reasoning-verification layer built on relation operator algebra.

• Precision = 1.0, guaranteed (Theorem G) — accepts a claim only if a grounded proof path exists.
• Zero extra tokens — local matrix multiplication, no LLM call. Compare to "have the LLM self-verify," which costs +110% tokens for 34% precision.
• Two-sided guarantee (Theorem I) — precision and recall both have tight bounds.
• No external KB required (SGDC) — uses the LLM's own internal consistency. Precision=1.0 is conditional on the LLM's own atomic facts being sound; that assumption can be measured too — calibrate_transitivity doesn't care whether facts came from an external KB or the model's own assertions, so it already calibrates SGDC's real output precision with zero new code (see self_grounded_calibration_eval.py, PAPER.md §6's remark).

Is not: an "unprecedented breakthrough." The Katz index, the Neumann series, graph reachability, and neuro-symbolic grounding are all classical math and technique. The contribution here is unification, a measured guarantee, and benchmark numbers — not a new primitive. The guard needs a relation graph (supplied, or extracted from LLM facts); flexibility is bounded (see PAPER §5).

Two sharp edges the algebra itself can't see (and how to guard them)

Raised in review, reproduced, and fixed with an opt-in guard each — not swept under the rug:

• Entity identity is exact-string by default. If an LLM extraction is inconsistent about one entity's surface form ("Bob" vs "bob"), the graph treats them as two nodes and a real path silently breaks — the guard then (correctly, per its own contract) rejects a claim that is actually true. Fix (binary): GroundedReasoner(normalize=lambda s: s.strip().casefold()) folds surface-form variants together before they become graph keys; proofs still display each entity's original first-seen spelling. Theorem N characterizes exactly when this is safe: precision stays exactly 1.0 as long as normalize never merges two genuinely distinct entities — that's the only way it can go wrong, so it's exactly what gr.calibrate_normalization(labeled_pairs) measures from held-out evidence, reusing the same Clopper-Pearson machinery as Theorem M.
• Theorem G doesn't know if via is transitive in reality. It guarantees "a path exists under the closure of via," not "via actually composes in the world." Compose a relation that's only partially/conditionally transitive ("trusts": A trusts B, B trusts C, does not imply A trusts C) and you get a confident, mathematically correct grounded=True that answers a different question than the one you meant to ask. Fix (binary): GroundedReasoner(transitive_relations={"parent", "is_a", ...}) makes the guard raise ValueError for any undeclared relation, turning a silent modeling assumption into an explicit, checked one. Fix (measured — Theorem M): gr.calibrate_transitivity(rel, labeled_pairs) replaces the binary declare-or-reject with an actual number — a Clopper-Pearson lower confidence bound on "a graph-grounded claim for rel is really true," computed from held-out labeled pairs. Where the binary guard can only guess or block outright, the calibrated bound tells you how much to trust it.

Both opt-in guards are off by default (identical behavior to previous releases). Reproductions: tests/test_agent.py::TestEntityNormalization, ::TestTransitiveRelationsGuard, ::TestTransitivityCalibration, ::TestNormalizationCalibration; the A/B comparisons: transitivity_calibration_eval.py, normalization_calibration_eval.py.

Heterogeneous relation chains. verify(via=rel) composes ONE relation with itself; gr.verify_path(subject, obj, via=["parent","employer"]) composes an exact sequence of different relations (e.g. a derived "financially dependent on" claim) — not new math (OperatorRelationAlgebra.follow already composes mixed-relation chains exactly per Theorem G, this just exposes it at the facade with proof-path reconstruction) — and gr.calibrate_path(via, labeled_pairs) calibrates that fixed pattern with the same Clopper-Pearson engine as calibrate_transitivity (see PAPER.md §5.3.4). Checked against independent ground-truth BFS across 8,000 triples with zero mismatches: tests/test_agent.py::TestHeterogeneousPathVerification, heterogeneous_path_calibration_eval.py.

How this differs from the usual fixes

Three theorems, one operator (F = G = H)

The reasoning core rests on a single unification (numerically verified, zero error):

⟹ fuzzy inference is spectral analysis of the relation operator. grounded_reasoning/reasoning/.

Six further theorems extend this core: I (two-sided precision/recall guarantee for a self-grounded, no-external-KB variant), J (closure-learning completeness, validated on CLUTRR), K (conformal reasoning — distribution-free coverage under a noisy relation graph, including one extracted by an LLM from raw text), L (Horn forward-chaining, generalizing transitive closure to conjunctive rules), M (empirical transitivity calibration — a Clopper-Pearson confidence bound replacing a blind transitivity assumption with a measured one), and N (normalization precision isolation — precision=1.0 breaks only via an over-merge, and only that is what needs calibrating). All nine are stated, proved, and numerically verified in PAPER.md.

Evidence on real LLMs (DeepSeek)