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

Related MCP server: Proofworks

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)

Guaranteed reasoning over a graph an LLM extracted from raw text

The guard/solver needs a clean graph. But if you let an LLM extract relations from natural-language text, the graph is noisy (missing/spurious edges). Conformal Reasoning (Theorem K) fixes exactly that: use operator confidence as a score, calibrate a threshold ⟹ distribution-free coverage ≥ 1−α, even on a noisy graph.

End-to-end demo: DeepSeek extracts an "is a" graph from text → conformal runs on that extracted graph (ground truth is used only for scoring):

The LLM's extraction drops 31% of the edges (a genuinely noisy graph) → the coverage guarantee still holds (93% ≥ 90%), only efficiency degrades. Validity always holds; efficiency scales with graph quality.

⟹ A path to guaranteed reasoning over natural-language relations — where the hard guard can't reach. grounded_reasoning/experiments/conformal_llm_eval.py.

Efficiency can be pushed further under dropout-dominant noise, at no cost to validity. ConformalReasoner.calibrate(..., group_fn=...) calibrates a separate threshold per group instead of one global one (Mondrian conformal — classical, not new); redundancy_group groups a pair by whether it has more than one walk in the extracted graph, computable with no ground truth. A different grouping tried first (hop-distance) was numerically falsified before shipping — it made efficiency worse, not better, and was discarded. Redundancy grouping cuts FPR from 98.7% → 80.8% when dropped edges dominate the noise (matching this system's real LLM-extraction noise mode) while coverage still holds ≥90% — and honestly gives ~no benefit when spurious added edges dominate instead. redundancy_conformal_eval.py, PAPER.md §7.1's remark.

A different, orthogonal weakness — the noise level DRIFTING over time, not being heterogeneous — needs a different classical tool. Split-conformal (and its Mondrian extension above) assumes calibration and test data share a distribution; that breaks if extraction quality changes between document batches. AdaptiveConformalReasoner (Adaptive Conformal Inference — Gibbs & Candès, 2021, classical, not new) updates its threshold from a stream of confirmed-true examples instead of freezing it after one calibration. When noise shifts partway through a stream (p_drop 0.05 → 0.45), a frozen threshold's coverage collapses from 88.6% to 47.6% — well below the 90% target, silently — while ACI recovers to 89.6%, in 15/15 trials tested. drift_conformal_eval.py, PAPER.md §7.1's remark.

Strongest efficiency result: removing the specific bad edges beats calibrating around them. identify_suspect_edges removes any edge that appears on a held-out FALSE-labeled claim's proof path and NO true-labeled claim's — a simple decision rule, not a statistical guarantee. Verified across 5 noise regimes (60 seeds each): FPR drops substantially and consistently everywhere, e.g. 77.0% → 49.2% (dropout-dominant) and 58.7% → 15.7% (spurious-dominant, where redundancy_group gives almost nothing) — coverage on the remaining graph essentially unaffected. Unlike every calibration method above, this one carries no false-discovery-rate guarantee — a real, measured tradeoff: at the default configuration (identify_frac=0.5, min_evidence=1), the pooled wrongly-removed rate ranges 13.2%–32.2% across regimes. At the recommended configuration (identify_frac=0.85, min_evidence=2, found by a Pareto sweep — the default of identify_and_prune_edges, which applies it automatically so it's the path of least resistance), it drops to 1.5%–3.1% (95% upper confidence bound 2.6%–6.6%), at the cost of cleaned FPR rising somewhat (e.g. ~49% → ~59% in the dropout-dominant regime, still far below the 77% raw baseline) and a smaller reserved evaluation set. Checked against a real LLM (DeepSeek), not just simulated noise, on data where each candidate edge is backed by exactly one labeled encounter (no query repeated — the realistic case for a deployment that verifies each claim once): the count-based rules above (min_evidence≥2, and its hub-aware use_propagation=True variant) never fire at all on this regime, since they require an edge to independently clear the evidence bar twice, which never happens with single-encounter evidence. Lowering to min_evidence=1 does block real hallucinated edges, but on its own makes downstream FPR worse than doing nothing (63.0% → 70.7%, beats raw in only 4/15 splits) — traced to the diffusion engine's row-normalization concentrating transition probability onto a source's surviving edges once its OTHER edges are pruned. Pairing that same blocking decision with masked_infer (normalizes by each source's pre-prune degree, so removal only ever removes confidence mass, never redistributes it) recovers a real improvement: 63.0% → 54.0%, beats raw in 12/15 splits, with no regression on the synthetic benchmark. A learned (logistic regression) alternative was also tried and rejected: it failed to generalize from synthetic training data to the real data at all. Pruning also costs real recall for any true claim that depended solely on a removed edge, and it edits the graph in place (a one-way change, unlike calibration which only adjusts a threshold). edge_pruning_eval.py, edge_pruning_llm_eval.py, PAPER.md §7.1's remark.

Self-verification with NO external knowledge base (SGDC)

The guard above needs some relation graph handed to it. Self-Grounded Deductive Consistency (Theorem I) removes even that: it exploits the fact that LLMs are reliably accurate on atomic (1-hop) facts but hallucinate on composition. Take the model's own confident 1-hop facts, build the operator closure from those, then reject any of the model's own multi-hop conclusions that fall outside its own closure — self-contradiction is the hallucination signal, not disagreement with an external source.

from grounded_reasoning import GroundedReasoner

# the LLM's OWN atomic facts (no external KB) -- taken at face value
gr = GroundedReasoner()
gr.add_facts([("sparrow", "is_a", "bird"), ("bird", "is_a", "animal")])

# the LLM's OWN multi-hop conclusion, self-verified against ITS OWN facts above
gr.verify("sparrow", "animal", via="is_a")   # grounded=True: self-consistent
gr.verify("sparrow", "plant",  via="is_a")   # grounded=False: self-contradiction, blocked

The honest cost is recall (72% vs. 87%): self-closure is conservative. And Theorem I's precision=1.0 is conditional — it holds if the model's own atomic facts are sound; in a counter-prior domain (e.g. "a whale is a fish"), atomic precision itself can drop, and recall suffers with it (PAPER.md §6 records this honestly rather than hiding it).

That assumption can be measured too, with zero new code. gr.calibrate_transitivity(rel, labeled_pairs) (Theorem M) doesn't care whether gr's facts came from an external KB or the model's own atomic self-assertions — so calling it on a reasoner built purely from an LLM's own facts calibrates SGDC's actual output precision directly, from held-out evidence, instead of assuming atomic soundness. In a synthetic domain with 15% of the atomic facts deliberately wrong, SGDC's real precision fell to ~74% (not the naively-expected ~85% — a single wrong atomic edge composes into several downstream claims, amplifying its damage), and the calibrated bound correctly stayed below that in 98.3% of trials — self_grounded_calibration_eval.py, PAPER.md §6's remark.

Runnable: examples/self_grounded_demo.py (offline) · live on DeepSeek: grounded_reasoning/experiments/self_grounded_eval.py.

Quickstart

pip install grounded-reasoning

# or, for development (tests + lint):
git clone https://github.com/ALEXaquarius/grounded-reasoning
cd grounded-reasoning && pip install -e ".[dev]"
pytest tests/                       # every theorem + offline-locked logic, no network needed

# Use it right now (no LLM/network needed):
python -c "from grounded_reasoning import GroundedReasoner as G; r=G(); r.add_facts([('a','p','b'),('b','p','c')]); print(r.verify('a','c',via='p'))"

# Real-LLM experiments (need a key — read from an env var, NEVER hardcoded):
export DEEPSEEK_API_KEY=sk-...        # bring your own; .env is gitignored
python -m grounded_reasoning.experiments.guard_llm_eval        # hallucination guard
python -m grounded_reasoning.experiments.guard_llm_stress_eval # harder: distractors + traps + high temperature
python -m grounded_reasoning.experiments.self_grounded_eval    # SGDC
python -m grounded_reasoning.experiments.clutrr_eval           # public CLUTRR benchmark
python -m grounded_reasoning.experiments.conformal_llm_eval    # end-to-end conformal (LLM-extracted graph)
python -m grounded_reasoning.experiments.guard_cost_eval       # token cost: guard vs. LLM self-verify
python -m grounded_reasoning.experiments.nl_ontology_eval      # dense anti-commonsense ontology (add run_dense() for the 106/106 result)

Integrating with an Agent / LLM (grounded_reasoning/agent/)

A relation-reasoning verifier for agents: check a multi-hop claim before asserting it — zero model tokens, precision guaranteed (accepts iff a grounded proof path exists).

from grounded_reasoning import GroundedReasoner
gr = GroundedReasoner()
gr.add_facts([("alice","parent","bob"),("bob","parent","carol")])
gr.verify("alice","carol", via="parent")   # Verdict(grounded=True, proof=['alice','bob','carol'], confidence=0.36, relation='parent')
gr.verify("alice","zed",   via="parent")   # Verdict(grounded=False, proof=None, confidence=0.0, relation='parent')  ← hallucination blocked

Three integration paths (details: docs/integration.md):

• Library: GroundedReasoner.verify / filter_claims / contradictions.

• Function-calling: TOOL_SPEC (Anthropic) / openai_tool_spec() (OpenAI) + run_tool — a stateless verify_relation tool.

• MCP server: python -m grounded_reasoning.agent.mcp_server — plugs into Claude or any MCP-compatible agent.

Multi-provider (not just DeepSeek): LLMClient(provider=...) for DeepSeek / OpenAI / Groq / OpenRouter / Together / Mistral / Ollama (local) — all OpenAI-compatible, switch providers without changing code. Multilingual: entities/relations are opaque Unicode strings ⟹ works with any language (cha, 父, والد…) with zero configuration.

A real function-calling demo (agent verifies itself, blocks hallucination): python -m grounded_reasoning.experiments.agent_demo. When the graph is noisy (relations extracted by an LLM from text), use ConformalReasoner for a coverage ≥1−α guarantee instead of hard precision.

Source map

Origin story

This project began as an attempt to invent an embedding-free retrieval algorithm that could compete with dense/RAG retrieval. That research question reached a rigorous, fully honest negative conclusion (ties BM25, loses significantly to dense embeddings — with a proof of why). The same mathematical toolkit — operator algebra, spectral analysis — turned out to have real, measurable value on a different problem: guaranteeing multi-hop relational reasoning. This repository ships only that validated, tested reasoning system; the full retrieval research trail (including every failed attempt, honestly recorded) lives in a separate research repository and is not part of this package. See PAPER.md §1 for the full framing.

Contributing & Community

• How to contribute + research principles: CONTRIBUTING.md

• Code of conduct: CODE_OF_CONDUCT.md · Security: SECURITY.md

• Version history: CHANGELOG.md · Citation: CITATION.cff

• License: MIT (LICENSE)

Principle: proof before code, formal definitions, falsifiability, and honest reporting of negative results — see CONTRIBUTING.md.