Grounded Reasoning MCP server

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 gentrain234test2to10, clean-chain, n=12/hop; full test set n=635: solver covers 99.5%, accuracy 99.2%. groundedreasoning/experiments/clutrreval.py.)

What it is / is NOT (honestly)

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

"have the LLM self-verify," which costs +110% tokens for 34% precision.

• 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

Precision=1.0 is conditional on the LLM's own atomic facts being sound; that assumption can be measured too — calibratetransitivity 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 selfgroundedcalibrationeval.py, PAPER.md §6's remark).

• Two-sided guarantee (Theorem I) — precision and recall both have tight bounds.
• No external KB required (SGDC) — uses the LLM's own internal consistency.

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

Shortened. The full README is on GitHub.