Skip to content

Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs

🕒 Published (v1): 2026-07-14 11:33 UTC · Source: Arxiv · Venue: ICML 2026 · link

Why this paper was selected

ICML 2026; formal evidence-attestation for agentic reasoning; directly addresses hallucination in tool-using agents

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

EG-VAR is a Lean 4-based agentic architecture that eliminates unsupported "verified" LLM outputs on empirical claims by requiring every accepted answer to structurally descend from a tool-attested evidence leaf and pass a Lean kernel type-check. On TableBench (n=120), it achieves 120/120 versus a 95% same-tool baseline; under counterfactual stress it remains 100% source-faithful while same-tool drops to 80–90%. Residual error reduces to semantic mis-formalization (3.3% on Sonnet, 1.7% on Opus), which is addressable by fine-tuning.

Problem

LLMs hallucinate on empirical facts even when given tool access: (1) models exhibit confirmation bias, retaining parametric priors over retrieved evidence (∼12–15% prior-retention on counterfactual tables); (2) tool access provides no formal guarantee that an accepted output actually descends from retrieved evidence or that inference steps are deductively valid. Existing approaches — symbolic factual verifiers, LLM-driven math provers, execution-attestation systems — each cover only part of the trust pipeline and leave mapping-error or wrong-but-attested residuals.

Method

EG-VAR organizes the agentic inference loop into a four-layer trust-stratified stack:

  • L1 (trusted, deterministic): A tool layer that executes queries (cell lookups, filtered aggregates) and produces Attested T witnesses — typed runtime objects that record query, source identity, and result. Only the runtime can produce Attested T terms.
  • L2 (audited offline): A per-source formalization layer mapping L1 storage facts (e.g., CellAt r "state" "alabama") to L2 world-ontology claims (e.g., ArgmaxWhere "rate" all "alabama" v) via a curator-audited list of typed lift axioms \(\Lambda(s)\).
  • L3 (trusted): The Lean 4 kernel, which is the sole minter of Evidence Verified w via the rule mkVerified, requiring an Attested T hypothesis. No LLM component can synthesize Attested T terms; the kernel rejects any proof lacking them.
  • L4 (untrusted): The solver LLM, which receives a typed \(\Sigma\)-goal (e.g., \(\Sigma\,(e:\text{String})\,(v:\text{Value}),\;\text{ArgmaxWhere}\;\ldots\)), calls tools, and proposes Lean tactics; the kernel checks each tactic and returns rejection messages for revision.

Evidence carries an explicit grade \(g \in \{\text{VERIFIED}, \text{SUPPORTED}, \text{PLAUSIBLE}, \text{SPECULATIVE}\}\) with downcast-only rules; no upcast path exists, preventing conclusions from outranking their weakest premise. On rejection, the system returns an honest ABSTAIN with a replayable audit trail (leanFile, evidence, steps) rather than a confident wrong answer.

Two formal safety theorems underpin the architecture: Theorem 3.1 (no unsupported VERIFIED outputs) and Theorem 3.2 (no deductive errors — every accepted proof step type-checks under the declared axiom set).

Key Contributions

  • First Lean 4-verified architecture for empirical (non-mathematical, tool-grounded) claims, combining proof-assistant checking with tool-attested grounding and structural honest abstention.
  • mkVerified as the sole VERIFIED constructor, requiring a runtime-emitted Attested T witness — a structural, not statistical, guarantee.
  • Per-source lift catalog (\(\Lambda(s)\)) separating L1 storage semantics from L2 world-ontology claims, making both independently auditable.
  • Proof object (leanFile, evidence, steps) as a replayable, third-party-verifiable audit artifact (no LLM re-run required).
  • Formal governance translation: tool-attestation-as-axiom for independent output audit; typed grade discipline for queryable uncertainty; honest abstention as a measurable system property.
  • Curator corpus of (claim, gold goal) pairs released as supervised training data for NL-to-formal formalizer fine-tuning.

Results

  • Tier 1 (TableBench, n=120, gold formalization, Sonnet): EG-VAR 120/120 (100%) vs. Tools-curated 114/120 (95.0%) vs. Tools-open 113/120 (94.2%) vs. Table-only 107/120 (89.2%).
  • Tier 1.5 (counterfactual stress, 5 domains × 2 models × 2 flip magnitudes, n=20/panel): EG-VAR 100% source-faithful in every cell; same-tool (Tools-curated/Tools-open) on Sonnet drops to 80–90% under extreme and subtle flips; no-tool baseline 50–80%.
  • Tier 2 (end-to-end with LLM formalizer, n=120): Sonnet: 84.2% correct, 3.3% semantic formalizer error, 4.2% ambiguous (logged), 1.7% benchmark-gold error (surfaced), 2.5% honest abstain, 4.2% solver gave up. Opus: 87.5% correct, 1.7% formalizer error, 4.2% ambiguous, 1.7% benchmark error, 5.0% honest abstain, 0.0% solver gave up.
  • Counterfactual prior-retention baseline (no-tool, no anchoring cue) reproduces ClashEval ranking at ∼12–15% table context override.

Limitations

  • Empirical evaluation is restricted to the tabular substrate; cross-substrate validation (SQL views, typed APIs, knowledge graphs) is explicitly flagged as future work.
  • Semantic mis-formalization error is non-zero at current LLM capability (3.3% Sonnet / 1.7% Opus on Tier 2), and the structural VERIFIED guarantee does not cover semantically wrong but syntactically valid formalizations.
  • Semantically wrong audited lifts (\(\Lambda(s)\)) and source-data corruption that passes the runtime identity-cell validator are explicitly out of scope of the safety theorems.
  • Per-source lift curation is an offline manual/semi-automated cost; the formalization flywheel argument for amortization is prospective, not demonstrated.
  • Tier 1/1.5 results use fixture-committed gold formalization goals (bypassing the LLM formalizer), so reported 100% numbers do not reflect full deployment-path accuracy.
  • All experiments use temperature 0 with one canonical run per EG-VAR condition; multi-rep replication is only partial.

Relevance to Agentic AI / LLM Agents

EG-VAR directly addresses a core failure mode of tool-augmented LLM agents — that tool access does not guarantee that accepted outputs are actually grounded in retrieved evidence — by interposing a formal kernel between the LLM solver and the output label. For researchers tracking agentic AI, the architecture offers a concrete technical-governance interface: the agentic loop is restructured so that the LLM is one untrusted layer in a formally stratified stack, and the kernel enforces grounding as a structural invariant rather than a prompt-engineering convention. The honest-abstention mechanism is particularly relevant to high-stakes agent deployments where silent hallucination is worse than a declined answer. The per-source lift / tool-attestation pattern is source-agnostic and extends naturally to agent architectures over SQL, APIs, and knowledge graphs, making EG-VAR a candidate building block for verifiable agentic pipelines beyond tabular reasoning.